The Key monad: type-safe unconstrained dynamic typing
- 8 September 2016
- conference paper
- conference paper
- Published by Association for Computing Machinery (ACM) in Proceedings of the 9th International Symposium on Haskell
- p. 146-157
- https://doi.org/10.1145/2976002.2976008
Abstract
We present a small extension to Haskell called the Key monad. With the Key monad, unique keys of different types can be created and can be tested for equality. When two keys are equal, we also obtain a concrete proof that their types are equal. This gives us a form of dynamic typing, without the need for Typeable constraints. We show that our extension allows us to safely do things we could not otherwise do: it allows us to implement the ST monad (inefficiently), to implement an embedded form of arrow notation, and to translate parametric HOAS to typed de Bruijn indices, among others. Although strongly related to the ST monad, the Key monad is simpler and might be easier to prove safe. We do not provide such a proof of the safety of the Key monad, but we note that, surprisingly, a full proof of the safety of the ST monad also remains elusive to this day. Hence, another reason for studying the Key monad is that a safety proof for it might be a stepping stone towards a safety proof of the ST monad.Keywords
This publication has 12 references indexed in Scilit:
- Embedding effect systems in HaskellPublished by Association for Computing Machinery (ACM) ,2014
- Simple and compositional reification of monadic embedded languagesPublished by Association for Computing Machinery (ACM) ,2013
- Abstract syntax graphs for domain specific languagesPublished by Association for Computing Machinery (ACM) ,2013
- Functional programming with structured graphsPublished by Association for Computing Machinery (ACM) ,2012
- Idioms are Oblivious, Arrows are Meticulous, Monads are PromiscuousElectronic Notes in Theoretical Computer Science, 2011
- Unembedding domain-specific languagesPublished by Association for Computing Machinery (ACM) ,2009
- Parametric higher-order abstract syntax for mechanized semanticsPublished by Association for Computing Machinery (ACM) ,2008
- Monadic encapsulation of effects: a revised approach (extended version)Journal of Functional Programming, 2001
- Lazy functional state threadsPublished by Association for Computing Machinery (ACM) ,1994
- Re: ElliottAnnals of Plastic Surgery, 1988