Institute of Cybernetics at TUT
Thursday, 27 October 2011, 14:00
Cybernetica Bldg (Akadeemia tee 21), room B101
Slides from the talk [pdf]
Abstract: In my last talk, I presented a record system that is implemented as a Haskell library. In this record system, record types contain so-called sorts that denote families of related types. Sorts can be all types of a single kind. However, there are situations where we would like to restrict the set of possible sorts for a record scheme. So we want to be able to specify subkinds that sorts must belong to.
In this talk, I am going to show how subkinds can be emulated in present-day Haskell. In my approach, subkinds are represented by types. That way, type polymorphism can be used to emulate subkind polymorphism. Subkind inhabitation is defined by type class instantiation. A difficulty with this approach is that Haskell's type classes are open, while kinds have to be closed. I will present a general technique for closing subkinds, which is based on higher-rank polymorphism.