[Haskell-cafe] Use distributivity proof in a simple example
Adam Gundry
adam at well-typed.com
Tue Dec 2 08:27:08 UTC 2014
Hi Marco,
I think typeclasses are a bit of a red herring here: the problem, as you
observed, is that it isn't possible to write a useful term of type
proof :: forall xs ys zs . Append xs ys ~ zs
=> Proxy xs -> Proxy ys -> Proxy zs
-> Append (Map [] xs) (Map [] ys) :~: Map [] zs
because the runtime behaviour of proof (i.e. the program that constructs
the witness to the equality) must depend on xs. (With typeclasses, the
unsolved constraint of type `MapDist xs` amounts to needing this
argument to be passed at runtime; having the two cases covered by class
instances isn't enough.)
The nice way to solve this problem would be to use a dependent product
(pi-type), which would allow a single argument to be used both in types
(like forall) and at runtime (like normal functions). Unfortunately,
Haskell doesn't support pi-types (yet...) but we can fake them with a
standard trick known as "singleton types", like this:
-- The singleton type of lists, which allows us to take a list as a
-- term-level and a type-level argument at the same time (although
-- we're not interested in the elements here, only the structure)
data SList xs where
SNil :: SList '[]
SCons :: SList xs -> SList (x ': xs)
-- Now mapDist takes xs at runtime but ys/zs only at compile time
mapDist :: zs ~ Append xs ys
=> SList xs -> proxy ys
-> Append (Map [] xs) (Map [] ys) :~: Map [] zs
mapDist SNil _ = Refl
mapDist (SCons l) p = apply Refl (mapDist l p)
-- Connect term-level and type-level list append
append :: SList xs -> SList ys -> SList (Append xs ys)
append SNil ys = ys
append (SCons xs) ys = SCons (append xs ys)
-- Convert your DF type into a list
toSingleton :: DF xs -> SList xs
toSingleton Empty = SNil
toSingleton (Single _) = SCons SNil
toSingleton (Cons xs ys) = append (toSingleton xs) (toSingleton ys)
-- Now it's easy to define wrap
wrap :: DF xs -> DF (Map [] xs)
wrap Empty = Empty
wrap (Single a) = Single [ a ]
wrap (Cons x y) = case mapDist (toSingleton x) y of
Refl -> Cons (wrap x) (wrap y)
If you're interested in this technique, Richard and Jan's excellent
"singletons" library [1] and accompanying paper take it much further.
Hope this helps,
Adam
[1] http://hackage.haskell.org/package/singletons
On 02/12/14 01:28, Marco Vassena wrote:
> 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
--
Adam Gundry, Haskell Consultant
Well-Typed LLP, http://www.well-typed.com/
More information about the Haskell-Cafe
mailing list