[Haskell-cafe] closed world instances, closed type families

[Richard Eisenberg]

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 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