I've been meaning to port the stuff I have for my research thing to nbe-for-mltt.. I can probably just do that this evening
This Tweet was deleted by the Tweet author. Learn more
Conversation
This sounds very interesting, if you have an example I’d love to see it
1
OK, the code is here github.com/jozefg/nbe-for. It will be merged into master once I finish documenting the new type checker
1
1
The type checker is in github.com/jozefg/nbe-for
1
1
Thinks so much for this! Working on porting this to Rust so that I can figure out if I want to use it in Pikelet: github.com/brendanzab/rus - Still need to add a parser, pretty printing, and some tests! 🙂
1
Do you know if recursive definitions could be implemented using this style of semantic type checking? I'm considering going with an Idris approach to this - allow general recursion, but have a totality checker to ensure that a subset of the language terminates.
1
One must be a bit careful that everything is termination-checked before you attempt to normalize it (otherwise normalization might diverge) but if you do this (or are fine with things diverging) it should be fine. Mini-TT supports recursion IIRC
1
2
Currently trying to add the labelled sums from the Mini-TT paper to the language! Just curious, why do you need the type annotations in the values? They seem to manage without it in the Mini-TT paper. 🤔
1
1
This Tweet is from a suspended account. Learn more
Oh yeah, I do know that part wrt. bidirectional type checking, but thanks! I got an answer to the type annotation stuff for normal and neutral terms here: twitter.com/dannygratzer/s - sorry, forgot to link it back to this thread.
Quote Tweet
@brendanzab old thread was getting a bit long: Which type annotations are you referring to? For normal forms?