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

Isaac Dupree isaacdupree at charter.net
Tue May 27 17:47:13 EDT 2008

Darrin Thompson wrote:
> On Tue, May 27, 2008 at 3:40 PM, Kim-Ee Yeoh <a.biurvOir4 at asuhan.com> wrote:
>> Let's fill in the type variable: (x -> x) -> (Char, Bool) ==>
>> forall x. (x -> x) -> (Char, Bool) ==> x_t -> (x -> x) -> (Char, Bool),
>> where x_t is the hidden type-variable, not unlike the reader monad.
>> As you've pointed out, callER chooses x_t, say Int when
>> passing in (+1) :: Int -> Int, which obviously would break
>>  \f -> (f 'J', f True).
>> What we want is the callEE to choose x_t since callEE needs to
>> instantiate x_t to Char and Bool. What we want is
>>  (x_t -> x -> x) -> (Char, Bool).
>> But that's just
>>  (forall x. x -> x) -> (Char, Bool).
> Nice. That's the first time any of this really made sense to me. Is it
> possible to construct valid argument for that function?

agree, the types-are-arguments-too makes thinking about how it works A 
LOT clearer... and it's actually what GHC's intermediate Core language 
does.  It's too bad there's no way in the language syntax to make that 
interpretation clearer.  (That's a subset of explicit dependent types -- 
explicitness is opposite type inference, not static vs. dependentness.)


More information about the Haskell-Cafe mailing list