[Haskell-cafe] Re: checking types with type families

[oleg at okmij.org]

Simon Peyton-Jones wrote:

> Until now, no one has know how to combine fundeps and local constraints. 
> For example

>   class C a b | a->b where
>     op :: a -> b

>   instance C Int Bool where
>     op n = n>0

>   data T a where
>     T1 :: T a
>     T2 :: T Int

>   -- Does this typecheck?
>   f :: C a b => T a -> Bool
>   f T1 = True
>   f T2 = op 3

> The function f "should" typecheck because inside the T2 branch we know
> that (a~Int), and hence by the fundep (b~Bool).  But we have no formal
> type system for fundeps that describes this, and GHC's implementation
> certainly rejects it. 

At least for this particular example, a simple desugaring translation
makes even GHC 6.10.4 accept the example. We first desugar GADT
into the regular ADT and the EQ constraint (the process, as I understand,
already happens under the hood). We then make use of that constraint.

> {-# LANGUAGE GADTs, MultiParamTypeClasses, FunctionalDependencies #-}
>
> module F where
>
> class C a b | a->b where
>     op :: a -> b
>
> instance C Int Bool where
>     op n = n>0
>
> data EQ a b where
>     Refl :: EQ a a
>
> -- A primitive version of Leibniz substitution principle.
> cast :: EQ a b -> a -> b
> cast Refl x = x
>
> -- Original GADT
> -- data T a where
> --     T1 :: T a
> --     T2 :: T Int
>
> -- desugared version of T
> data TT a = TT1 | TT2 (EQ a Int)
>
> g :: C a b => TT a -> Bool
> g TT1 = True
> g (TT2 eq) = op (if False then cast eq undefined else 3)
>
> test1 = g (TT2 Refl)

It works.


Martin Sulzmann wrote:
> Type families and Fundeps are equivalent in expressive power and it's
> not too hard to show how to encode one in terms of the other.

As Martin himself said in the next paragraph of his message, the
equivalence claim has an exception: overlapping instances. Functional
dependencies do work with overlapping instances, but type families do
not. That issue has been noted just the other month on this list.

There is another exception. Let's consider type class C with a
functional dependency, and a seemingly equivalent type family F.

> {-# LANGUAGE TypeFamilies, MultiParamTypeClasses #-}
> {-# LANGUAGE RankNTypes, FunctionalDependencies #-}
>
> module F1 where
>
> class C a b | a->b
> instance C Int Bool
>
> type family F a :: *
> type instance F Int = Bool
>
>
> newtype N1 a = N1 (F a)
>
> n1 :: N1 Int -> Bool
> n1 (N1 x) = x
>
> t1 = n1 (N1 True)
>
> newtype N2 a = N2 (forall b. C a b => b)
>
> n2 :: N2 Int -> Bool
> n2 (N2 x) = x
>
> -- t2 = n2 ((N2 True) :: N2 Int)

The code type checks. It seems that for each piece of code using C we
can write an equivalent piece of code using F -- until we come to t1 and
t2. If we uncomment the last line, we get a type error

/tmp/c.hs:25:13:
    Couldn't match expected type `b' against inferred type `Bool'
      `b' is a rigid type variable bound by
          the polymorphic type `forall b. (C Int b) => b' at /tmp/c.hs:25:10
    In the first argument of `N2', namely `True'
    In the first argument of `n2', namely `((N2 True) :: N2 Int)'
    In the expression: n2 ((N2 True) :: N2 Int)

Although the type variable b must be Bool (since it is uniquely
determined by the functional dependency C Int b), GHC can't see that.