Henning Thielemann | 2 Apr 22:28 2013
Picon

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
(Continue reading)

Richard Eisenberg | 2 Apr 23:09 2013

Re: 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 <lemming <at> 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
(Continue reading)

Daniel Peebles | 3 Apr 01:12 2013
Picon

Re: 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 <lemming <at> 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 <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Henning Thielemann | 3 Apr 01:30 2013
Picon

Re: 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 <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
oleg | 3 Apr 05:23 2013

Re: 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.

Gmane