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

[Marco Vassena]

Hi Adam,

Thank you very much for your help and for the reference.

Singleton types were exactly what I needed.

Cheers,
Marco

On 02/dic/2014, at 09.27, Adam Gundry wrote:

> 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/