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?

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe