[Haskell-cafe] closed world instances, closed type families
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
Re: [Haskell-cafe] closed world instances, closed type families
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 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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] closed world instances, closed type families
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-cafehttp://www.haskell.org/mailman/listinfo/haskell-cafe
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] closed world instances, closed type families
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 Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] closed world instances, closed type families
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 Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
