It seems very similar to Ryan Ingram's post a few years back (pre-TypeNats): http://www.haskell.org/pipermail/haskell-cafe/2009-June/062690.html The main difference is that he introduces the "knowledge" about zero vs. suc as a constraint, and you introduce it as a parameter. In fact, his induction function (which is probably what I'd call it too) is almost identical to your switch. Anyway, it's cool stuff :) I don't have a name for it, but I enjoy it. On Tue, Apr 2, 2013 at 4:28 PM, Henning Thielemann < lemming@henning-thielemann.de> 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-cafehttp://www.haskell.org/mailman/listinfo/haskell-cafe