RE: [Haskell-cafe] Re: Aren't type system extensions fun? [Further analysis]
Andrew writes | I have complete confidence that whoever wrote the GHC manual knew | exactly what they meant. I am also fairly confident that this was the | same person who implemented and even designed this particular feature. | And that they probably have an advanced degree in type system theory. I, | however, do not. So if in future the GHC manual could explain this in | less opaque language, that would be most appreciated. :-} As the person who wrote the offending section of the GHC user manual (albeit lacking a qualification of any sort in type theory), I am painfully aware of its shortcomings. Much of the manual is imprecise, and explains things only by examples. The wonder is that it apparently serves the purpose for many people. Nevertheless, the fact is that it didn't do the job for Andrew, at least not first time around. After some useful replies to his email, he wrote | Thank you for coming up with a clear and comprehensible answer. I would very much welcome anyone who felt able to improve on the text in the manual, even if it's only a paragraph or two. If you stub your toe on the manual, once you find the solution, take a few minutes to write the words you wish you had read to begin with, and send them to me. Meanwhile, Andrew, I recommend the paper Practical type inference for arbitrary rank types, which is, compared to the user manual at least, rather carefully written. Simon ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Aren't type system extensions fun? [Further analysis]
Kim-Ee Yeoh [EMAIL PROTECTED] wrote: 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. This begs the question: Can God come up with a type He doesn't understand? The answer, it seems, is Mu. -- (c) this sig last receiving data processing entity. Inspect headers for past copyright information. All rights reserved. Unauthorised copying, hiring, renting, public performance and/or broadcasting of this signature prohibited. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Aren't type system extensions fun? [Further analysis]
Andrew Coppin wrote:
(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.
When you type some expression such as
\x - x
you have to choose among an infinite number of valid types for it:
Int - Int
Char - Char
forall a . a - a
forall a b . (a,b) - (a,b)
...
Yet the type inference is smart enough to choose the best one:
forall a. a - a
because this is the most general type.
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.
You might have a preference to type it so that
foo :: (forall a . a-a) - (Char,Bool)
foo id == ('J',True) :: (Char,Bool)
but one could also require the following, similarly reasonable code to work:
foo :: (forall a. a - (a,a)) - ((Char,Char),(Bool,Bool))
foo (\y - (y,y)) == (('J','J'),(True,True))
:: ((Char,Char),(Bool,Bool))
And devising a type inference system allowing both seems to be quite
hard. Requiring a type annotation for these not-so-common code snippets
seems to be a fair compromise, at least to me.
Regards,
Zun.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Aren't type system extensions fun? [Further analysis]
andrewcoppin: Gleb Alexeyev wrote: foo :: (forall a . a - a) - (Bool, String) foo g = (g True, g bzzt) 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. I'm sorry you are still confused, Andrew. This is documented rather nicely in section 8.7.4.2 of the GHC user's guide. In particularly, you'll want to not ethat arbitrary rank type inference is undecidable, so GHC imposes a simple rule requiring you to annotate those polymorphic parameters of higher rank you want. See here http://www.haskell.org/ghc/docs/latest/html/users_guide/other-type-extensions.html#id408394 Read this carefully, and then read the references. Interestingly, if you throw in the undocumented forall keyword, everything magically works: (forall x. x - x) - (Char, Bool) Obviously, the syntax is fairly untidy. And the program is now not valid Haskell according to the written standard. And best of all, the compiler seems unable to deduce this type automatically either. Please read the above link. In particular, pay attention to the word undecidable. Reading and comprehending Odersky and Laufer's paper, Putting type annotations to work, will explain precisely why you're butting your head up against deciability. -- Don ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Aren't type system extensions fun? [Further analysis]
2008/5/27 Andrew Coppin [EMAIL PROTECTED]: Gleb Alexeyev wrote: foo :: (forall a . a - a) - (Bool, String) foo g = (g True, g bzzt) 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. No, this is a flaw in the type inferencer, but simply adding the Rank-N type to our type system makes type inference undecidable. I would argue against the obviously perfectly type-safe too since most type system don't even allow for the second case. 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! None of the possible choice would be type-safe. This type means : whatever the type a, function of type (a - a) to a pair (Char, Bool) But the type a is unique while in the body of your function, a would need to be two different types. Interestingly, if you throw in the undocumented forall keyword, everything magically works: (forall x. x - x) - (Char, Bool) Obviously, the syntax is fairly untidy. And the program is now not valid Haskell according to the written standard. And best of all, the compiler seems unable to deduce this type automatically either. As I said, the compiler can't deduce this type automatically because it would make type inference undecidable. 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. So far, the only really plausible theory I have been able to come up with is this: Rank-N type aren't a hack, they're perfectly understood and fit nicely into the type system, their only problem is type inference. yada yada, complicated theory... cut What you don't seem to understand is that (x - x) - (Char, Bool) and (forall x. x - x) - (Char, Bool) are two very different beasts, they aren't the same type at all ! Taking a real world situation to illustrate the difference : Imagine you have different kind of automatic washer, some can wash only wool while others can wash only cotton and finally some can wash every kind of fabric... You want to do business in the washing field but you don't have a washer so you publish an announce : If your announce say whatever the type of fabric x, give me a machine that can wash x and all you clothes and I'll give you back all your clothes washed, the customer won't be happy when you will give him back his wool clothes that the cotton washing machine he gave you torn to shreds... What you really want to say is give me a machine that can wash any type of fabric and your clothes and I'll give you back your clothes washed. The first announce correspond to (x - x) - (Char, Bool), the second to (forall x. x - x) - (Char, Bool) - Why are top-level variables and function arguments treated differently by the type system? They aren't (except if you're speaking about the monomorphism restriction and that's another subject entirely). - Why do I have to manually tell the type checker something that should be self-evident? Because it isn't in all cases to a machine, keep in mind you're an human and we don't have real IA just yet. - Why is this virtually never a problem in real Haskell programs? Because we seldom needs Rank-2 polymorphism. - Is there ever a situation where the unhacked type system behaviour is actually desirably? Almost everytime. Taking a simple example : map If the type of map was (forall x. x - x) - [a] - [a], you could only pass it id as argument, if it was (forall x y. x - y) - [a] - [b], you couldn't find a function to pass to it... (No function has the type a - b) - Why can't the type system automatically detect where polymorphism is required? It can and does, it can't detect Rank-N (N 1) polymorphism because it would be undecidable but it is fine with Rank-1 polymorphism (which is what most people call polymorphism). - 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? Maybe this should suggest to you that it is rather your understanding of the question that is flawed... Haskell's type system is a fine meshed mechanism that is soundly grounded in logic and mathematics, it is rather unlikely that nobody would have noted the problem if it was so important... -- Jedaï ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org
Re: [Haskell-cafe] Re: Aren't type system extensions fun? [Further analysis]
Chaddaï Fouché wrote: - Why are top-level variables and function arguments treated differently by the type system? They aren't In a sense, they are. id :: (forall a. a - a) useId :: (forall a. a - a) - (Int,Bool) brokenUseId :: (forall a. (a - a) - (Int,Bool)) brokenUseId :: (a - a) - (Int,Bool) Note that polymorphic variables in function argument types scope over the function results too by default. And that's a good thing. Otherwise, id :: a - a would be understood as brokenId :: (forall a. a) - (forall a. a) which is not at all intended (id specialized to _|_ values only). Basically, you only want higher-rank types in Haskell when you know what you're doing: due to parametric polymorphism it is less often useful to apply an argument function to, e.g., both Int and Bool than you might find in Python, for example. In Haskell, more often you would just take two functions as arguments e.g. useFunctions :: (Int - Int) - (Bool - Bool) - (Int,Bool) or more interestingly, let's make the caller be able to choose any kind of number: useFunctions2 :: (Num a) = (a - a) - (Bool - Bool) - (a,Bool) a.k.a. useFunctions2 :: forall a. (Num a) = (a - a) - (Bool - Bool) - (a,Bool) -Isaac ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: 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! All possible choices wouldn't be type-safe, so its even worse. 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. Interestingly, if you throw in the undocumented forall keyword, everything magically works: (forall x. x - x) - (Char, Bool) But you have to do it right. forall x . (x - x) - (Char, Bool) is equivalent to the version without forall, and does you no good. (Note the parentheses to see why these two types are different). So there lies no magic in mentioning forall, but art in putting it in the correct position. The key problem seems to be that the GHC manual assumes that anybody reading it will know what universal quantification actually means. Unfortunately, neither I nor any other human being I'm aware of has the slightest clue what that means. A quick search on that infallable reference [sic] Wikipedia yields several articles full of dense logic theory. Trying to learn brand new concepts from an encyclopedia is more or less doomed from the start. As far as I can comprehend it, we have existential quantification = this is true for SOMETHING universal quantification = this is true for EVERYTHING Quite how that is relevant to the current discussion eludes me. Your MUST accept any type is related to universal quantification, and your MAY accept any type is related to existential quantification: This works for EVERYTHING, so it MUST accept any type. This works for SOMETHING, so it accepts some unknown type. Quantification is the logic word for abstracting by introducing a name to filled with content later. For example, in your above paragraph you wanted to tell us that no human being you are aware of has the slightest clue what universal quantification means. You could have done so by enumerating all human beings you are aware of. Instead, you used universal quantification: for all HUMAN BEING, HUMAN BEING has no clue. (shortened to not overcomplicate things, HUMAN BEING is the name here). Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Aren't type system extensions fun? [Further analysis]
Warning for Andrew: this post explains a new-to-you typed lambda calculus and a significant part of the innards of Hindley-Milner typing in order to answer your questions. Expect to bang your head a little! On Tue, 27 May 2008, Andrew Coppin wrote: - A function starts out with a polymorphic type, such as 'x - x'. Which is the same as forall x. x - x. - Each time the function is called, all the type variables have to be locked down to real types such as 'Int' or 'Either (Maybe (IO Int)) String' or something. Yep, in fact in the explicitly-typed calculus commonly used as a model for rank-n polymorphism (System F) there are explicit type lambdas and type applications that do exactly this. Using /\ for a type lambda and [term type] for type applications, id might be written thus: id = /\t.(\x::t-x) and called thus: [id Int] 1 - By the above, any function passed to a high-order function has to have all its type variables locked down, yielding a completely monomorphic function. Yep. - The forall hack somehow convinces the type checker to not lock down some of the type variables. In this way, the type variables relating to a function can remain unlocked until we reach each of the call sites. This allows the variables to be locked to different types at each site [exactly as they would be if the function were top-level rather than an argument]. Not a hack. If there is a hack, it's in /not/ including a forall for rank-1 types. Foralls correspond to type lambdas in the same way that -s correspond to ordinary lambdas. - Why are top-level variables and function arguments treated differently by the type system? The big difference is between lambdas and binding groups (as in let, top-level etc). With the binding group, any constraints on a value's type will be found within its scope - so the type can be 'generalised' there, putting a forall around it. The same isn't true of lambdas, and so their parameters can only be polymorphic given an appropriate type annotation. For extra confusion, type variables are themselves monomorphic[1]. - Why do I have to manually tell the type checker something that should be self-evident? It isn't - the general case is in fact undecidable. - Why do all type variables need to be locked down at each call site in the first place? Find an alternative model for parametric polymorphism that works! Note that 'not locking down' is equivalent to locking down to parameters you took from elsewhere. As such, if you stick to rank-1 types you never actually notice the difference - whereas it makes the type system an awful lot easier to understand. - Why is this virtually never a problem in real Haskell programs? I wouldn't go so far as to say virtually never, I've run into it a fair few times - but normally until you're trying to do pretty generalised stuff it's just not necessary. - Is there ever a situation where the unhacked type system behaviour is actually desirably? There are plenty of situations where a rank-1 type is the correct type. If you give id a rank-2 type, it's more specific - just as if you typed it Int-Int. - Why can't the type system automatically detect where polymorphism is required? Because there's often more than one possible type for a term, without a 'most general' type. - 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? About as much as the undecidability of the halting problem and the incompleteness theory suggest our understanding of computation and logic is fundamentally flawed - which is to say, not at all. The key problem seems to be that the GHC manual assumes that anybody reading it will know what universal quantification actually means. Unfortunately, neither I nor any other human being I'm aware of has the slightest clue what that means. Guess nobody on this list's human, huh? It's really not the GHC manual's job to teach you the language extensions from scratch any more than it should teach Haskell 98 from scratch. I guess the real question is where the relevant community documentation is, something I have to admit to not having needed to check. existential quantification = this is true for SOMETHING universal quantification = this is true for EVERYTHING The type forall x. x - x is for all types x, x - x. As in, for all types x, (\y - y) :: x - x. [1] Actually this is no longer quite true since GHC now supports impredicative polymorphism in which type variables can be instantiated with polymorphic types. But please ignore that for now? -- [EMAIL PROTECTED] 'In Ankh-Morpork even the shit have a street to itself... Truly this is a land of opportunity.' - Detritus, Men at Arms ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Aren't type system extensions fun? [Further analysis]
On Tue, May 27, 2008 at 5:55 PM, Andrew Coppin [EMAIL PROTECTED] wrote: Gleb Alexeyev wrote: foo :: (forall a . a - a) - (Bool, String) foo g = (g True, g bzzt) 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) When you're reasoning about this, I think it would help you greatly to explicitly put in *all* the foralls. In haskell, when you write, say: map :: (a - b) - [a] - [b] All the free variables are *implicitly* quantified at the top level. That is, when you write the above, the compiler sees: map :: forall a b. (a - b) - [a] - [b] (forall has low precedence, so this is the same as: map :: forall a b. ((a - b) - [a] - [b]) ) And the type you mention above for the strange expression is: forall x. (x - x) - (Char, Bool) Which indicates that the caller gets to choose. That is, if a caller sees a 'forall' at the top level, it is allowed to instantiate it with whatever type it likes. Whereas the type you want has the forall in a different place than the implicit quantifiaction: (forall x. x - x) - (Char, Bool) Here the caller does not have a forall at the top level, it is hidden inside a function type so the caller cannot instantiate the type. However, when implementing this function, the argument will now have type forall x. x - x And the implementation can instantiate x to be whatever type it likes. But my strongest advice is, when you're thinking through this, remember that: x - x Is not by itself a type, because x is meaningless. Instead it is Haskell shorthand for forall x. x - x Luke 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. Interestingly, if you throw in the undocumented forall keyword, everything magically works: (forall x. x - x) - (Char, Bool) Obviously, the syntax is fairly untidy. And the program is now not valid Haskell according to the written standard. And best of all, the compiler seems unable to deduce this type automatically either. 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. So far, the only really plausible theory I have been able to come up with is this: - A function starts out with a polymorphic type, such as 'x - x'. - Each time the function is called, all the type variables have to be locked down to real types such as 'Int' or 'Either (Maybe (IO Int)) String' or something. - By the above, any function passed to a high-order function has to have all its type variables locked down, yielding a completely monomorphic function. - In the exotic case above, we specifically WANT a polymorphic function, hence the problem. - The forall hack somehow convinces the type checker to not lock down some of the type variables. In this way, the type variables relating to a function can remain unlocked until we reach each of the call sites. This allows the variables to be locked to different types at each site [exactly as they would be if the function were top-level rather than an argument]. This is a plausible hypothesis for what this language feature actually does. [It is of course frustrating that I have to hypothesise rather than read a definition.] However, this still leaves a large number of questions unanswered... - Why are top-level variables and function arguments treated differently by the type system? - Why do I have to manually tell the type checker something that should be self-evident? - Why do all type variables need to be locked down at each call site in the first place? - Why is this virtually never a problem in real Haskell programs? - Is there ever a situation where the unhacked type system behaviour is actually desirably? - 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? Unfortunately, the GHC manual doesn't have a lot to say on the matter. Reading section 8.7.4 (Arbitrary-rank polymorphism), we find the following: - The type 'x - x' is equivilent to
