I'm studying optimal implementations of the λ-calculus. There is a particular subset of lambda terms that is very efficient. It corresponds to the type system of Elementary Affine Logic with fixed points. In order to test my implementations of that algorithm, I have to write moderately complex terms on that system. This is difficult without a infrastructure. I have to use the untyped lambda calculus and then manually add the types; no checking, unification, no type errors.
One idea would be to write programs in Haskell - taking benefit from its mature type-checker - and then translate to EAL. Unfortunately, there is a mismatch between System-Fw and EAL. For example, you can't express Scott-encoded ADTs in Haskell without newtype, due to the lack of a type-level fix. Moreover, Haskell is a complex language, and writing a Haskell->EAl compiler would not be trivial.
Is there any quick/dirty way to get a working type checker/inferencer/unifier for that system - or at least something close enough - without having to program it all myself?
Probably the quickest and easiest way is to embed your system into Haskell as an EDSL. The finally, tagless approach may be ideal and there's an example of encoding a linear type system with it. In particular, I'd recommend using the HOAS variation by Jeff Polakow. This will give you syntax like:
*Main> :t eval $ llam $ \x -> add x (int 1)
eval $ llam $ \x -> add x (int 1) :: Int -<> Int
which isn't too terrible. One aspect of the finally, tagless approach is that you can can have multiple interpretations for the same term, so you can have an interpretation that translates the term to some AST representing EAL, or have an interpretation that performs some additional typechecking if you aren't able to capture all of it in Haskell's type system.
Collected from the Internet
Please contact [email protected] to delete if infringement.
Comments