Write a Blog >>
ICFP 2016
Sun 18 - Sat 24 September 2016 Nara, Japan
Fri 23 Sep 2016 14:00 - 14:25 at Noh Theater - Monads Chair(s): Yukiyoshi Kameyama

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.

Fri 23 Sep

14:00 - 14:50: Haskell - Monads at Noh Theater
Chair(s): Yukiyoshi KameyamaUniversity of Tsukuba
haskellsymp-2016-papers14:00 - 14:25
Pablo BuirasChalmers University of Technology, Koen ClaessenChalmers University of Technology, Atze van der Ploeg
haskellsymp-2016-papers14:25 - 14:50