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
Yeah, haven't really thought through the details on how this stuff might be applied to different structures. I take it you're aware of bentnib.org/context-constr? Perhaps you wouldn't have lifting, but you might have other operations you could do depending on the structure. 🤷♂️
I've seen it float by on here, but haven't increased my awareness over and above that...