I want to implement a cubical type theory based proof assistant from scratch. Any pointers for how to get started? There's a good research reason for this
10
6
58
Conversation
I haven’t done cubical stuff yet, but in doing dependently typed languages I’ve found normalisation-by-evaluation with debruijn indicies in terms and debruijn levels in values to be a pretty good starting point! You might already be on top of that stuff though 😅
2
4
I found exactly the same thing, I wonder abstractly why, roughly the reason is because indices are good for deconstructing terms and levels for reconstructing in terms of sharing but it would be nice to have an abstract reason.
1
1
Yeah, seems to be something like that! Here is a neat post by on the indices+levels approach as well: colimit.net/posts/normalis
1
3
I've also seen indices in terms and HOAS in values - see andres-loeh.de/LambdaPi/ for that. Mini-TT uses strings in terms, levels in values, and indices in normal forms (which are interestingly kept separate from Terms): cse.chalmers.se/~bengt/papers/
2
1
There's a nice implementation of Mini-TT here in Rust, which might find handy as well: github.com/owo-lang/minit - the docs are pretty nice too! docs.rs/minitt/0.4.2/m
