Untyping Cat: Mixing the Static World with the Dynamic World
Since I started work on converting Scheme to Cat, I have been spending a lot of time thinking about supporting dynamic code in Cat.
Well it turns out that the Cat type system is a bit special in that it is compositional. For example, giving two terms side-by-side, say “A B”, the type of the term can be achieved by computing the type of A and the type of B in parallel and then composing the results. If I understand correctly, this breaks from traditional Hindly-Milner type systems where the type of B is dependent on A (at least in the common presentation of such systems, I am unconvinced this is neccessarily true, but I am not a type theorist).
One way I can use the compositional property of the Cat type system is to allow untypable terms in-between typable terms. As horrible as this sounds at first to strong typing advocates, we can employ a frequently-used technique: punt type-checking until run-time. Clearly the untypable term requires full dynamic typing, but we can easily move from a type-safe mode into a un-typesafe mode, and back-again by using runtime executed type-safe coercion operators.
Unfortunately there is a down-side. Given a term: A B C where A and C are typed terms, and B is an untyped term the type of C may contain polymorphic types: universally quantified type variables. What this means is that C may be polymorphic over a type not known until run-time. This really isn’t that big of a deal, but it means that we don’t get all the optimization advantages of a type-checker. However, we can, if we choose, run a JIT compilation, to optimize the code on C, once we leave the untyped term B and know the type configuration of the stack.
This little trick will make it very easy for me to support translation from highly dynamic languages such as Scheme, but at the same time, still provide strong type-safety for translation from more static languages like C.