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)) -
Kim-Ee Yeoh wrote:
How about
foo :: (exists. m :: * - *. forall a. a - m a) - (m Char, m Bool)
Thank you: I had actually thought about something like that.
First, the exists above should actually span over the whole type, so it
becomes a forall because (-) is contravariant on its 1st
On Thu, May 29, 2008 at 01:44:24PM +0200, Roberto Zunino wrote:
Kim-Ee Yeoh wrote:
How about
foo :: (exists. m :: * - *. forall a. a - m a) - (m Char, m Bool)
Thank you: I had actually thought about something like that.
First, the exists above should actually span over the whole type,
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
Another valid type for foo can be done AFAICS with intersection types:
foo :: (Char - a /\ Bool - b) - (a,b)
But I can not comment about their inference, or usefulness in practice.
Again, undecidable :) In fact, I believe that an inference algorithm for
intersection types is equivalent to
Isaac Dupree wrote:
foo :: (Char - a /\ Bool - b) - (a,b)
a.k.a. find some value that matches both Char-a and Bool-b for some a
and b. Could use type-classes to do it.
Uhmm... you mean something like (neglecting TC-related issues here)
class C a b where
fromChar :: Char - a
Roberto Zunino wrote:
Uhmm... you mean something like (neglecting TC-related issues here)
class C a b where
fromChar :: Char - a
fromBool :: Bool - b
Oops: i meant something like
class C x a b | x - a,b where
fromChar :: x - Char - a
fromBool :: x - Bool - b
Zun.
foo :: (Char - a /\ Bool - b) - (a,b)
a.k.a. find some value that matches both Char-a and Bool-b for some a and b. Could use type-classes to do it.
Uhmm... you mean something like (neglecting TC-related issues here)
class C a b where
fromChar :: Char - a
fromBool :: Bool - b
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
12 matches
Mail list logo
