class Foo a b | a -> b instance Foo Int String bar :: Foo Int b => b bar = "rargh" Is there any reason why that shouldn't work? GHC gives one of its silly "b is a rigid variable" errors (aside: that's a really confusing error; I'd prefer something like Hugs's "Infered type is not general enough"). -- -David House, dmhouse@gmail.com
Hello,
There is nothing wrong with this program. I have run into this
problem and I consider it to be a bug/weakness of the type checking
algorithm used by the implementation.
(I also agree with you that the term "rigid variable" is rather
confusing because it is an artifact of the type checking algorithm
used by GHC.)
-Iavor
On 3/3/07, David House
class Foo a b | a -> b instance Foo Int String bar :: Foo Int b => b bar = "rargh"
Is there any reason why that shouldn't work? GHC gives one of its silly "b is a rigid variable" errors (aside: that's a really confusing error; I'd prefer something like Hugs's "Infered type is not general enough").
-- -David House, dmhouse@gmail.com _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
| > class Foo a b | a -> b | > instance Foo Int String | > bar :: Foo Int b => b | > bar = "rargh" | There is nothing wrong with this program. I have run into this | problem and I consider it to be a bug/weakness of the type checking | algorithm used by the implementation. | | (I also agree with you that the term "rigid variable" is rather | confusing because it is an artifact of the type checking algorithm | used by GHC.) Some brief comments a) I agree there is nothing wrong with this program, BUT it can't be translated into System F. That's why GHC rejects it. However, it *can* be translated into System FC (see "System F with type equality coercions", on my home page). But doing so requires a new implementation of type inference for functional dependencies, and I have not done that yet. b) While the program is arguably OK, I have yet to see a really convincing application that needs it. Why not write bar :: String? c) I really want to get rid of functional dependencies altogether, in favour of associated types. Thus class Foo a where type Bar a instance Foo Int where type Bar Int = String bar :: Foo a => Bar a bar = "rargh" This too requires work on type inference, and we're actively working on that. 4. The "rigid type variable" thing isn't just an implementation question. What *would* you like the error message to say when you write f :: ([a], Int) -> Int f (x:xs, y) = x+y Here we unify 'a' with Int, which is wrong. What would a nicer error message say? Simon
On 3/5/07, Simon Peyton-Jones
4. The "rigid type variable" thing isn't just an implementation question. What *would* you like the error message to say when you write f :: ([a], Int) -> Int f (x:xs, y) = x+y Here we unify 'a' with Int, which is wrong. What would a nicer error message say?
IMO, the "rigid type variable" error message is confusing for two reasons: (1) it doesn't suggest to the user (or at least the novice-to-intermediate user) what they should do to solve the problem, and (2) it makes the user feel like they need to go read six papers on type inference before they can make any progress when all they wanted to do is add two numbers. In this particular case, something like "Suggested fix: change 'a' in the type signature to 'Int'" would be an improvement: it addresses reason (1), and putting it ahead of the "rigid type variable" part (e.g., textually highlighting the more newbie-friendly portion of the error message) addresses reason (2). (I realize that the same error might occur in cases where the type variable isn't bound by a user type signature, but it's common enough for users to insert type signatures when the code isn't compiling that I think it's worth it to treat that as a special case, even if there isn't a more general way to improve the error message.) Cheers, Kirsten -- Kirsten Chevalier* chevalier@alum.wellesley.edu *Often in error, never in doubt "And I have grown with each disappointment through the years" -- Great Big Sea
On 06/03/07, Simon Peyton-Jones
4. The "rigid type variable" thing isn't just an implementation question. What *would* you like the error message to say when you write f :: ([a], Int) -> Int f (x:xs, y) = x+y Here we unify 'a' with Int, which is wrong. What would a nicer error message say?
"Inferred type was monomorphic but a polymorphic type was given", or something. Hugs says "Inferred type not as polymorphic as expected", which is the right kind of area. -- -David House, dmhouse@gmail.com
| > 4. The "rigid type variable" thing isn't just an implementation question. What *would* you like the | error message to say when you write | > f :: ([a], Int) -> Int | > f (x:xs, y) = x+y | > Here we unify 'a' with Int, which is wrong. What would a nicer error message say? | | "Inferred type was monomorphic but a polymorphic type was given", or | something. Hugs says "Inferred type not as polymorphic as expected", | which is the right kind of area. Hmm. But at the moment the type error happens, we are indeed unifying 'a' with Int, and I think it's helpful to say so. What Hugs does (I think) is to infer the most general type of the untyped fn, and compare with the signature. But in general that gives worse error messages; and when you have higher-rank types you can't ignore the type sig and do inference first. I'm not against adding "type is too monomorphic" or something like that if you think it'd help, but I'd like to say something about the incompatibility of 'a' and 'Int'. No? Smon
On 06/03/07, Simon Peyton-Jones
I'm not against adding "type is too monomorphic" or something like that if you think it'd help, but I'd like to say something about the incompatibility of 'a' and 'Int'. No?
Here's a proper draft, then. Foo.hs: foo :: [a] -- line 1 foo = "hello" -- line 2 Error message: Inferred type is not as polymorphic as type signature claims. Inferred type: [Char] Expected type: [a] Provided by the type signature: foo :: [a] at ~/foo.hs:1 (`a', a polymorphic type variable, could not be unified with `Char', a monotype.) In the expression: "hello" at ~/foo.hs:1:8 In the definition of `foo': foo = "hello" How's that sound? -- -David House, dmhouse@gmail.com
Error message: Inferred type is not as polymorphic as type signature claims. Inferred type: [Char] Expected type: [a] Provided by the type signature: foo :: [a] at ~/foo.hs:1 (`a', a polymorphic type variable, could not be unified with `Char', a monotype.) In the expression: "hello" at ~/foo.hs:1:8 In the definition of `foo': foo = "hello"
How's that sound?
too complicated? more explanation isn't always more helpful. the user is confused at this point, and more information might mean more confusion. compare with Hugs> let {foo :: [a];foo = "hello" } in "oops" ERROR - Inferred type is not general enough *** Expression : foo *** Expected type : [a] *** Inferred type : [Char] Prelude> let {foo :: [a];foo = "hello" } in "oops" <interactive>:1:22: Couldn't match the rigid variable `a' against `Char' `a' is bound by the type signature for `foo' Expected type: [a] Inferred type: [Char] In the definition of `foo': foo = "hello" In the definition of `it': it = let foo :: [a] foo = "hello" in "oops" personally, i like the Hugs version best, but the GHC version is consistent and informative as well. the problem is that GHC refers to a new concept, rigid variables, whereas Hugs keeps things basic (and even that takes some getting used to for beginners). rigidness is a useful concept, once you get used to it. and GHC's message actually contains an explanation of what rigid means in this context, but that in itself isn't obvious when the user is freshly confused by that new term (not to mention the rejected program). perhaps just replacing the line `a' is bound by the type signature for `foo' with instantiating `a' with `Char' would conflict with the explicit type signature for `foo' might help. perhaps a section in the user's guide on the topic "how to interpret error messages" (Simon Thompson had such a thing for the mysteries of Hugs messages), and a "dictionary of terms used" (briefly explaining 'rigid' and the like) would not go amiss, either. these days, they could perhaps be a wiki, growing as needed, but you'd want to copy snapshots into releases, right into the user's guide. claus ps. i was somewhat shocked to read that SPJ wants FDs gone.
ps. i was somewhat shocked to read that SPJ wants FDs gone.
Why? Simon has good taste. :)
de gustibus non est disputandum ;) FD have uses and problems and AT have uses and problems. starting anew with the latter doesn't fix the problems, it just changes their form. if AT are meant to take over from FD, then either they have fewer uses or similar problems. the assumption seems to be that AT are somehow equivalent to FD, as in "any working FD program has an equivalent AT form". but if the problems can be fixed in the AT form, they can be fixed in the FD form, and if the problems cannot be fixed in the FD form, they cannot be fixed in the AT form. in particular, many of the problems with FD are ambiguities in interpreting interactions with other popular features, such as overlap resolution. it took half a decade of practical experience to expose such issues for FD, and i don't see the fact that AT haven't reached that stage yet as any advantage. there are examples for which the AT form looks nicer than the FD form, and there are examples for which the AT form is more complicated than the FD form. about the only half-way convincing non-aesthetic argument i recall in favour of AT is that their restricted form might help to exclude problematic programs, but if that is true, imposing equivalent restrictions on FD should have similar benefits. i was hoping that the delay on standardising FD meant that we would get an additional option, with opportunities to gain insights into the issues with AT, without losing the FD view. after that, the issues common to both FD and AT ought to be sorted out. only *after* that would there be any point in chosing one of the two on aestethic grounds, and possibly phasing out support for the other. unless i'm missing something, and all this has already happened?-) claus
Claus Reinke wrote:
ps. i was somewhat shocked to read that SPJ wants FDs gone.
Why? Simon has good taste. :)
de gustibus non est disputandum ;)
FD have uses and problems and AT have uses and problems. starting anew with the latter doesn't fix the problems, it just changes their form.
Well, the choice between FD and AT (and maybe yet undiscovered alternatives) is entirely a matter of "convenience" as much as everything related to type inference is. The same goes for type classes or subtyping: all these can be translated to system F (or FC for FD and AT) so they don't add abstraction power at run-time. Their only but important purpose is to auto-infer code. FD are pretty much type-level programming in a kind of mini-prolog. Of course, AT are type-level programming as well, but functional in style, which is arguably more compelling for a functional base language. At least, I think that FD are somehow ugly.
in particular, many of the problems with FD are ambiguities in interpreting interactions with other popular features, such as overlap resolution. it took half a decade of practical experience to expose such issues for FD, and i don't see the fact that AT haven't reached that stage yet as any advantage.
Quite telling that it took half a decade to shed light on the semantics of the many FD variants, isn't it? :) I guess that AT will come with semantics included because it's otherwise unclear how to implement them. Implementing FD is simply easier as type inference already is a kind of mini-prolog. Of course, that doesn't simplify their semantics at all. In a sense, knowing AT is knowing how much functional in style type inference can be. Regards, apfelmus
F, FD, FC, AT, SPJ ;) WTH does it mean? On Wed, Mar 07, 2007 at 10:12:11AM +0100, apfelmus@quantentunnel.de wrote:
Claus Reinke wrote:
ps. i was somewhat shocked to read that SPJ wants FDs gone.
Why? Simon has good taste. :)
de gustibus non est disputandum ;)
FD have uses and problems and AT have uses and problems. starting anew with the latter doesn't fix the problems, it just changes their form.
Well, the choice between FD and AT (and maybe yet undiscovered alternatives) is entirely a matter of "convenience" as much as everything related to type inference is. The same goes for type classes or subtyping: all these can be translated to system F (or FC for FD and AT) so they don't add abstraction power at run-time. Their only but important purpose is to auto-infer code.
FD are pretty much type-level programming in a kind of mini-prolog. Of course, AT are type-level programming as well, but functional in style, which is arguably more compelling for a functional base language. At least, I think that FD are somehow ugly.
in particular, many of the problems with FD are ambiguities in interpreting interactions with other popular features, such as overlap resolution. it took half a decade of practical experience to expose such issues for FD, and i don't see the fact that AT haven't reached that stage yet as any advantage.
Quite telling that it took half a decade to shed light on the semantics of the many FD variants, isn't it? :)
I guess that AT will come with semantics included because it's otherwise unclear how to implement them. Implementing FD is simply easier as type inference already is a kind of mini-prolog. Of course, that doesn't simplify their semantics at all. In a sense, knowing AT is knowing how much functional in style type inference can be.
Regards, apfelmus
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
hi mm (?-),
F, FD, FC, AT, SPJ ;) WTH does it mean?
sorry about this acronymitis :) there was a lengthy debate about some of these things in the context of haskell' a year or so ago, and i just fell back into the mood, forgetting to explain my acronyms before using them again F: System F, polymorphic lambda-calculi due to Girard FC: System F, extended with equality coercions, FD: functional dependencies, as in Hugs/GHC CHR: constraint-handling rules, used for operational semantics of MPTC with FD AT: associated types, as in GHC SPJ: advanced haskell processor, theory and practice MPTC: multi-parameter type (constructor) classes, as in Hugs/GHC/? ACRONYM: abbreviations can relatively often nix your message for relevant publications see Mark Jones on FD,MPTC origins, Simon Peyton Jones, Martin Sulzmann, Manuel Chakravarty on more recent work on FC,AT, FD,CHR. also check the bibliography section at haskell.org, in particular the part on type systems: http://www.haskell.org/haskellwiki/Research_papers/Type_systems hth claus hth: hope this helps
ATs are not in any of the official GHC releases... Are they in the CVS head?
darcs, these days;-) but yes, from 6.7. see: announcement http://article.gmane.org/gmane.comp.lang.haskell.general/14447 main? info page http://haskell.org/haskellwiki/GHC/Indexed_types ghc status, with new features http://hackage.haskell.org/trac/ghc/wiki/Status/October06 master plan http://hackage.haskell.org/trac/ghc/wiki/TypeFunctions claus
| ATs are not in any of the official GHC releases... Are they in the CVS head? The HEAD has fully-implemented associated *data types*, but not associated *type synonyms*. We're working on the latter, quite hard. As Claus says, the place to look is here http://hackage.haskell.org/trac/ghc/wiki/TypeFunctions Simon
-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1
too complicated? more explanation isn't always more helpful. the user is confused at this point, and more information might mean more confusion.
That is true, but my experience is that when an error message perplexes me I need all the suggestions I can get from more error messages. Sometimes a Hugs error has helped me more than a GHC error, and sometimes the other way around. Type inference is complicated and doesn't know where your mistake is, so it may be best to point out several views of the problem in case one of them makes sense. (of course it could also be that I was writing programs that were too complicated for me to understand, as I was still learning good style in Haskell :)) Isaac -----BEGIN PGP SIGNATURE----- Version: GnuPG v1.4.3 (GNU/Linux) Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org iD8DBQFF7fc7HgcxvIWYTTURArAFAKDGCu6KwtCLen/UBj0FcS7LdKabKgCgknms deZzzGy0uFDPMoXxJMLPVF4= =inId -----END PGP SIGNATURE-----
participants (9)
-
apfelmus＠quantentunnel.de -
Claus Reinke -
David House -
Iavor Diatchki -
Isaac Dupree -
Kirsten Chevalier -
Lennart Augustsson -
mm -
Simon Peyton-Jones