29 May
2008
29 May
'08
7:29 a.m.
On Thu, May 29, 2008 at 9:51 AM, Kim-Ee Yeoh
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