[Haskell-cafe] Use distributivity proof in a simple example
Marco Vassena
marco.vax91 at gmail.com
Tue Dec 2 01:28:48 UTC 2014
My GADT data type is indexed over type level list.
data DF (xs :: [ * ]) where
Empty :: DF []
Single :: a -> DF '[ a ]
Cons :: DF xs -> DF ys -> DF (Append xs ys)
Append is a type family that append two type level lists:
type family Append (xs :: [ * ]) (ys :: [ * ]) :: [ * ] where
Append '[] ys = ys
Append (x ': xs) ys = x ': Append xs ys
Map is a type level map:
type family Map (f :: * -> *) (xs :: [ * ]) :: [ * ] where
Map f '[] = '[]
Map f (x ': xs) = f x ': Map f xs
Now I want to write a function that wraps all the component in Single in a list:
wrap :: DF xs -> DF (Map [] xs)
wrap Empty = Empty
wrap (Single a) = Single [ a ]
wrap (Cons x y) = Cons (wrap x) (wrap y) -- Type Error
The type-checker doesn't know anything about distributivity:
Could not deduce (Append (Map [] xs) (Map [] ys) ~ Map [] zs)
from the context (zs ~ Append xs ys)
I managed to prove this property by induction on the first type level list.
class MapDist xs where
mapDist :: (zs ~ Append xs ys) => Proxy xs -> Proxy ys -> Append (Map [] xs) (Map [] ys) :~: Map [] zs
instance MapDist '[] where
mapDist Proxy Proxy = Refl
tailP :: Proxy (x ': xs) -> Proxy xs
tailP _ = Proxy
instance MapDist xs => MapDist (x ': xs) where
mapDist p1 p2 =
case mapDist (tailP p1) p2 of
Refl -> Refl
I have adjusted wrap as follows:
toProxy :: DataFormat xs -> Proxy xs
toProxy _ = Proxy
wrap (Cons x y) =
let p1 = toProxy x
p2 = toProxy y in
case mapDist p1 p2 of
Refl -> Cons (wrap x) (wrap y)
The problem now is that MapDist xs is not in the context.
Adding it to the Cons constructor in the GADT definition does not solve the problem:
Could not deduce (MapDist (Map [] xs)) ...
How can I solve this issue?
Clearly the two instances of MapDist cover all possible cases, and therefore it should be possible
to use it for any list xs.
I tried avoiding the type class MapDist with a normal function:
proof :: forall xs ys zs . Append xs ys ~ zs =>
Proxy xs -> Proxy ys -> Proxy zs ->
Append (Map [] xs) (Map [] ys) :~: Map [] zs
However here I have no mean to distinguish the base case ('[]) from
the inductive case (x ': xs), thus I cannot complete the proof.
Do you have any idea, suggestion or workaround for this kind of situations?
Cheers,
Marco
More information about the Haskell-Cafe
mailing list