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: [Haskell-cafe] Aren't type system extensions fun? [Further analysis]
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 argument: foo :: forall m :: * - * . (forall a. a - m a) - (m Char, m Bool) This seems to be Haskell+extensions, but note that m above is meant to be an arbitrary type-level function, and not a type constructor (in general). So, I am not surprised if undecidability issues arise in type checking/inference. :-) 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. Regards, Zun. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Aren't type system extensions fun? [Further analysis]
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, so it becomes a forall because (-) is contravariant on its 1st argument: foo :: forall m :: * - * . (forall a. a - m a) - (m Char, m Bool) This seems to be Haskell+extensions, but note that m above is meant to be an arbitrary type-level function, and not a type constructor (in general). So, I am not surprised if undecidability issues arise in type checking/inference. :-) Type *checking* is still decidable (System Fw is sufficiently powerful to model these types) but type inference now needs higher order unification, which indeed is undecidable. 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 solving the halting problem. Type checking however is decidable, but expensive. Edsko ___ 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: [Haskell-cafe] Aren't type system extensions fun? [Further analysis]
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 solving the halting problem. Type checking however is decidable, but expensive. 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. But why, when we can just use standard tuples instead? foo :: (Char - a , Bool - b) - (a,b) Admittedly this function is isomorphic to type (Char,Bool)... but that's a different issue, with the arbitrariness of our choice of example function. -Isaac ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Aren't type system extensions fun? [Further analysis]
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 fromBool :: Bool - b or some more clever thing? If this can be encoded with method-less classes, I would be quite interested in knowing how. But why, when we can just use standard tuples instead? foo :: (Char - a , Bool - b) - (a,b) This makes the class dictionary explicit. Alas, IIUC we lost type erasure (does that still hold with intersection types?) in this implementation. Zun. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Aren't type system extensions fun? [Further analysis]
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. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Aren't type system extensions fun? [Further analysis]
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 Oops: i meant something like class C x a b | x - a,b where fromChar :: x - Char - a fromBool :: x - Bool - b no... let me figure out what I meant. Just somehow to have a single function that takes an argument of two different types without completely ignoring it. class Arg a where whatYouPass :: a - Something instance Arg Char where whatYouPass = ... instance Arg Bool where whatYouPass = ... Then (foo whatYouPass) :: (Something, Something). Or if it was class Arg a where whatYouPass :: a - a then (foo whatYouPass) :: (Char, Bool). And I'm sure there are ways to make the return type different if you want to think about FDs etc. Zun. ___ 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
