[Haskell-cafe] Witnessing lifted types?

[Richard Eisenberg]

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