Adam Gundry writes:

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

Am I right in thinking that you can also use case unsafeCoerce Refl `asTypeOf` mapDist (toSingleton x) of .. to get the same proof, but without any runtime cost? It seems like this might be a nice middle ground. Of course there is a risk that the proof is just wrong, in which case things could awry. Maybe another option is to switch that line with -XCPP macros depending on whether or not you're in "production" mode. - Ollie

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/