Mastodawn

RE: https://mastodon.social/@jcreed/116303446377766919

Ok, due to @edwinb mentioning the idea of "dependently typed language on 8-bit computer" I have at least *visually* cleaned up my old experiment from a couple of years ago, here: https://jcreedcmu.github.io/twelf-nes/

But to be completely honest I don't really remember how the thing worked that well. I am pretty sure it could manage to type-check first-order terms, but the invariants even then were kind of subtle and frequently changing during development...

Show thread

jcreed 1d ago

@edwinb nor is this something that is *directly* yet implementable in 6502... but I was trying to get some sort of system together with various stacks such that you could imagine each token as it is parsed doing a limited amount of work at a time, very forthily.

Show thread

jcreed 1d ago

@edwinb Somewhere buried in here was the idea that traversal of a term while it is being initially typechecked would match very closely the traversal of the same term "executing" as the typechecker for its own arguments

Show thread

Taus

@jcreed @edwinb Whenever I see people doing dependent type checking in funny ways, I'm reminded of how the Dedukti folks used to do it: use Normalisation-by-Evaluation to compile into _Lua_ and run the code there. If it terminates, the code is type-correct, if not, the stack trace you get can tell you something about the type error.
They abandoned this approach, so it's unfortunately not easy to find information about it these days. Best I could find was these slides: https://www.cs.yale.edu/homes/qcar/data/dkpl-slides.pdf