Saturday, October 27, 2012
Linear Types with HOAS
I've recently been writing a tagless interpreter for the linear lambda calculus based on the pi calculus as in this paper. While there existed previously a typed interpreter for linear logic in haskell, it used DeBruijn indexes for the context. This isn't great if you'd actually like to use your language, and you can't convert into typed DeBruijn indexes from an untyped representation without template meta-programming, so this needed to be fixed. As it turns out, all DeBruijn indexes are really giving you here is the ability to wade through the context intelligently searching for the correct type. I've created a version where this is unnecessary. Instead type families are used to search for the instance of the variable in the context.