I was going to say something about Pola and ask if you know of similar exciting developments but all I can find is researchgate.net/profile/Robin_ - I could swear I saw something like a full-blown thesis about it, a while back
Conversation
This Tweet is from a suspended account. Learn more
Sort of related, but I've been thinking of trying to get something where multiplicity > 1 implies some that you need some sort of allocator (ie. in something like & 's bentnib.org/context-constr). But I want that to be configurable. Ugh, it's a hard problem.
1
1
Ie. I want to be able to specify a GC or arena or whatever. And also be able to do something about OOM. All of this kind of needs some interaction between coeffects and effects though, which is well beyond me. And then you get tons of coeffect/effect annotations eeverywhere.
1
Semantic results really should inform the compiler more. I'm not sure what Idris (Blodwen?) does, but I imagine resource information gets erased.
1
Oh, its more about the syntactic burden. Trying to design a nice concrete syntax...
1
Mm. I think in a lot of code, you should be able to get decent resource inference. I guess with type signatures, good defaults would go a long way. Or do you mean something more C/Rust-like?
1
Oh, I want to integrate it into Pikelet, which is a dependently typed functional lang... hoping to get it closer to a Rust/C-style systems language: github.com/pikelet-lang/p
Yeah, hoping that the defaults would help. Needs some experimentation too. I've been watching Blodwen with interest!


