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
Interesting thought. Transporting the concepts across naively, in Rust lifetime subtyping might correspond to cumulativity, and lifetime polymorphism to, well, universe polymorphism. But then what is shifting (and what is it useful for)?
2
Btw, if you have any thoughts on this terminology bikeshed, please halp github.com/pikelet-lang/p
1
1
I seen it. I like "embiggening". Hope this helps! 😛
1
1
Arrgh I don't know what I was hoping for but thanks I think.
Replying to
(I don't have nearly enough familiarity with / intuition for these matters to be able to give productive input alas)
1
Me niether. But you are a friend to cats, so I appreciate your input.
1
1
Show replies