yeslogic
Switch to an explicitly typed core language
This switches the core language to be explicitly typed, which might make compilation easier down the line, for example when figuring out if we need to compile to a term or a type. I remember this was tricky on my last time trying to implementing compilation/extraction, but I’d like to do some more experiments to see if this is actually the case, however, but this at least demonstrates the idea.
The resulting terms are a bit larger than I’d like, because we need to quote type annotations back to terms during elaboration. Glued evaluation potentially help here.
Closes #270
The resulting terms are a bit larger than I’d like, because we need to quote type annotations back to terms during elaboration. Glued evaluation potentially help here.
Should be fixed by https://github.com/yeslogic/fathom/pull/462? I'd like to see this merged
Hmm, not sure. I think most of the bloat added here is from terms that do not come from user code originally. Because they have been quoted from values, they would need something like glued evaluation to keep them small. Does having explicit type annotations help you in something you are looking at? Should we try to get this merged?
Does having explicit type annotations help you in something you are looking at? Should we try to get this merged?
No, I just wanted symmetry with the type annotations in FunType. But if you want to let it cook longer, no pressure