[Haskell-cafe] Use distributivity proof in a simple example

[Adam Gundry]

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/