What I like about linear/uniqueness types - at least how Rust does them - is that they don't make types noisier, or increase the annotation burden. (At least, not directly!)
Is there any approach to solving "the problems which lifetimes solve" which is similar, or gets closer?
Conversation
I think I could devise a language where “lifetimes” are syntactically correct by construction—but the explicitness of plumbing values could be an unacceptable “annotation burden”.
In Kitten I’m doing a similar thing to Rust, where a type is inherently [non–]copyable/droppable.
1
2
I'd be interested in your thoughts about that to better understand the design space, even if it's not a clear/immediate improvement. :)
2
Still dunno what to do for Pikelet. 😭
I like the coeffect/effect stuff because you get lots of control, but then you get lots of annotations everywhere. Thoughts ?
1
Trouble is I'm not just interested in regions and linearity/uniqueness. I also want control over the execution phase, erasure, parametericity. But it might all end up being a mess. Also dependent types are hard.
1
2
It's been nice to use McBride-style universe 'lifting/hoisting' in Pikelet to get rid of the noise of all the universe levels you get in Agda and Lean:
- pikelet-lang.github.io/pikelet/langua
- pikelet-lang.github.io/pikelet/append
Perhaps something similar could be done with other 'hierarchies'?
2
2
McBride's use of the term 'hierarchy' here makes me wonder if he's thinking along the same lines! 🤔 twitter.com/pigworker/stat
This Tweet is unavailable.
1
1
That said, I’ve got no clue about soundness or anything. And perhaps precision is more useful for stuff like multiplicities and execution phase 🤔