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):
-- ghc -fglasgow-exts -c TypeLambda.hs
module TypeLambda where
{
class Fc a b | a -> b;
instance Fc Bool Int;
data F1 a = forall b. (Fc a b) => MkF1 b;
makeF1 :: Int -> F1 Bool;
makeF1 = MkF1;
getF1 :: F1 Bool -> Int;
getF1 (MkF1 i) = i;
data F2 a = MkF2 (forall b. (Fc a b) => b);
makeF2 :: Int -> F2 Bool;
makeF2 i = MkF2 i;
getF2 :: F2 Bool -> Int;
getF2 (MkF2 i) = i;
}
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:
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) = i
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 = MkF2 i
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:
Word8 -->> UArray Int Word8
Word16 -->> UArray Int Word16
(a -> b) -->> Array Int (a -> b)
It would be nice to hide the implementation and just expose some
type-constructor:
MyCollection Word8
MyCollection Word16
MyCollection (a -> b)
I believe this can't be done currently.
--
Ashley Yakeley, Seattle WA
_______________________________________________
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell
