Lennart Augustsson:
On Thu, Apr 10, 2008 at 4:20 AM, Manuel M T Chakravarty [EMAIL PROTECTED]
wrote:
the five signatures
forall a. S a
forall b. S b
forall a b. S (a, b)
Int
S Int
By alpha-convertible I mean the usual thing from lambda calculus,
they are identical modulo the names
Lennart Augustsson:
In the current GHC there are even definitions that are perfecty
usable, that cannot be given the type signature that that was
inferred.
That's bad, I agree.
At work we have the warning for missing signatures enabled, and we
turn warnings into errors. We have to
Lennart Augustsson:
On Thu, Apr 10, 2008 at 4:20 AM, Manuel M T Chakravarty [EMAIL PROTECTED]
wrote:
Lennart Augustsson:
On Wed, Apr 9, 2008 at 8:53 AM, Martin Sulzmann [EMAIL PROTECTED]
wrote:
Lennart, you said
(It's also pretty easy to fix the problem.)
What do you mean? Easy to fix
Lennart Augustsson wrote:
On Wed, Apr 9, 2008 at 8:53 AM, Martin Sulzmann
[EMAIL PROTECTED] mailto:[EMAIL PROTECTED] wrote:
Lennart, you said
(It's also pretty easy to fix the problem.)
What do you mean? Easy to fix the type checker, or easy to fix the
program by
On Thu, Apr 10, 2008 at 4:20 AM, Manuel M T Chakravarty
[EMAIL PROTECTED] wrote:
the five signatures
forall a. S a
forall b. S b
forall a b. S (a, b)
Int
S Int
By alpha-convertible I mean the usual thing from lambda calculus, they are
identical modulo the names of bound variables.
I didn't say TF was the only broken feature in GHC. But I want to see the
broken ones removed, instead of new ones added. :)
In the current GHC there are even definitions that are perfecty usable, that
cannot be given the type signature that that was inferred.
At work we have the warning for
On Thu, Apr 10, 2008 at 4:20 AM, Manuel M T Chakravarty
[EMAIL PROTECTED] wrote:
Lennart Augustsson:
On Wed, Apr 9, 2008 at 8:53 AM, Martin Sulzmann
[EMAIL PROTECTED] wrote:
Lennart, you said
(It's also pretty easy to fix the problem.)
What do you mean? Easy to fix the type
To make it legal: If foo' with a type signature doesn't type check,
try to infer a type without a signature. If this succeeds then
check that the type that was inferred is alpha-convertible to the
original signature. If it is, accept foo'; the signature doesn't
add any information.
Manuel said earlier that the source of the problem here is foo's
ambiguous type signature
(I'm switching back to the original, simplified example).
Type checking with ambiguous type signatures is hard because the type
checker has to guess
types and this guessing step may lead to too many
-cafe] type families and type signatures
Manuel said earlier that the source of the problem here is foo's ambiguous type
signature (I'm switching back to the original, simplified example).
Type checking with ambiguous type signatures is hard because the type checker
has to guess types
Let's look at this example from a higher level.
Haskell is a language which allows you to write type signatures for
functions, and even encourages you to do it.
Sometimes you even have to do it. Any language feature that stops me from
writing a type signature is in my opinion broken.
TFs as
I think it's not fair to say TFs as implemented in GHC are broken.
Fine, they are situations where the current implementation is overly
conservative.
The point is that the GHC type checker relies on automatic inference.
Hence, there'll
always be cases where certain reasonable type signatures
Claus Reinke wrote:
type family Id a
type instance Id Int = Int
foo :: Id a - Id a
foo = id n
foo' :: Id a - Id a
foo' = foo
type function notation is slightly misleading, as it presents
qualified polymorphic types in a form usually reserved for unqualified
polymorphic types.
rewriting
The point is that the GHC type checker relies on automatic inference.
Hence, there'll
always be cases where certain reasonable type signatures are rejected.
..
To conclude, any system with automatic inference will necessary reject
certain type signatures/instances
in order to guarantee
Claus Reinke wrote:
The point is that the GHC type checker relies on automatic inference.
Hence, there'll
always be cases where certain reasonable type signatures are rejected.
..
To conclude, any system with automatic inference will necessary
reject certain type signatures/instances
in
type family Id a
type instance Id Int = Int
foo :: Id a - Id a
foo = id n
foo' :: Id a - Id a
foo' = foo
type function notation is slightly misleading, as it presents
qualified polymorphic types in a form usually reserved for
unqualified polymorphic types.
rewriting foo's type helped me
On Wed, Apr 9, 2008 at 8:53 AM, Martin Sulzmann [EMAIL PROTECTED]
wrote:
Lennart, you said
(It's also pretty easy to fix the problem.)
What do you mean? Easy to fix the type checker, or easy to fix the program
by inserting annotations
to guide the type checker?
Martin
I'm referring
Claus Reinke:
type family Id a
type instance Id Int = Int
foo :: Id a - Id a
foo = id n
foo' :: Id a - Id a
foo' = foo
type function notation is slightly misleading, as it presents
qualified polymorphic types in a form usually reserved for
unqualified polymorphic types.
rewriting foo's
Lennart Augustsson:
On Wed, Apr 9, 2008 at 8:53 AM, Martin Sulzmann [EMAIL PROTECTED]
wrote:
Lennart, you said
(It's also pretty easy to fix the problem.)
What do you mean? Easy to fix the type checker, or easy to fix the
program by inserting annotations
to guide the type checker?
Lennart Augustsson:
Let's look at this example from a higher level.
Haskell is a language which allows you to write type signatures for
functions, and even encourages you to do it.
Sometimes you even have to do it. Any language feature that stops
me from writing a type signature is in my
Ganesh Sittampalam:
On Mon, 7 Apr 2008, Manuel M T Chakravarty wrote:
Ganesh Sittampalam:
The following program doesn't compile in latest GHC HEAD, although
it does if I remove the signature on foo'. Is this expected?
Yes, unfortunately, this is expected, although it is very
unintuitive.
Manuel Chakravarty wrote:
Ganesh Sittampalam:
On Mon, 7 Apr 2008, Manuel M T Chakravarty wrote:
Ganesh Sittampalam:
The following program doesn't compile in latest GHC HEAD, although
it does if I remove the signature on foo'. Is this expected?
Yes, unfortunately, this is expected, although
Sittampalam, Ganesh:
Manuel Chakravarty wrote:
Ganesh Sittampalam:
On Mon, 7 Apr 2008, Manuel M T Chakravarty wrote:
Ganesh Sittampalam:
The following program doesn't compile in latest GHC HEAD, although
it does if I remove the signature on foo'. Is this expected?
Yes, unfortunately, this
On Wed, 9 Apr 2008, Manuel M T Chakravarty wrote:
Sittampalam, Ganesh:
No, I meant can't it derive that equality when matching (Id a) against
(Id b)? As you say, it can't derive (a ~ b) at that point, but (Id a ~
Id b) is known, surely?
No, it is not know. Why do you think it is?
Well,
Id is an operation over types yielding a type, as such it doesn't make
much sense to me to have (Id a - Id a) but rather something like (a -
Id a). One could make this compile by adding the obvious instance:
type instance Id a = a
Curiously, is this a reduction from a real world use of
Ganesh Sittampalam:
The following program doesn't compile in latest GHC HEAD, although
it does if I remove the signature on foo'. Is this expected?
Yes, unfortunately, this is expected, although it is very
unintuitive. This is for the following reason.
Let's alpha-rename the signatures
On Sun, 6 Apr 2008, Thomas M. DuBuisson wrote:
Id is an operation over types yielding a type, as such it doesn't make
much sense to me to have (Id a - Id a) but rather something like (a -
Id a). One could make this compile by adding the obvious instance:
type instance Id a = a
Curiously,
On Mon, 7 Apr 2008, Manuel M T Chakravarty wrote:
Ganesh Sittampalam:
The following program doesn't compile in latest GHC HEAD, although it does
if I remove the signature on foo'. Is this expected?
Yes, unfortunately, this is expected, although it is very unintuitive.
This is for the
28 matches
Mail list logo
