[Haskell-cafe] Aren't type system extensions fun? [Further analysis]

[Luke Palmer]

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