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. 😬
2
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
This stuff pops up because I've been also wanting to use the context constrained stuff to help mark the phase distinction, but this would then interact with generative modules. Maybe I could just ignore generative modules for now?