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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe