Open jacereda opened 4 years ago
Huh, yeah the tail variant idea was really cool and interesting. Have you tried it out?
The other thing looks a lot like Liquid types in Haskell, right? It's probably quite hard to implement, I have never done it. Perhaps we can get some of the benefits using macros, it's definitely something to think more about. Perhaps trying to assert some things using macros and seeing what machinery in the compiler could be exposed to make that work...
Haven't tried it, I'm quite snowed under ATM.
It looks like an idiosyncratic approach to liquid types/dependent types. Some of these things can definitely be done with macros (that would be a bit hacky, though, I think); some of them need more typesystem machinery than we currently have. But I always wanted to experiment with dependent types in Carp at one point (though it will take quite a while until we’ll get there I assume).
Thanks for the resource!
I've been looking at this language and IMHO it has some interesting ideas:
https://github.com/aep/zz
I guess the "tail variants" could be used for things like stack-allocated strings on Carp's side.
Also, how hard would it be to implement its
model/where/static_attest/static_assert
magic in Carp?