Here is a small puzzle. -- The following generates a type error: f :: Char -> Char f c = let x = g c in h x -- But this definition does not: f :: Char -> Char f c = let x :: Bool x = g c in h x Furthermore, replacing Bool by any other type in the latter definition will always give a type error. How is this possible? Scroll down for the answer. Here is the module: module Puzzle(f) where f :: Char -> Char f c = let x = g c in h x class C a where g :: Char -> a h :: a -> Char instance C Bool where g c = c == 'T' h b = if b then 'T' else 'F' The error message from ghc is Puzzle.hs:5:12: Ambiguous type variable `a' in the top-level constraint: `C a' arising from use of `g' at Puzzle.hs:5:12 I know the technical reason why this is happening. But it's hard for me to motivate why this is reasonable. The type variable `a' is not ambiguous at all, the only type it can possibly have is Bool; any other type is an error. Furthermore, there can never be any other instance of the class C added to any program using the module Puzzle since the class C is not exported. So in what sense is this really ambiguous? I think it would be quite reasonable to allow the Puzzle module to compile, resolving `a' to be Bool. I.e., if there is only one instance that can satisfy a constraint and there is no possibility of adding instances outside the compiled module, I think resolving the overloading makes sense. -- Lennart
Lennart Augustsson wrote:
[snip] So in what sense is this really ambiguous?
I think it would be quite reasonable to allow the Puzzle module to compile, resolving `a' to be Bool. I.e., if there is only one instance that can satisfy a constraint and there is no possibility of adding instances outside the compiled module, I think resolving the overloading makes sense.
You may be interested in a recent paper by Bastiaan Heeren and Juriaan Hage [1] about type class directives. The "closed" directive in that paper is more or less implied by your example. Here is a quote from the paper: "The main advantage of a closed type class is that we know the fixed set of instances. Using this knowledge, we can influence the type inference process. As discussed in the introduction to Section 2, we can reject definitions early on (in case the set of instances for a certain type class is empty) or improve a type variable to a certain type (in case the set of instances is a singleton)." All the best, -- Daan Leijen. [1] http://www.cs.uu.nl/~bastiaan/papers.html#typeclassdirectives (to appear in PADL 2005)
-- Lennart _______________________________________________ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
No, closed classes are different, here we are talking about lazy overlap resolution, so if at _call_ time only one instance fits we choose it. Closing a class is different. Keean. Daan Leijen wrote:
Lennart Augustsson wrote:
[snip] So in what sense is this really ambiguous?
I think it would be quite reasonable to allow the Puzzle module to compile, resolving `a' to be Bool. I.e., if there is only one instance that can satisfy a constraint and there is no possibility of adding instances outside the compiled module, I think resolving the overloading makes sense.
You may be interested in a recent paper by Bastiaan Heeren and Juriaan Hage [1] about type class directives. The "closed" directive in that paper is more or less implied by your example. Here is a quote from the paper:
"The main advantage of a closed type class is that we know the fixed set of instances. Using this knowledge, we can influence the type inference process. As discussed in the introduction to Section 2, we can reject definitions early on (in case the set of instances for a certain type class is empty) or improve a type variable to a certain type (in case the set of instances is a singleton)."
All the best, -- Daan Leijen.
[1] http://www.cs.uu.nl/~bastiaan/papers.html#typeclassdirectives (to appear in PADL 2005)
-- Lennart _______________________________________________ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
_______________________________________________ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
Keean Schupke wrote:
No, closed classes are different, here we are talking about lazy overlap resolution, so if at _call_ time only one instance fits we choose it. Closing a class is different.
A "closed class" directive however is an explicit specification that makes the intention of the designer explicit in the program. Since it would solve the puzzle in a rather elegant and explicit way, I thought that it was interesting to mention. All the best, -- Daan.
Keean.
Daan Leijen wrote:
Lennart Augustsson wrote:
[snip] So in what sense is this really ambiguous?
I think it would be quite reasonable to allow the Puzzle module to compile, resolving `a' to be Bool. I.e., if there is only one instance that can satisfy a constraint and there is no possibility of adding instances outside the compiled module, I think resolving the overloading makes sense.
You may be interested in a recent paper by Bastiaan Heeren and Juriaan Hage [1] about type class directives. The "closed" directive in that paper is more or less implied by your example. Here is a quote from the paper:
"The main advantage of a closed type class is that we know the fixed set of instances. Using this knowledge, we can influence the type inference process. As discussed in the introduction to Section 2, we can reject definitions early on (in case the set of instances for a certain type class is empty) or improve a type variable to a certain type (in case the set of instances is a singleton)."
All the best, -- Daan Leijen.
[1] http://www.cs.uu.nl/~bastiaan/papers.html#typeclassdirectives (to appear in PADL 2005)
-- Lennart _______________________________________________ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
_______________________________________________ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
_______________________________________________ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
Daan Leijen wrote:
Keean Schupke wrote:
No, closed classes are different, here we are talking about lazy overlap resolution, so if at _call_ time only one instance fits we choose it. Closing a class is different.
A "closed class" directive however is an explicit specification that makes the intention of the designer explicit in the program. Since it would solve the puzzle in a rather elegant and explicit way, I thought that it was interesting to mention.
Indeed, a closed directive would have been fine. But it's not really necessary, the class is obviously closed because of not being exported. But the type checker doesn't use this fact. I find it somewhat anomalous that there is one unique way to give types to my program, but that the type checker refuses to do it. :) -- Lennart
Lennart Augustsson wrote:
Daan Leijen wrote:
A "closed class" directive however is an explicit specification that makes the intention of the designer explicit in the program. Since it would solve the puzzle in a rather elegant and explicit way, I thought that it was interesting to mention.
Indeed, a closed directive would have been fine. But it's not really necessary, the class is obviously closed because of not being exported. But the type checker doesn't use this fact. I find it somewhat anomalous that there is one unique way to give types to my program, but that the type checker refuses to do it. :)
You are right, I feel like that too: one should expect that the type checker can figure this out, and perhaps it is even really useful. On the other hand, suppose you decide later to export the class, and suddenly your code would no longer type check. The fact that adding an export defintion would lead to a type error somewhere else in the code might be rather confusing. (worse! it might be considered inelegant :-) Personally, I feel that this problem might be better solved by making a lot of the implicit assumptions (and semantics) of type classes more explicit, and bring them under user control. Of course, I do have not have any idea of how this should be done concretely ;-) (although type class directives might be a step in the right direction?) -- Daan
Daan Leijen wrote:
You are right, I feel like that too: one should expect that the type checker can figure this out, and perhaps it is even really useful. On the other hand, suppose you decide later to export the class, and suddenly your code would no longer type check.
I must have missed a mail... how could adding an export change the code?
The fact that adding an export defintion would lead to a type error somewhere else in the code might be rather confusing. (worse! it might be considered inelegant :-)
Keean.
Keean Schupke wrote:
Daan Leijen wrote:
You are right, I feel like that too: one should expect that the type checker can figure this out, and perhaps it is even really useful. On the other hand, suppose you decide later to export the class, and suddenly your code would no longer type check.
I must have missed a mail... how could adding an export change the code?
If you export the class you can add another instance to it. And now my type variable would really be ambiguous. -- Lennart
Ah, I see... Thats basically the same problem as overlapping instances then... (Which we have - but I try to avoid except where unavoidable...). Still, It seems it could be a good 'optional' feature. Keean. Lennart Augustsson wrote:
Keean Schupke wrote:
Daan Leijen wrote:
You are right, I feel like that too: one should expect that the type checker can figure this out, and perhaps it is even really useful. On the other hand, suppose you decide later to export the class, and suddenly your code would no longer type check.
I must have missed a mail... how could adding an export change the code?
If you export the class you can add another instance to it. And now my type variable would really be ambiguous.
-- Lennart
Daan Leijen wrote:
You are right, I feel like that too: one should expect that the type checker can figure this out, and perhaps it is even really useful. On the other hand, suppose you decide later to export the class, and suddenly your code would no longer type check. The fact that adding an export defintion would lead to a type error somewhere else in the code might be rather confusing. (worse! it might be considered inelegant :-)
Yes, that is somewhat strange, I agree. :)
Personally, I feel that this problem might be better solved by making a lot of the implicit assumptions (and semantics) of type classes more explicit, and bring them under user control. Of course, I do have not have any idea of how this should be done concretely ;-)
(although type class directives might be a step in the right direction?)
Yes, I think the type class directives is a step forwards. :) -- Lennart
This is a great example, thanks for posting it. However, I feel like the real problem in this example is the lexically-scoped type variables declared with your function f. I am always surprised by the effects that lexically-scoped type variables can have on top-level declarations. Consider another example: f :: a -> a f = \x -> x Of course, f has type (forall a. a -> a). However, if we add another declaration g with lexically-scoped type variable a: g :: a -> a = \x -> 1 Then, suddenly, f has type Integer -> Integer If g is defined as: g :: a -> a = \x -> (1::Int) Then, f has type Int -> Int. If g is defined as: g :: a -> Int = \x -> 1 Then, f has type () -> () Personally, I would not mind if lexically-scoped type variables on top-level declarations were disallowed; or at least treated as "normal" top-level type annotations. --Paul On Nov 24, Lennart Augustsson wrote:
Here is a small puzzle.
-- The following generates a type error: f :: Char -> Char f c = let x = g c in h x
-- But this definition does not: f :: Char -> Char f c = let x :: Bool x = g c in h x
Furthermore, replacing Bool by any other type in the latter definition will always give a type error.
[...snip...]
I realize now that your original example did not actually have any such type variables. While playing around with your puzzle, I managed to introduce some. However, perhaps the lexically-scoped type variables are interesting in their own right. Sorry for the confusion, --Paul On Nov 24, Paul Govereau wrote:
This is a great example, thanks for posting it. However, I feel like the real problem in this example is the lexically-scoped type variables declared with your function f. I am always surprised by the effects that lexically-scoped type variables can have on top-level declarations.
[...snip...]
Paul Govereau <govereau@eecs.harvard.edu> writes:
This is a great example, thanks for posting it. However, I feel like the real problem in this example is the lexically-scoped type variables declared with your function f. I am always surprised by the effects that lexically-scoped type variables can have on top-level declarations.
I remain unpuzzled by your examples, could I ask you to elaborate?
Consider another example:
f :: a -> a f = \x -> x
Of course, f has type (forall a. a -> a).
Yes.
However, if we add another declaration g with lexically-scoped type variable a:
g :: a -> a = \x -> 1
Then, suddenly, f has type Integer -> Integer
Well, you say that the parameter and return value have the same type a, and I suppose Haskell monomorphs the constant 1 to Integer. Did you perhaps mean: g :: a -> a = \x -> x which has type () -> () ? -kzm -- If I haven't seen further, it is by standing in the footprints of giants
Ketil Malde <ketil+haskell@ii.uib.no> writes:
Did you perhaps mean:
g :: a -> a = \x -> x
which has type () -> () ?
Or maybe the difference between: g :: Num a => a -> a g = \x -> 1 (which gives the specified type) and g' :: forall a . Num a => a -> a g' = \x -> 1 (which gives Integer -> Integer)? -kzm -- If I haven't seen further, it is by standing in the footprints of giants
G'day all. Quoting Lennart Augustsson <lennart@augustsson.net>:
Here is a small puzzle.
You can understand this one because the closed world hypothesis doesn't apply to type context inference. However, this seems as good a time as any to mention one of my pet peeves again: module FD where class C from to | from -> to where g :: from -> to h :: to -> from instance C Char Bool where g c = c == 'T' h b = if b then 'T' else 'F' f :: (C Char a) => Char -> a f c = g c -- And the error, found in f, is... {- FD.hs:12: Cannot unify the type-signature variable `a' with the type `Bool' Expected type: Bool Inferred type: a When using functional dependencies to combine C Char Bool, arising from the instance declaration at FD.hs:7 C Char a, arising from a type signature at FD.hs:11 When generalising the type(s) for `f' -} This is a pretty serious problem when you're doing typeclass metaprogramming. In this case, the type you're trying to find is Bool. In general, it might be a large complex type, generated by the class C as a typeclass metaprogram, which you don't want to put in the type signature for maintainability reasons. Because of the functional dependency on C, the return type of f can only be one thing. This partially "closes the world" in a way that the original program did not. So in that sense, the declared type of f is no less general than its "real" type, Char -> Bool. It would be nice if Haskell implementations allowed declarations such as this. Cheers, Andrew Bromage
ajb@spamcop.net wrote:
G'day all.
Quoting Lennart Augustsson <lennart@augustsson.net>:
Here is a small puzzle.
You can understand this one because the closed world hypothesis doesn't apply to type context inference.
I have no problem understanding the technical reason for this. But I now think it's a poor design. -- Lennart
I have already asked Simon PJ if this can be implemented in GHC... So if more people ask for it, it might get done! Keean Lennart Augustsson wrote:
Here is a small puzzle.
-- The following generates a type error: f :: Char -> Char f c = let x = g c in h x
-- But this definition does not: f :: Char -> Char f c = let x :: Bool x = g c in h x
Furthermore, replacing Bool by any other type in the latter definition will always give a type error.
How is this possible?
Scroll down for the answer.
Here is the module:
module Puzzle(f) where
f :: Char -> Char f c = let x = g c in h x
class C a where g :: Char -> a h :: a -> Char
instance C Bool where g c = c == 'T' h b = if b then 'T' else 'F'
The error message from ghc is Puzzle.hs:5:12: Ambiguous type variable `a' in the top-level constraint: `C a' arising from use of `g' at Puzzle.hs:5:12
I know the technical reason why this is happening. But it's hard for me to motivate why this is reasonable. The type variable `a' is not ambiguous at all, the only type it can possibly have is Bool; any other type is an error.
Furthermore, there can never be any other instance of the class C added to any program using the module Puzzle since the class C is not exported.
So in what sense is this really ambiguous?
I think it would be quite reasonable to allow the Puzzle module to compile, resolving `a' to be Bool. I.e., if there is only one instance that can satisfy a constraint and there is no possibility of adding instances outside the compiled module, I think resolving the overloading makes sense.
-- Lennart _______________________________________________ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
I have a concern with this, if I understand the issue correctly. Suppose I have a source module that compiles and runs correctly. Now suppose I add a restricted (selective) import statement to the file, explicitly introducing a name that I know does not clash with anything in my module. I expect the module to continue to compile and run correctly. If I understand Lennart's proposal correctly, adding such an import could cause the compilation to fail, by adding new instance options that then needs to be disambiguated. Under the present regime, this is not a problem, because information to disambiguate the instance selection needs to added even if there's only one visible instance, so adding the restricted import cannot introduce this failure. Similar concerns might apply if new instances are added to a module that is already a restricted import. I suspect that the proper fix to this is that a selective import should also name the instances that are imported. Then disambiguation of instances can reasonably be based on just the visible imports. The automatic import of instances, even when the restricted form of import is used, has often seemed a little odd to me. #g -- At 14:36 25/11/04 +0000, Keean Schupke wrote:
I have already asked Simon PJ if this can be implemented in GHC... So if more people ask for it, it might get done!
Keean
Lennart Augustsson wrote:
Here is a small puzzle.
-- The following generates a type error: f :: Char -> Char f c = let x = g c in h x
-- But this definition does not: f :: Char -> Char f c = let x :: Bool x = g c in h x
Furthermore, replacing Bool by any other type in the latter definition will always give a type error.
How is this possible?
Scroll down for the answer.
Here is the module:
module Puzzle(f) where
f :: Char -> Char f c = let x = g c in h x
class C a where g :: Char -> a h :: a -> Char
instance C Bool where g c = c == 'T' h b = if b then 'T' else 'F'
The error message from ghc is Puzzle.hs:5:12: Ambiguous type variable `a' in the top-level constraint: `C a' arising from use of `g' at Puzzle.hs:5:12
I know the technical reason why this is happening. But it's hard for me to motivate why this is reasonable. The type variable `a' is not ambiguous at all, the only type it can possibly have is Bool; any other type is an error.
Furthermore, there can never be any other instance of the class C added to any program using the module Puzzle since the class C is not exported.
So in what sense is this really ambiguous?
I think it would be quite reasonable to allow the Puzzle module to compile, resolving `a' to be Bool. I.e., if there is only one instance that can satisfy a constraint and there is no possibility of adding instances outside the compiled module, I think resolving the overloading makes sense.
-- Lennart _______________________________________________ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
_______________________________________________ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
------------ Graham Klyne For email: http://www.ninebynine.org/#Contact
Graham Klyne wrote:
I have a concern with this, if I understand the issue correctly.
Suppose I have a source module that compiles and runs correctly.
Now suppose I add a restricted (selective) import statement to the file, explicitly introducing a name that I know does not clash with anything in my module. I expect the module to continue to compile and run correctly.
If I understand Lennart's proposal correctly, adding such an import could cause the compilation to fail, by adding new instance options that then needs to be disambiguated. Not in my particular case. The class is local to the module. Any instance declaration would have to be in that module.
-- Lennart
At 19:14 25/11/04 +0100, Lennart Augustsson wrote:
Graham Klyne wrote:
I have a concern with this, if I understand the issue correctly. Suppose I have a source module that compiles and runs correctly. Now suppose I add a restricted (selective) import statement to the file, explicitly introducing a name that I know does not clash with anything in my module. I expect the module to continue to compile and run correctly. If I understand Lennart's proposal correctly, adding such an import could cause the compilation to fail, by adding new instance options that then needs to be disambiguated. Not in my particular case. The class is local to the module. Any instance declaration would have to be in that module.
OK, I missed that. But, it seems to me, that adding export of the class concerned to the module heading could raise a similar scenario to that mentioned. It's less clear-cut, but it seems surprising to me that the choice of whether or not to export something from a module should (potentially) change its meaning or validity. #g ------------ Graham Klyne For email: http://www.ninebynine.org/#Contact
Of course it can. I might do it myself. :) -- Lennart Keean Schupke wrote:
I have already asked Simon PJ if this can be implemented in GHC... So if more people ask for it, it might get done!
Keean
Lennart Augustsson wrote:
Here is a small puzzle.
-- The following generates a type error: f :: Char -> Char f c = let x = g c in h x
-- But this definition does not: f :: Char -> Char f c = let x :: Bool x = g c in h x
participants (8)
-
ajb＠spamcop.net -
Daan Leijen -
Graham Klyne -
Graham Klyne
-
Keean Schupke -
Ketil Malde -
Lennart Augustsson -
Paul Govereau