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

[Daniel Peebles]

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<http://www.haskell.org/mailman/listinfo/haskell-cafe>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20130402/2e07253e/attachment.htm>