Re: [GHC] #714: Inconsistency between handling functional dependencies in class and signature constraints
#714: Inconsistency between handling functional dependencies in class and signature constraints +--- Reporter: claus.rei...@talk21.com |Owner: simonpj Type: bug | Status: new Priority: low |Milestone: 6.12 branch Component: Compiler (Type checker) | Version: 6.5 Severity: normal | Resolution: Keywords: | Difficulty: Unknown Testcase: | Os: Unknown/Multiple Architecture: Unknown/Multiple | +--- Changes (by igloo): * milestone: 6.10 branch = 6.12 branch -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/714#comment:18 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #714: Inconsistency between handling functional dependencies in class and signature constraints
#714: Inconsistency between handling functional dependencies in class and
signature constraints
-+--
Reporter: [EMAIL PROTECTED] | Owner: simonpj
Type: bug | Status: new
Priority: low | Milestone: 6.10 branch
Component: Compiler (Type checker) |Version: 6.5
Severity: normal | Resolution:
Keywords: | Difficulty: Unknown
Testcase: | Architecture: Unknown
Os: Unknown |
-+--
Comment (by simonpj):
An instance declaration is a bit like a function type signature, but a
class declaration is different. It ''looks'' a bit like a signature, but
it is used the other way round. Consider
{{{
class C a = D a where ...
}}}
This means that we can get a dictionary for (C a) from a dictionary for
(D a). On the other hand
{{{
instance C a = D [a] where ...
}}}
means we can get a dictionary for (D [a]) from a dictionary for (C a).
Notice the reversal. So (reversing my previous comment above) I don't
think it's inconsistent to have different rules for class and instance
decls.
So I think Manuel is right here. (And the user manual could be improved.)
I don't think it's impossible to make sense of
{{{
class C a b = D a
}}}
if (C a b) has a functional dependency. But if so, I'd prefer to write
{{{
class C a (F b) = D a
}}}
Let's see if there are examples that give convincing evidence to the
contrary. Perhaps these exist -- Claus describes the problem as acute.
Simon
--
Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/714#comment:11
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler___
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #714: Inconsistency between handling functional dependencies in class and signature constraints
#714: Inconsistency between handling functional dependencies in class and
signature constraints
-+--
Reporter: [EMAIL PROTECTED] | Owner: simonpj
Type: bug | Status: new
Priority: low | Milestone: 6.10 branch
Component: Compiler (Type checker) |Version: 6.5
Severity: normal | Resolution:
Keywords: | Difficulty: Unknown
Testcase: | Architecture: Unknown
Os: Unknown |
-+--
Comment (by claus):
Replying to [comment:10 chak]:
What is the problem with the following answer?
{{{
*Main :t tf
tf :: a
}}}
The constraint `TF a ~ b` can always be satisfied by `b := TF a` and
does not put any restriction on the application of `tf`.
There should be the restriction that there '''exists''' at least one type
family instance (type function application is strict, not lazy, right?-)
at the point of use. There isn't one at all here.
The same holds for the super class constraint `TF a ~ b`. It is
meaningless; hence, I cannot see why we should support it.
It brings a short name `b` into scope, bound to the result of the type
function application.
--
Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/714#comment:12
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler___
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #714: Inconsistency between handling functional dependencies in class and signature constraints
#714: Inconsistency between handling functional dependencies in class and
signature constraints
-+--
Reporter: [EMAIL PROTECTED] | Owner: simonpj
Type: bug | Status: new
Priority: low | Milestone: 6.10 branch
Component: Compiler (Type checker) |Version: 6.5
Severity: normal | Resolution:
Keywords: | Difficulty: Unknown
Testcase: | Architecture: Unknown
Os: Unknown |
-+--
Comment (by claus):
Replying to [comment:11 simonpj]:
An instance declaration is a bit like a function type signature, but a
class declaration is different. It ''looks'' a bit like a signature, but
it is used the other way round.
That is because superclass context constraints are required earlier than
other context constraints: you cannot even write down a class constraint
unless there are corresponding superclass instances, whereas you can write
down instances and function types with unsatisfied contexts, you just
can't use them if the context constraints can't be satisfied.
So, by the time you have a handle on a class constraint that isn't
outright invalid, you know you've already checked its superclass
constraints, which is why you can use the implication backwards.
{{{
class C a b = D a
}}}
if (C a b) has a functional dependency. But if so, I'd prefer to write
{{{
class C a (F b) = D a
}}}
The whole point was to bring `b` into scope as functionally dependent on
`C a _`, thereby ''modelling'' a type function in the scope, using the
(class) contexts for type-level let-bindings. Which is why the
inconsistent handling of contexts in different locations hurts.
Let's see if there are examples that give convincing evidence to the
contrary. Perhaps these exist -- Claus describes the problem as acute.
If the patient was in acute trouble 3 years ago, it might not matter now.
As far as I can recall, the discussion was on TF vs FD, and I was trying
to demonstrate that FD, fully implemented, can do everything that TF can.
As I have seen no indication that any other compiler is going to implement
TF, it still seems important to me to have FD supported well.
--
Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/714#comment:13
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler___
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #714: Inconsistency between handling functional dependencies in class and signature constraints
#714: Inconsistency between handling functional dependencies in class and
signature constraints
-+--
Reporter: [EMAIL PROTECTED] | Owner: simonpj
Type: bug | Status: new
Priority: low | Milestone: 6.10 branch
Component: Compiler (Type checker) |Version: 6.5
Severity: normal | Resolution:
Keywords: | Difficulty: Unknown
Testcase: | Architecture: Unknown/Multiple
Os: Unknown/Multiple |
-+--
Comment (by chak):
Replying to [comment:12 claus]:
Replying to [comment:10 chak]:
What is the problem with the following answer?
{{{
*Main :t tf
tf :: a
}}}
The constraint `TF a ~ b` can always be satisfied by `b := TF a` and
does not put any restriction on the application of `tf`.
There should be the restriction that there '''exists''' at least one
type family instance (type function application is strict, not lazy,
right?-) at the point of use. There isn't one at all here.
Type families are neither strict nor lazy (or rather, I guess, you mean
non-strict). In fact, given that the type language is supposed to be
strongly normalising, the outcome of normalisation is independent of the
evaluation order.
There is absolutely no requirement that a family instance needs to be in
scope in that example. Given the absence of instances for `TF`, `(TF a)`
is simply a type that is only equal to itself and which is not inhabited,
except for bottom. `(TF a)` is already fully normalised.
So, I maintain, GHC is doing the right thing.
The same holds for the super class constraint `TF a ~ b`. It is
meaningless; hence, I cannot see why we should support it.
It brings a short name `b` into scope, bound to the result of the type
function application.
But that name does not occur anywhere else. Hence, it will have no effect
whatsoever on the typing of the rest of the program.
Judging from your previous comment, I believe I know what you were trying
to do. Given
{{{
class TF a ~ b = CTF a
}}}
your intention was that whenever somebody declares an instance
{{{
instance CTF t
}}}
the superclass rules would require that there is also an instance for `TF
t`. Is that right?
Unfortunately, this wouldn't work anyway, for the same reason that `:t tf`
gives you `a`, not `TF a ~ b = a`. A superclass equality of the form `TF
a ~ b`, where `b` doesn't occur anywhere else is trivial to satisfy: just
instantiate `b` with `TF a`. (This again works even if there is no single
instance for `TF`.)
--
Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/714#comment:16
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler___
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #714: Inconsistency between handling functional dependencies in class and signature constraints
#714: Inconsistency between handling functional dependencies in class and
signature constraints
-+--
Reporter: [EMAIL PROTECTED] | Owner: simonpj
Type: bug | Status: new
Priority: low | Milestone: 6.10 branch
Component: Compiler (Type checker) |Version: 6.5
Severity: normal | Resolution:
Keywords: | Difficulty: Unknown
Testcase: | Architecture: Unknown
Os: Unknown |
-+--
Comment (by chak):
Concerning
{{{
type family TF a
-- class TF a ~ b = CTF a -- Not in scope: type variable `b'
tf :: TF a ~ b = a
tf = undefined
}}}
What is the problem with the following answer?
{{{
*Main :t tf
tf :: a
}}}
The constraint `TF a ~ b` can always be satisfied by `b := TF a` and does
not put any restriction on the application of `tf`. Hence, GHC reckons
the types `a` and `TF a ~ b = a` are interchangeable. (If you want the
verbatim signature given for `tf`, use `:i tf`.)
The situation is different for type classes, as `FD a b` signifies that
all methods of `FD` are available in `fd`. There is nothing corresponding
for TFs.
The same holds for the super class constraint `TF a ~ b`. It is
meaningless; hence, I cannot see why we should support it.
--
Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/714#comment:10
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler___
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #714: Inconsistency between handling functional dependencies in class and signature constraints
#714: Inconsistency between handling functional dependencies in class and signature constraints -+-- Reporter: [EMAIL PROTECTED] | Owner: simonpj Type: bug | Status: new Priority: low | Milestone: 6.10 branch Component: Compiler (Type checker) |Version: 6.5 Severity: normal | Resolution: Keywords: | Difficulty: Unknown Testcase: | Architecture: Unknown Os: Unknown | -+-- Changes (by igloo): * milestone: _|_ = 6.10 branch -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/714#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #714: Inconsistency between handling functional dependencies in class and signature constraints
#714: Inconsistency between handling functional dependencies in class and
signature constraints
-+--
Reporter: [EMAIL PROTECTED] | Owner: simonpj
Type: bug | Status: new
Priority: low | Milestone: _|_
Component: Compiler (Type checker) |Version: 6.5
Severity: normal | Resolution:
Keywords: | Difficulty: Unknown
Testcase: | Architecture: Unknown
Os: Unknown |
-+--
Comment (by claus):
could this please be re-milestoned, for 6.10, as that seems to be the
target for completing the overhaul mentioned by Simon PJ.
since this is reported as a scope error, the same inconsistency now
applies to TFs, but there we have the additional oddity that the signature
constraint is simply dropped even if there are no type instances at all..:
{{{
class FD a b | a - b
-- class FD a b = CFD a -- Not in scope: type variable `b'
fd :: FD a b = a
fd = undefined
type family TF a
-- class TF a ~ b = CTF a -- Not in scope: type variable `b'
tf :: TF a ~ b = a
tf = undefined
}}}
{{{
*Main :t fd
fd :: (FD a b) = a
*Main :t tf
tf :: a
}}}
--
Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/714#comment:8
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler___
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Re: [GHC] #714: Inconsistency between handling functional dependencies in class and signature constraints
#714: Inconsistency between handling functional dependencies in class and signature constraints -+-- Reporter: [EMAIL PROTECTED] | Owner: simonpj Type: bug | Status: new Priority: low | Milestone: _|_ Component: Compiler (Type checker) |Version: 6.5 Severity: normal | Resolution: Keywords: | Difficulty: Unknown Testcase: | Architecture: Unknown Os: Unknown | -+-- Changes (by simonpj): * summary: inconsistency between handling of class and signature constraints = Inconsistency between handling functional dependencies in class and signature constraints -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/714#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler___ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
