Darrin Thompson wrote:
On Tue, May 27, 2008 at 3:40 PM, Kim-Ee Yeoh <[EMAIL PROTECTED]> 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.)
-Isaac
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
