[Haskell-cafe] Re: Fun with type functions

[Ashley Yakeley]

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