On Thu, May 29, 2008 at 9:51 AM, Kim-Ee Yeoh <[EMAIL PROTECTED]> wrote: > Roberto Zunino-2 wrote: >> >> Alas, for code like yours: >> foo = \f -> (f 'J', f True) >> >> there are infinite valid types too: >> (forall a. a -> Int) -> (Int, Int) >> (forall a. a -> Char)-> (Char, Char) >> (forall a. a -> (a,a)) -> ((Char,Char),(Bool,Bool)) >> ... >> >> and it is much less clear if a "best", most general type exists at all. >> > > How about > foo :: (exists. m :: * -> *. forall a. a -> m a) -> (m Char, m Bool) > > Not quite Haskell, but seems to cover all of the examples you gave.
You have now introduced a first-class type function a la dependent types, which I believe makes the type system turing complete. This does not help the decidability of inference :-) Luke _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe