Re: Re: [Haskell-cafe] Aren't type system extensions fun? [Further analysis]
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. -- Kim-Ee -- View this message in context: http://www.nabble.com/Aren%27t-type-system-extensions-fun--tp17479349p17531238.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: Re: [Haskell-cafe] Aren't type system extensions fun? [Further analysis]
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)) - ((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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: Re: [Haskell-cafe] Aren't type system extensions fun? [Further analysis]
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 ... uh, as He pleases. Anyway, the original point of it was semantic. Let's first explore the meaning of the most general type. Type functions give one answer, intersection types another. -- Kim-Ee (yeoh at cs dot wisc dot edu) -- View this message in context: http://www.nabble.com/Aren%27t-type-system-extensions-fun--tp17479349p17534701.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: Re: [Haskell-cafe] Aren't type system extensions fun? [Further analysis]
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 checker stubbornly rejects the second example. Clearly this is a flaw in the type checker. So what is the type of that second expression? You would think that (x - x) - (Char, Bool) as a valid type for it. But alas, this is not correct. The CALLER is allowed to choose ANY type for x - and most of possible choices wouldn't be type-safe. So that's no good at all! In a nutshell, the function being passed MAY accept any type - but we want a function that MUST accept any type. This excusiatingly subtle distinction appears to be the source of all the trouble. 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). For completeness' sake, let me just state that if universal quantification is like (x_t - ...), then existential quantification is like (x_t, ...). Andrew Coppin wrote: At this point, I still haven't worked out exactly why this hack works. Indeed, I've spent all day puzzling over this, to the point that my head hurts! I have gone through several theories, all of which turned out to be self-contradictory. My sympathies. You may find the haskell-cafe archive to be as useful as I have (search Ben Rudiak-Gould or Dan Licata). Having said that, I think you've done pretty well on your own. Andrew Coppin wrote: - Why can't the type system automatically detect where polymorphism is required? - Does the existence of these anomolies indicate that Haskell's entire type system is fundamentally flawed and needs to be radically altered - or completely redesigned? Well, give it a try! I'm sure I'm not the only one interested in your type inference experiments. Warning: they're addictive and may lead to advanced degrees and other undesirable side-effects. -- Kim-Ee -- View this message in context: http://www.nabble.com/Aren%27t-type-system-extensions-fun--tp17479349p17498362.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: Re: [Haskell-cafe] Aren't type system extensions fun? [Further analysis]
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? -- Darrin ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: Re: [Haskell-cafe] Aren't type system extensions fun? [Further analysis]
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 (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? Yes, it's easy, especially since there is only one total function of that type: id -- ryan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
