Fundep & Datatype Request

[Simon Peyton-Jones]

Another tricky one.  There are at least two difficulties.

1.  Consider the simpler function
	foo :: Fc Bool b =3D> [b] -> Int
	foo (x:xs) =3D x
Since b must be Int, you might argue that this function is OK, but GHC
rejects it because it unifies the signature type variable b.  This is a
"legitimate" constraint on 'b'.  The question is how to distinguish the
legitimate constraints on b from the illegitimate ones.  In principle,
not too hard -- just "improve" the type signature, but GHC translates
the whole thing to System F, so it really will pass a type parameter for
'b'...   Maybe it can be done, but I feel queasy about it.

2. Suppose we have

  makeF3 i =3D [MkF2 i, ...., (undefined :: F2 Bool)]

When type-checking MkF2 it's less obvious that the result will be an (F2
Bool) than it was in your example.  So perhaps type-correctness depends
on the "pushing-types-inwards" idea. Well, ok, that's what I do for
higher-rank types, but we'd need to precisely say what programs are
accepted and what programs are not.



At the moment I'm somewhat resisting making further ad-hoc
"improvements" to GHC's type-inference algorithm, even though it falls
short in various ways, because I keep hoping someone is going to come up
with a simple non-ad-hoc story that will address these various issues in
a more systematic way.

Simon

| -----Original Message-----
| From: haskell-admin@haskell.org [mailto:haskell-admin@haskell.org] On
Behalf Of Ashley Yakeley
| Sent: 05 September 2003 01:24
| To: haskell@haskell.org
| Subject: Fundep & Datatype Request
|=20
| OK, this is an issue I have raised before I think, but I don't
remember
| what the opinion on it was. The following doesn't compile with ghc
| -fglasgow-exts (or Hugs -98):
|=20
| -- ghc -fglasgow-exts -c TypeLambda.hs
| module TypeLambda where
|     {
|     class Fc a b | a -> b;
|=20
|     instance Fc Bool Int;
|=20
|     data F1 a =3D forall b. (Fc a b) =3D> MkF1 b;
|=20
|     makeF1 :: Int -> F1 Bool;
|     makeF1 =3D MkF1;
|=20
|     getF1 :: F1 Bool -> Int;
|     getF1 (MkF1 i) =3D i;
|=20
|     data F2 a =3D MkF2 (forall b. (Fc a b) =3D> b);
|=20
|     makeF2 :: Int -> F2 Bool;
|     makeF2 i =3D MkF2 i;
|=20
|     getF2 :: F2 Bool -> Int;
|     getF2 (MkF2 i) =3D i;
|     }
|=20
| Clearly makeF1 and getF2 are OK. But I claim getF1 and makeF2 should
| compile, since the type inside either an "F1 Bool" or an "F2 Bool"
must
| always be an Int. Instead I get this:
|=20
|=20
| TypeLambda.hs:14:
|     Inferred type is less polymorphic than expected
|         Quantified type variable `b' is unified with `Int'
|     When checking an existential match that binds
|         i :: b
|     and whose type is F1 Bool -> Int
|     In the definition of `getF1': getF1 (MkF1 i) =3D i
|=20
| TypeLambda.hs:19:
|     Cannot unify the type-signature variable `b' with the type `Int'
|         Expected type: b
|         Inferred type: Int
|     In the first argument of `MkF2', namely `i'
|     In the definition of `makeF2': makeF2 i =3D MkF2 i
|=20
|=20
| So why is this useful? Because you can do some form of type-lambda
with
| it. For instance, you might have some system of collection types:
|=20
|   Word8     -->>  UArray Int Word8
|   Word16    -->>  UArray Int Word16
|   (a -> b)  -->>  Array Int (a -> b)
|=20
| It would be nice to hide the implementation and just expose some
| type-constructor:
|=20
|   MyCollection Word8
|   MyCollection Word16
|   MyCollection (a -> b)
|=20
| I believe this can't be done currently.
|=20
| --
| Ashley Yakeley, Seattle WA
|=20
| _______________________________________________
| Haskell mailing list
| Haskell@haskell.org
| http://www.haskell.org/mailman/listinfo/haskell