Prism: An Impure Functional Language With Typed Effects
55 points by jcmkk3
55 points by jcmkk3
I wonder what lenses have to do with effects. Every mention of lenses in the article makes them sound unrelated, except that they are listed under “one trick five ways”.
Also, what the heck is tick_use() supposed to do?! Are readers expected to understand such a convoluted example without explanation? Some type annotations would have helped.
This explains more about lenses: https://sdiehl.github.io/prism/spec.html#86-optic-paths
I still don't see what lenses have to do with effects, other than metaphorically. The author writes:
This is the language’s “effects instead of monads” stance applied to optics, paths instead of optic combinators.
So the metaphor is: monads are values, but effects are not values. They are some kind of control structure. Likewise, lenses are values, but in Prism, “optic paths” are not values, they are some kind of control structure with hard-coded syntax.
That makes sense, thanks for the pointer to the spec! I had got the impression from the overview that lenses were special-case syntax, but that made the relation to effects even more obscure since the syntaxes appeared unrelated to each other.
very impressive! so impressive, in fact, that i wonder why diehl calls the compiler a toy at the end of his post - really seems like a successful PoC for a new level of elegance
I'd be curious to see more of the details of what the call by push value IR looks like. Especially does it handle join points or not. There have been papers that talk about the theory of adjoining CBPV with effects. It's pretty natural to say Computations have an effect type and values don't, but I haven't seen anything fleshed out enough to be directly applicable to kokas evidence passing, so that's quite interesting.
In general I'd be curious to understand how this stands against koka. Between FBIP, perceus, and evidence passing, it's clearly very inspired by kokas work. Its also clearly distinct (it uses CBPV for its IR). But it's hard for me to see how different it is.
Need to spend more time understanding it, but it looks so beautiful
not exactly on topic, but i have always been a bit sad that Stephen’s “write you a haskell” project stalled years back… i hope we get some good tutorial-grade implementation details for Prism!
Oooh it looks a lot like what I keep trying to find time working on. Nice!
This almost reads too good to be true! They even managed to include Verse-like failure semantics, I may need to play with this "toy".
Also, I very much appreciate the pointing to literature, I wish more blogs did this
I'm wondering what's "impure" about this language. That word only appears in the title, not in the rest of the article. It seems that all effects are tracked, so a function without effects is still a mathematical function. Am I missing something?
afaict it is related to local mutation of variables in function definitions, as in the given definition of fib: var x is an impure, mutable variable, let x is a pure, immutable variable.
a function without effects is still a mathematical function
and a function with effects is impure.
Right, but Haskell has "functions with effects" and yet it's still considered pure.
All programming languages have functions with effects. I/O is an effect, so if your language can do I/O, then it has effects. In older imperative languages like C and Python, effects are encoded as “side effects”. Any function can have an effect, but the presence or absence of effects is not encoded in the function type, so we call the effects “side effects”. Haskell has a way of encoding effects using pure functions, using monads. Prism does not use monads, and it is not a pure functional language. In a pure functional language, all functions are pure, and function calls are referentially transparent. Roughly speaking, this means you can replace any function call with the value that it returns, without changing the meaning of a program. Haskell has this property. Prism only has this property when you call pure functions (that is, functions without effects).
Really cool work to take what’s commonly been language a feature (X language has yield’s, Y language has throw’s, etc.) and come up with an implementation of it as just another interface! Being able to build all sorts of different control flows—side effects, exceptions, continuations—on top of one abstraction is an exciting new way to look at a whole category of design questions, and hopefully facilitates or stimulates more exploration and innovation; I certainly suspect I’ll be coming back to this for many years to come for inspiration.
effect handlers come from Koka : https://koka-lang.github.io/koka/doc/book.html#sec-handlers and are really powerful
What you are excited about is effect systems or more specifically algebraic effects. A previous blog post from Stephen Diehl has links to some older languages with algebraic effects; it has been an ongoing research topic for a decade or two.
The concluding paragraph is rather grim, but I do believe first class effects will eventually see the light of day in a widely used language, no matter how satisfied the wider ecosystem is with the status quo
[Lean uses Perceus because] a dependently typed proof assistant cannot afford GC pauses any more than a game loop can.
I'm surprised--is this true? A game needs to finish its frame in ~16ms, but I thought a proof assistant is more like a shell/REPL, where ~300m is probably fine. And lots of UIs are built on languages with GC runtimes.