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
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! 😱
I have a silly mascot though, so at least that's something:
Quote Tweet
1