25 Nov 14:54 2013

## Witnessing lifted types?

Andras Slemmer <0slemi0 <at> gmail.com>

2013-11-25 13:54:33 GMT

2013-11-25 13:54:33 GMT

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:

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

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)

We need two classes because one will define the witness type, the other will do the "pattern matching".

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe <at> haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe