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.
Conversation
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.
1
1
(I don't have nearly enough familiarity with / intuition for these matters to be able to give productive input alas)
1
Replying to
Me niether. But you are a friend to cats, so I appreciate your input.
I just find the whole 'level' nomenclature annoying. WHY CAN'T IT BE 'SIZE'?
1
even the "size" nomenclature feels like a not-transparently-intuitive inheritance to me
(possibly they're called levels because it feels more natural to number them than sizes?)
1
Show replies