[Haskell-cafe] Witnessing lifted types?
eir at cis.upenn.edu
Mon Nov 25 16:01:57 UTC 2013
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! :)
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
> pure' :: WNat n -> a -> Vec n a
> pure' WZero _ = VecNil
> pure' (WSucc w) a = a ::: pure' w a
> (<*>) = app' witness
> 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
More information about the Haskell-Cafe