[Haskell-cafe] Use distributivity proof in a simple example
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?
More information about the Haskell-Cafe