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
