[Haskell-cafe] Witnessing lifted types?

[Andras Slemmer]

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?
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20131125/fe0c6ff7/attachment.html>