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 [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
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 <[hidden email]> 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 > [hidden email] > http://www.haskell.org/mailman/listinfo/haskell-cafe _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by Henning Thielemann
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 <[hidden email]> wrote:
_______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
On Tue, 2 Apr 2013, Daniel Peebles wrote: > 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. The answer to his post by Miguel Mitrofanov contains a caseNat that is exactly my 'switch'. I see I am four years late. _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by Henning Thielemann
Henning Thielemann wrote: > 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: You might like the following message posted in January 2005 http://www.haskell.org/pipermail/haskell-cafe/2005-January/008239.html (the whole discussion thread is relevant). In particular, the following excerpt -- data OpenExpression env r where -- Lambda :: OpenExpression (a,env) r -> OpenExpression env (a -> r); -- Symbol :: Sym env r -> OpenExpression env r; -- Constant :: r -> OpenExpression env r; -- Application :: OpenExpression env (a -> r) -> OpenExpression env a -> -- OpenExpression env r -- Note that the types of the efold alternatives are essentially -- the "inversion of arrows" in the GADT declaration above class OpenExpression t env r | t env -> r where efold :: t -> env -> (forall r. r -> c r) -- Constant -> (forall r. r -> c r) -- Symbol -> (forall a r. (a -> c r) -> c (a->r)) -- Lambda -> (forall a r. c (a->r) -> c a -> c r) -- Application -> c r shows the idea of the switch, but on more complex example (using higher-order rather than first-order language). That message has anticipated the tagless-final approach. _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
Free forum by Nabble | Edit this page |