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 Tweet is from a suspended account. Learn more
This Tweet was deleted by the Tweet author. Learn more
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. 🤔
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?
1