[Haskell-cafe] closed world instances, closed type families

[Henning Thielemann]

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
    Append m a n =
       Append {runAppend :: Vec n a -> Vec m a -> Vec (Add n m) a}

type family Add n m :: *
type instance Add Zero m = m
type instance Add (Succ n) m = Succ (Add n m)

append :: Nat n => Vec n a -> Vec m a -> Vec (Add n m) a
append =
    runAppend $
    switch
       (Append $ \_empty x -> x)
       (Append $ \x y ->
           case decons x of
              (a,as) -> cons a (append as y))


decons :: Vec (Succ n) a -> (a, Vec n a)

cons :: a -> Vec n a -> Vec (Succ n) a



The technique reminds me on GADTless programming. Has it already a name?