2 Apr 22:28 2013

## closed world instances, closed type families

Henning Thielemann <lemming <at> henning-thielemann.de>

2013-04-02 20:28:19 GMT

2013-04-02 20:28:19 GMT

Recently I needed to define a class with a restricted set of instances. After some failed attempts I looked into the DataKinds extension and in "Giving Haskell a Promotion" I found the example of a new kind Nat for type level peano numbers. However the interesting part of a complete case analysis on type level peano numbers was only sketched in section "8.4 Closed type families". Thus I tried again and finally found a solution that works with existing GHC extensions: data Zero data Succ n class Nat n where switch :: f Zero -> (forall m. Nat m => f (Succ m)) -> f n instance Nat Zero where switch x _ = x instance Nat n => Nat (Succ n) where switch _ x = x That's all. I do not need more methods in Nat, since I can express everything by the type case analysis provided by "switch". I can implement any method on Nat types using a newtype around the method which instantiates the f. E.g. newtype(Continue reading)