[Haskell-cafe] Use distributivity proof in a simple example
Marco Vassena
marco.vax91 at gmail.com
Tue Dec 2 15:40:40 UTC 2014
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/
More information about the Haskell-Cafe
mailing list