Made a few small changes to the AST. Implementing a number of routines ahead of time until I figure out what to do with the type checker.
The type checker, as implemented in the bootstrap, is okay-ish. Not too shabby. The major difference between it and other functional type checker is that it records substitutions as type equivalences. I probably could speed it up already by factoring out different propositions. Moreover, I decided against using the gathered type equivalences to attribute the tree; I could do without recording substitutions.
Still, there's this thing about being able to typecheck cyclic types. Suppose, you have a type definition which unravels to the following:
t
/ \
/\
t
/ \
/\
.. ..
The type checker I now have "records" substitutions. It should therefore be able to prove type equivalences like the above by stating an equivalence, unfolding the type once, and using the postulated type. (Conceptually, the second "t" in the picture above becomes a cycle pointing to the first "t'.)
But that doesn't seem to be a problem in practice. To prove equivalences ML compilers simply unravel types a few times and use the definition to "close the cycle".
Ah well. First kindification I guess.
No comments:
Post a Comment