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
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)) -
Luke Palmer-2 wrote:
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 :-)
God does not care about our computational difficulties. He infers
types emp^H^H^H
Andrew Coppin wrote:
So, after an entire day of boggling my mind over this, I have brought it
down to one simple example:
(id 'J', id True) -- Works perfectly.
\f - (f 'J', f True) -- Fails miserably.
Both expressions are obviously perfectly type-safe, and yet the type
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
On 5/27/08, Darrin Thompson [EMAIL PROTECTED] wrote:
On Tue, May 27, 2008 at 3:40 PM, Kim-Ee Yeoh [EMAIL PROTECTED] wrote:
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
