[Haskell-cafe] Re: Fun with type functions
Ashley Yakeley
ashley at semantic.org
Wed Dec 3 04:15:35 EST 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
More information about the Haskell-Cafe
mailing list