Hello Henning, That's a way of branching on type-level data that I haven't seen yet. I don't know of a name for it. However, if you find yourself needing to branch on type-level data, I encourage you to check out singleton types:

data Nat = Zero | Succ Nat -- this will be promoted data SNat :: Nat -> * where SZero :: SNat Zero SSucc :: SNat n -> SNat (Succ n)

append :: SNat n -> Vec n a -> Vec m a -> Vec (Add n m) a append SZero _empty x = x append (SSucc n') x y = case decons x of (a, as) -> cons a (append n' as y)

The key thing about singleton types is that they mirror any term-level case matching at the type level. So, in the first clause of `append`, GHC knows that n is Zero. In the second, GHC knows that n is Succ of n', for some n'. I think this should be able to do what you are doing with switch. If you think this sort of thing would be useful, you might find use in the 'singletons' package, available on Hackage. It's home page is here: http://www.cis.upenn.edu/~eir/packages/singletons/ The singletons package generates definitions like SNat, above, and also allows you to use singletons as class constraints, so you don't have to pass them around explicitly. Richard On Apr 2, 2013, at 4:28 PM, Henning Thielemann wrote:

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