Any approach to libraries based on category theory in Rust needs to address explicit fusion via stack allocated adaptors (found in iterators, futures, streams, visitors, etc). This suggests that we might need a more general form of `Functor` than that found in Haskell. 🤔
Conversation
Making a purely functional dependently typed language that's designed to do lots of stack allocation is ambitious... good luck!
1
Hah! Will probably end in tears. 😬
1
I feel like it's really quite tricky because of how big terms usually get... without knowing the size in advance it's hard to put a whole term on the stack without copying. But if most are on the heap, you want fast GC, which usually means no destructors...
1
1
Usually this is where linearity comes to the rescue, but (AFAIK) the terms you get during conversion generally won't be linear even in most existing linear dependent type theories. So this won't help too much.
1
I was planning on using 's Quantitative TT and Context Constrained Computation for this. Which has the advantage of allowing for linearity for all universes (I think?).
1
1
Still unclear how to integrate it with effects and regions though - one of my bigger worries. 😬
Also been going down the rabbit hole watching Bob Harper's Computational TT lectures at OPLSS 2018, and wondering if maybe I'm doing everything wrong! 😱
1
I have a silly mascot though, so at least that's something:
Quote Tweet
1
Integrating dependent type theory of any sort with effects in a sound way is an active research topic so I wouldn't be too concerned about its interactions with another active research topic yet :) . Making TT work nicely with effects seems mostly about restricting dependency.
1
Hehe, yeah. Interestingly I see stuff about 'fibration' popping up with both generative module functors and DT+effect work. Is this coincidence, or is this due to the connection between functors and DTs?
2
Show replies