[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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] Re: Fun with type functions

[Toby Hutton]

On Thu, Nov 27, 2008 at 8:29 PM, Simon Peyton-Jones
[EMAIL PROTECTED] wrote:
 So this message is to ask you:

can you tell us about the most persuasive, fun application
you've encountered, for type families or functional dependencies?

I only just discovered functional dependencies a week or two ago, and
when it solved my problem it absolutely made my day.

I was reading 'Bananas, Lenses, etc.' and wanted to implement
paramorphic recursion with a type class.  My initial attempt:

class Paramorphic p where
   term :: p - Bool
   this :: p - a
   next ::: p - p

para :: (Paramorphic p) = t - (a - (p, t) - t) -p - t
para a f p | term p = a
   | otherwise = f (this p) (next p, para a f (next p))

instance Paramorphic Int where
term = (== 0)
this = id
next = subtract 1

This is broken, since 'a' in 'this' is loose.  Then I found multiple
class parameters:

class Paramorphic p a where
   ...

But 'a' was still too loose--para's type became

para :: (Paramorphic p a, Paramorphic p a1, Paramorphic p a2,
Paramorphic p a3) = t - (a1 - (p, t) - t) - p - t

But a fundep solved it for me:

class Paramorphic p a | p - a where
   ...

I could now pretty much do factorial and tails from the paper.

fact = para 1 (\a (_, b) - a * b)

instance Paramorphic [a] a where
term = null
this = head
next = tail

tails = para [[]] (\a (as, b) - (a : as) : b)

Not exactly a 'fun' example, but I was smiling for hours after
discovering this. :)

Toby.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe