Please log in to watch this conference skillscast.
The idea of this talk is to take a somewhat unusual route to dependent types, not via type-theory, but rather by trying to model a "topos" in Haskell. A "topos" is a special kind of category which is basically a theory of sets that makes it possible to do most of the usual constructions from set theory. In particular, one gets quotient types, subtypes, extensional equality for functions etc. The "protop" library models such (elementary) topoi in Haskell and can compile topos objects to Haskell types and topos morphisms to Haskell functions.
YOU MAY ALSO LIKE:
Lightning Talk: Protop--Dependent Types through Topoi