dreaming of a language with dependent records as modules (like in 1ML, but full spectrum dependent types), multistage stage programming, linearity, erasure, and effects+handlers that can be inlined or compiled to capability passing style (could be handy for custom allocators)
Conversation
Adding this to the list of things I want in this language:
Quote Tweet
Replying to @jonmsterling
Oh, and one thing I'm hoping to do is have each source file be an expression - wired together by the build system in a way that's similar to what's talked about in "A Principled Approach to REPL Interpreters": doi.org/10.1145/342642
2
Replying to
how would you handle the multiple semantic interpretations of the dependent product in the presence of linearity?
1
I dunno! I guess I was hoping that stuff like GrTT might help, but I've not looked too closely into the specifics. Would love to know though!
1
Show replies
It's where you pass resources as parameters to functions.
- Effekt compiles its handlers to this style: effekt-lang.org
- Zig also uses this approach for passing allocators: ziglang.org/documentation/
- There's also this version of the Rust std lib: github.com/bytecodeallian
1
Show replies
Replying to
Can you give me the pitch for Effect Handlers? I've heard them described as "generalised exceptions"?
1
They let you decouple the use of effects from their interpretation. This can let you do cool stuff like scheduling effects synchronously or asynchronously, mocking out dependencies in tests, inserting logging, etc.
1
1
Show replies