Andras Slemmer | 25 Nov 14:54 2013
Picon

Witnessing lifted types?

Hi, not sure whether this has been addressed before.
Basically the goal is to have a standardised way of witnessing lifted types (=simulating pattern matching on type indices).

A particular problem this would be useful for:
Given a standard natural-indexed vector (Vec n) provide an Applicative instance for it with n left polymorphic.
The issue is that we don't have a way of pattern matching on n, therefore we cannot implement pure/<*>. The way I addressed situations like this before was to have two Applicative instances, one for Vec Zero and one for Vec (Succ n), however I think there is a way to decouple this way of "pattern matching on types" by introducing a GADT:

data WNat n where
  WZero :: WNat Zero
  WSucc :: WNat n -> WNat (Succ n)

and a class

class WNatClass n where
  witness :: WNat n
instance WNatClass Zero where
  witness = WZero
instance (WNatClass n) => WNatClass (Succ n) where
  witness = WSucc witness

Now whenever we need to pattern match on a natural index we can just put a WNatClass restriction on it and pattern match on the automatically constructed witness.

For the Vec example:

instance (WNatClass n) => Applicative (Vec n) where
    pure = pure' witness
      where
        pure' :: WNat n -> a -> Vec n a
        pure' WZero _ = VecNil
        pure' (WSucc w) a = a ::: pure' w a
    (<*>) = app' witness
      where
        app' :: WNat n -> Vec n (a -> b) -> Vec n a -> Vec n b
        app' WZero _ _ = VecNil
        app' (WSucc w) (f ::: fs) (a ::: as) = f a ::: app' w fs as

We can also generalise this concept to any index type with PolyKinds, although I'm not 100% sure why it works in general:

class Construct (a :: k) where
  data Wit a :: *

class (Construct a) => Witness a where
  witness :: Wit a

The idea is that each instance of Construct will leave the type 'a' polymorphic and will only bind the kind 'k' and provide an indexed witness:

instance Construct (n :: Nat) where
  data Wit n where
    WZero :: Wit Zero
    WSucc :: Wit n -> Wit (Succ n)

and the Witness instances will be the same as with WNatClass.
We need two classes because one will define the witness type, the other will do the "pattern matching".

The part I don't understand is that together with the (n :: Nat) instance we can also have

instance Construct (a :: SomeOtherType) where ...

without triggering any 'overlapping' diagnostic, even though both instances are "fully polymorphic". I am assuming this is because internally the compiler adds a kind parameter to the class that disambiguates the instances? If so then I think this is a nice uniform way of handling lifted type witnesses. (The instances can be generated automatically too).

What do you think? Is there a better way of doing this? Is the decoupling even worth the trouble? Is the performance hit big compared to the explicit instance splitting?
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Richard Eisenberg | 25 Nov 17:01 2013

Re: Witnessing lifted types?

Hi Andras,

The road you're walking down leads to wonderful places, and your design ideas are right on. This general
direction of programming is addressed in my `singletons` library. That library uses Template Haskell to
generate a lot of the necessary definitions. So, you would just define plain old, non-GADT `Nat`, and you
get your `WNat` and `WNatClass` for free. And, it even uses the the same `Wit` data family -- I call it `Sing`.

If you want the cutting edge, you may want to look at the version of singletons on my github repo, at
github.com/goldfirere/singletons. That contains the (relatively stable) implementation of v. 0.9 of
the library -- the biggest (only?) missing piece is documentation. Feel free to email if you have
questions, though.

Even if you don't use the library, I can say that the design you have below works out fairly well, so just keep
going! :)

Richard

On Nov 25, 2013, at 8:54 AM, Andras Slemmer wrote:

> Hi, not sure whether this has been addressed before.
> Basically the goal is to have a standardised way of witnessing lifted types (=simulating pattern
matching on type indices).
> 
> A particular problem this would be useful for:
> Given a standard natural-indexed vector (Vec n) provide an Applicative instance for it with n left polymorphic.
> The issue is that we don't have a way of pattern matching on n, therefore we cannot implement pure/<*>. The
way I addressed situations like this before was to have two Applicative instances, one for Vec Zero and one
for Vec (Succ n), however I think there is a way to decouple this way of "pattern matching on types" by
introducing a GADT:
> 
> data WNat n where
>   WZero :: WNat Zero
>   WSucc :: WNat n -> WNat (Succ n)
> 
> and a class
> 
> class WNatClass n where
>   witness :: WNat n
> instance WNatClass Zero where
>   witness = WZero
> instance (WNatClass n) => WNatClass (Succ n) where
>   witness = WSucc witness
> 
> Now whenever we need to pattern match on a natural index we can just put a WNatClass restriction on it and
pattern match on the automatically constructed witness.
> 
> For the Vec example:
> 
> instance (WNatClass n) => Applicative (Vec n) where
>     pure = pure' witness
>       where
>         pure' :: WNat n -> a -> Vec n a
>         pure' WZero _ = VecNil
>         pure' (WSucc w) a = a ::: pure' w a
>     (<*>) = app' witness
>       where
>         app' :: WNat n -> Vec n (a -> b) -> Vec n a -> Vec n b
>         app' WZero _ _ = VecNil
>         app' (WSucc w) (f ::: fs) (a ::: as) = f a ::: app' w fs as
> 
> We can also generalise this concept to any index type with PolyKinds, although I'm not 100% sure why it
works in general:
> 
> class Construct (a :: k) where
>   data Wit a :: *
> 
> class (Construct a) => Witness a where
>   witness :: Wit a
> 
> The idea is that each instance of Construct will leave the type 'a' polymorphic and will only bind the kind
'k' and provide an indexed witness:
> 
> instance Construct (n :: Nat) where
>   data Wit n where
>     WZero :: Wit Zero
>     WSucc :: Wit n -> Wit (Succ n)
> 
> and the Witness instances will be the same as with WNatClass.
> We need two classes because one will define the witness type, the other will do the "pattern matching".
> 
> The part I don't understand is that together with the (n :: Nat) instance we can also have
> 
> instance Construct (a :: SomeOtherType) where ...
> 
> without triggering any 'overlapping' diagnostic, even though both instances are "fully polymorphic".
I am assuming this is because internally the compiler adds a kind parameter to the class that
disambiguates the instances? If so then I think this is a nice uniform way of handling lifted type
witnesses. (The instances can be generated automatically too).
> 
> What do you think? Is there a better way of doing this? Is the decoupling even worth the trouble? Is the
performance hit big compared to the explicit instance splitting?
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe <at> haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe

Gmane