[Haskell-cafe] Re: Fun with type functions

3 Dec 2008

      Simon Peyton-Jones wrote:
...
can you tell us about the most persuasive, fun application
        you've encountered, for type families or functional dependencies?
I'm using them to provide witnesses to lenses.

Given two lenses on the same base type, I want to compare them, and if 
they're the same lens, know that they have the same view type.

   data Lens base view = MkLens
   {
     -- lensWitness :: ???,
     lensGet :: base -> view,
     lensPut :: base -> view -> base
   };

How do I compare "Lens base view1" and "Lens base view2", and match up 
view1 and view2?

The difficulty is that my witnesses are monomorphic, while a lens may be 
polymorphic. For instance, the lens corresponding to the "fst" function:

   fstLens :: Lens (a,b) a;
   fstLens = MkLens
   {
     lensGet = fst,
     lensPut = \(_,b) a -> (a,b)
   };

I only want to generate one open witness for fstLens, but what is its type?

This is where type functions come in. I have a type family TF, and a 
basic set of instances:

   type family TF tf x;

   data TFIdentity;
   type instance TF TFIdentity x = x;

   data TFConst a;
   type instance TF (TFConst a) x = a;

   data TFApply (f :: * -> *);
   type instance TF (TFApply f) x = f x;

   data TFMatch;
   type instance TF TFMatch (f a) = a;

   data TFMatch1;
   type instance TF TFMatch1 (f a b) = a;

   data TFCompose tf1 tf2;
   type instance TF (TFCompose tf1 tf2) x = TF tf1 (TF tf2 x);

I create a new witness type, that witnesses type functions:

   import Data.Witness;

   data TFWitness w x y where
   {
     MkTFWitness :: w tf -> TFWitness w x (TF tf x);
   };

   instance (SimpleWitness w) => SimpleWitness (TFWitness w x) where
   {
     matchWitness (MkTFWitness wtf1) (MkTFWitness wtf2) = do
     {
       MkEqualType <- matchWitness wtf1 wtf2;
       return MkEqualType;
     };
   };

So for my lens type, I want a witness for the type function from base to 
view:

   data Lens base view = MkLens
   {
     lensWitness :: TFWitness IOWitness base view,
     lensGet :: base -> view,
     lensPut :: base -> view -> base
   };

For our "fst" lens, I can now generate a witness for the function from 
"(a,b)" to "a".

   fstWitness :: IOWitness TFMatch1;
   fstWitness <- newIOWitness; -- language extension

   fstLens :: Lens (a,b) a;
   fstLens = MkLens
   {
     lensWitness = MkTFWitness fstWitness,
     lensGet = fst,
     lensPut = \(_,b) a -> (a,b)
   };

I can now compare two lenses like this:

   get1put2 :: Lens base view1 -> Lens base view2 -> base -> Maybe base;
   get1put2 lens1 lens2 b = do
   {
     MkEqualType <- matchWitness (lensWitness lens1) (lensWitness lens2);
     return (lensPut lens2 b (lensGet lens1 b));
   };

(Actually, I'm doing something a bit more useful than get1put2.)

-- 
Ashley Yakeley