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 < lemm...@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-cafe<http://www.haskell.org/mailman/listinfo/haskell-cafe> >
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe