Tom Schrijvers wrote:
apfelmus wrote:
However, I have this feeling that
bar :: forall a . Id a - String
with a type family Id *is* parametric in the sense that no matter
what a is, the result always has to be the same. Intuitively, that's
because we may not pattern match on the branch
However, I have this feeling that
bar :: forall a . Id a - String
with a type family Id *is* parametric in the sense that no matter what a
is, the result always has to be the same. Intuitively, that's because we may
not pattern match on the branch of a definition like
type instance Id
Manuel M T Chakravarty wrote:
apfelmus:
Manuel M T Chakravarty wrote:
Let's alpha-rename the signatures and use explicit foralls for clarity:
foo :: forall a. Id a - Id a
foo' :: forall b. Id b - Id b
GHC will try to match (Id a) against (Id b). As Id is a type synonym
family, it would
apfelmus:
Manuel M T Chakravarty wrote:
apfelmus:
Manuel M T Chakravarty wrote:
Let's alpha-rename the signatures and use explicit foralls for
clarity:
foo :: forall a. Id a - Id a
foo' :: forall b. Id b - Id b
GHC will try to match (Id a) against (Id b). As Id is a type
synonym family,
Hi Tom,
It seems we are thinking of different things. I was referring to
the characterization of a type of the form P = t as being ambiguous
if there is a type variable in P that is not determined by the
variables in t; this condition is used in Haskell to establish
coherence (i.e., to show
The point is that Mark proposes a *pessimistic* ambiguity check whereas
Tom (as well as GHC) favors
an *optimistic* ambiguity check.
By pessimistic I mean that we immediately reject a program/type if
there's a potential
unambiguity. For example,
class Foo a b
forall a b. Foo a b = b - b
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'.
{-# LANGUAGE TypeFamilies #-}
module Test7 where
type family Id a
type instance Id Int = Int
foo :: Id a - Id a
foo = id
foo' ::
type instance Id Int = Int
foo :: Id a - Id a
foo = id
foo' :: Id a - Id a
foo' = foo
Is this expected?
Yes, unfortunately, this is expected, although it is very unintuitive.
This is for the following reason.
Huh? This sounds very wrong to me, simply because foo and foo' have the
The surprising thing about this example is the fact that
the definition of foo is accepted, and not the fact that
the definition of foo' is rejected. At least in Manuel's
equivalent program using functional dependencies, both
functions have ambiguous types, and hence both would be
rejected. It
On Mon, 7 Apr 2008, Mark P Jones wrote:
The surprising thing about this example is the fact that
the definition of foo is accepted, and not the fact that
the definition of foo' is rejected. At least in Manuel's
equivalent program using functional dependencies, both
functions have ambiguous
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).
Actually, it can make perfect sense: e.g. if the `Id' function acts as
a constraint.
Stefan
Hi Tom,
It seems we are thinking of different things. I was referring to
the characterization of a type of the form P = t as being ambiguous
if there is a type variable in P that is not determined by the
variables in t; this condition is used in Haskell to establish
coherence (i.e., to show
Hi Mark,
I don't know if you have defined/studied corresponding notions of
ambiguity/coherence in your framework. Instead, I was referring to
what Manuel described as the equivalent problem using FDs:
class IdC a b | a - b
instance IdC Int Int
bar :: IdC a b = b - b
bar = id
bar' ::
apfelmus:
Manuel M T Chakravarty wrote:
Ganesh Sittampalam:
Let's alpha-rename the signatures and use explicit foralls for
clarity:
foo :: forall a. Id a - Id a
foo' :: forall b. Id b - Id b
GHC will try to match (Id a) against (Id b). As Id is a type
synonym family, it would *not* be
14 matches
Mail list logo
