[Haskell-cafe] Extensionality principles for kinds?

[Richard Eisenberg]

The problem is that GHC doesn't do eta expansion for product types. See #7259, which won't be fixed by 7.10, as I would imagine a fair amount of theory needs to be done for this to be valid.

Luckily, you can do eta expansion manually yourself: either by requiring that the caller know the eta-expanded form (1) or by storing that knowledge in a GADT (2):

(1): Change the type signature of doubleEq to

> doubleEq :: (forall a b. f a -> f b -> Maybe (a :~: b))
>          -> Dbl f (TwiceVal a1 a2)
>          -> Dbl f (TwiceVal b1 b2)
>          -> Maybe (TwiceVal a1 a2 :~: TwiceVal b1 b2)

Here, I've dumped the unnecessary `forall`s (for my own sanity) and simply eta-expanded `a` and `b`. With this type, the original implementation of `doubleEq` type checks.

(2): Learn about the eta-expansion via a GADT pattern-match by changing `Dbl` to this:

> data Dbl (f :: k -> *) (tv :: Twice k) where
>   Dbl :: f a -> f b -> Dbl f (TwiceVal a b)

With this definition, when you pattern-match on the constructor `Dbl`, you also learn that `tv` really must be a `TwiceVal`. Then, the original type and definition for `doubleEq` type-check.

The trade-off between (1) and (2) is where the caller needs to know about the eta-expansions: in (1), it's the caller of `doubleEq` that must know it's passing in a real `TwiceVal`. In (2), it's the caller of the `Dbl` constructor that must know. I rather favor (2), as it allows you to pass the expansion knowledge around quite easily, and you don't need the `TwiceLeft` and `TwiceRight` type families.

Note that you need only solution (1) or (2), not both. (Though both works, too.)

I hope this helps!
Richard


On Nov 8, 2014, at 7:26 PM, Rob <rdockins at galois.com> wrote:

> Haskellers,
> 
> I've waded into some pretty deep waters, but I'm hoping there's a GHC type system wizard in here who can help me.  The following code fragment is extracted from something I've been working on involving some pretty fancy type-level programming.  I'm using GHC 7.8.3.
> 
> I've run into a problem where the typechecker refuses to believe that two types are equal; it seems to lack the necessary extensionality principles for lifted data kinds.  Basically (see below for definitions) I get into a contex where I know that (TwiceLeft a ~ TwiceLeft b) and (TwiceRight a ~ TwiceRight b), but the typechecker will not believe that (a ~ b).
> 
> Are there any tricks I can employ to make this code typecheck (using only safe operations)?  Bonus if it doesn't add any runtime cost.
> 
> Thanks,
>  Rob Dockins
> 
> 
> ====== code follows ======
> 
> {-# LANGUAGE DataKinds #-}
> {-# LANGUAGE PolyKinds #-}
> {-# LANGUAGE RankNTypes #-}
> {-# LANGUAGE TypeOperators #-}
> {-# LANGUAGE TypeFamilies #-}
> 
> import Data.Type.Equality
> 
> -- lifted kind (Twice k) consists of a pair of things of kind k
> data Twice k = TwiceVal k k
> 
> -- type family accessor functions for the Twice kind
> type family TwiceLeft (x::Twice k) :: k where
>  TwiceLeft (TwiceVal a b) = a
> 
> type family TwiceRight (x::Twice k) :: k where
>  TwiceRight (TwiceVal a b) = b
> 
> -- Double is already taken, use Dbl instead...
> data Dbl (f :: k -> *) (tv :: Twice k) = Dbl (f (TwiceLeft tv)) (f (TwiceRight tv))
> 
> -- This function doesn't typecheck...
> doubleEq :: forall (f:: k -> *)
>          . (forall (a::k) (b::k). f a -> f b -> Maybe (a :~: b))
>         -> (forall (a::Twice k) (b::Twice k). Dbl f a -> Dbl f b -> Maybe (a :~: b))
> doubleEq teq (Dbl x y) (Dbl z w) =
>   case teq x z of
>     Nothing -> Nothing
>     Just Refl ->
>       case teq y w of
>         Nothing -> Nothing
>         Just Refl -> Just Refl
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe