type families and type signatures
Hi, The following program doesn't compile in latest GHC HEAD, although it does if I remove the signature on foo'. Is this expected? Cheers, Ganesh {-# LANGUAGE TypeFamilies #-} module Test7 where type family Id a type instance Id Int = Int foo :: Id a -> Id a foo = id foo' :: Id a -> Id a foo' = foo
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 families? I just can't think of how a (Fam a -> Fam a) function would be of use. Cheers, Thomas Ganesh Sittampalam wrote:
The following program doesn't compile in latest GHC HEAD, although it does if I remove the signature on foo'. Is this expected?
Cheers,
Ganesh
{-# LANGUAGE TypeFamilies #-} module Test7 where
type family Id a
type instance Id Int = Int
foo :: Id a -> Id a foo = id
foo' :: Id a -> Id a foo' = foo _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
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, is this a reduction from a real world use of families? I just can't think of how a (Fam a -> Fam a) function would be of use.
Yes, it's cut down from an example where (I think) I really need the type signature to specialise a general function that does do something useful. The generalised intstance above wouldn't be valid or sensible in that context. Cheers, Ganesh
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 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 valid to derive (a ~ b) from this. After all, Id could have the same result for different argument types. (That's not the case for your one instance, but maybe in another module, there are additional instances for Id, where that is the case.) Now, as GHC cannot show that a and b are the same, it can also not show that (Id a) and (Id b) are the same. It does look odd when you use the same type variable in both signatures, especially as Haskell allows you to leave out the quantifiers, but the 'a' in the signature of foo and the 'a' in the signatures of foo' are not the same thing; they just happen to have the same name. BTW, here is the equivalent problem using FDs: class IdC a b | a -> b instance IdC Int Int bar :: IdC a b => b -> b bar = id bar' :: IdC a b => b -> b bar' = bar Given that this is a confusing issue, I am wondering whether we could improve matters by giving a better error message, or an additional hint in the message. Do you have any suggestion regarding what sort of message might have helped you? Manuel
{-# LANGUAGE TypeFamilies #-} module Test7 where
type family Id a
type instance Id Int = Int
foo :: Id a -> Id a foo = id
foo' :: Id a -> Id a foo' = foo _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
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 following reason.
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 valid to derive (a ~ b) from this. After all, Id could have the same result for different argument types. (That's not the case for your one instance, but maybe in another module, there are additional instances for Id, where that is the case.)
Can't it derive (Id a ~ Id b), though?
Now, as GHC cannot show that a and b are the same, it can also not show that (Id a) and (Id b) are the same. It does look odd when you use the same type variable in both signatures, especially as Haskell allows you to leave out the quantifiers, but the 'a' in the signature of foo and the 'a' in the signatures of foo' are not the same thing; they just happen to have the same name.
Sure, but forall a . Id a ~ Id a is the same thing as forall b . Id b ~ Id b. Thanks for the explanation, anyway. I'll need to have another think about what I'm actually trying to do (which roughly speaking is to specialise a general function over type families using a signature which I think I need for other reasons). Generally speaking, is there any way to give a signature to foo'?
Given that this is a confusing issue, I am wondering whether we could improve matters by giving a better error message, or an additional hint in the message. Do you have any suggestion regarding what sort of message might have helped you?
I can't think of anything good. Perhaps printing out the (type classes + equalities) context would have helped me to see that it was empty and understand why, but probably not. Cheers, Ganesh
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. This is for the following reason.
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 valid to derive (a ~ b) from this. After all, Id could have the same result for different argument types. (That's not the case for your one instance, but maybe in another module, there are additional instances for Id, where that is the case.)
Can't it derive (Id a ~ Id b), though?
That's what it does derive as a proof obligation and finds it can't prove. The error message you are seeing is GHC's way of saying, I cannot assert that (Id a ~ Id b) holds.
Now, as GHC cannot show that a and b are the same, it can also not show that (Id a) and (Id b) are the same. It does look odd when you use the same type variable in both signatures, especially as Haskell allows you to leave out the quantifiers, but the 'a' in the signature of foo and the 'a' in the signatures of foo' are not the same thing; they just happen to have the same name.
Sure, but forall a . Id a ~ Id a is the same thing as forall b . Id b ~ Id b.
Thanks for the explanation, anyway. I'll need to have another think about what I'm actually trying to do (which roughly speaking is to specialise a general function over type families using a signature which I think I need for other reasons).
Generally speaking, is there any way to give a signature to foo'?
Sorry, but in the heat of explaining what GHC does, I missed the probably crucial point. Your function foo is useless, as is foo'. Not only can't you rename foo (to foo'), but you generally can't use it. It's signature is ambiguous. Try evaluating (foo (1::Int)). The problem is related to the infamous (show . read). Manuel
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' :: 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 very same type.
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 valid to derive (a ~ b) from this. After all, Id could have the same result for different argument types. (That's not the case for your one instance, but maybe in another module, there are additional instances for Id, where that is the case.)
While in general (Id a ~ Id b) -/-> (a ~ b) , parametricity makes it "true" in the case of foo . For instance, let Id a ~ Int . Then, the signature specializes to foo :: Int -> Int . But due to parametricity, foo does not care at all what a is and will be the very same function for every a with Id a ~ Int . In other words, it's as if the type variable a is not in scope in the definition of foo .
Now, as GHC cannot show that a and b are the same, it can also not show that (Id a) and (Id b) are the same. It does look odd when you use the same type variable in both signatures, especially as Haskell allows you to leave out the quantifiers, but the 'a' in the signature of foo and the 'a' in the signatures of foo' are not the same thing; they just happen to have the same name.
Since both type variables are quantified, the types as a whole are the same, alpha conversion notwithstanding.
BTW, here is the equivalent problem using FDs:
class IdC a b | a -> b instance IdC Int Int
bar :: IdC a b => b -> b bar = id
bar' :: IdC a b => b -> b bar' = bar
Hugs rejects bar as ambiguous whereas GHC accepts bar but rejects bar' . Something is wrong here. I think that only rejecting both definitions due to ambiguity is correct, since bar has access to a from the class. For instance, consider class C a b | a -> b fromA :: a -> b oneA :: a instance C Int Int where fromA = const 1 oneA = 1 instance C Char Int where fromA = const 2 oneA = 'a' bar :: C a b => b -> b bar _ = fromA oneA This definition is clearly ambiguous, bar could be 1 or 2. The subtle difference in the type synonym family case is that a is "more parametric" there. At least, that's my feeling. In full System F , neither definition would be a problem since the type a is an explicit parameter. Regards, apfelmus
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 very same type.
Type systems reject programs that don't go wrong. It's hard to understand on the basis of such a single program why it should be rejected. The problem is decidability. There is no algorithm that accepts all well-behaved programs and rejects all ill-behaved programs. There probably is an algorithm that accepts a particular program. So far we haven't found an algorithm that accepts this example, that is decidable and sufficiently general to cover many other useful cases. This is our motivation for rejecting this program. Consider it a challenge to find a better algorithm in the design space. Cheers, Tom -- Tom Schrijvers Department of Computer Science K.U. Leuven Celestijnenlaan 200A B-3001 Heverlee Belgium tel: +32 16 327544 e-mail: tom.schrijvers@cs.kuleuven.be url: http://www.cs.kuleuven.be/~toms/
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 sounds like your implementation may be using a relaxed approach to ambiguity checking that delays ambiguity checking from the point of definition to the point of use. Although this is probably still sound, it can lead to puzzling error diagnostics ... All the best, Mark Tom Schrijvers wrote:
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 very same type.
Type systems reject programs that don't go wrong. It's hard to understand on the basis of such a single program why it should be rejected. The problem is decidability. There is no algorithm that accepts all well-behaved programs and rejects all ill-behaved programs. There probably is an algorithm that accepts a particular program.
So far we haven't found an algorithm that accepts this example, that is decidable and sufficiently general to cover many other useful cases. This is our motivation for rejecting this program.
Consider it a challenge to find a better algorithm in the design space.
Cheers,
Tom
-- Tom Schrijvers
Department of Computer Science K.U. Leuven Celestijnenlaan 200A B-3001 Heverlee Belgium
tel: +32 16 327544 e-mail: tom.schrijvers@cs.kuleuven.be url: http://www.cs.kuleuven.be/~toms/ _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
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 types, and hence both would be rejected. It sounds like your implementation may be using a relaxed approach to ambiguity checking that delays ambiguity checking from the point of definition to the point of use. Although this is probably still sound, it can lead to puzzling error diagnostics ...
On the algorithmic level I don't see a relaxed approach to ambiguity checking. If alpha is a unifiction variable, you get for the first body (Id a -> Id a) ~ (alpha ~ alpha) where there is no ambiguity: the unique solution (modulo equality theory) is alpha := Id a. For the second body you get (Id a -> Id a) ~ (Id alpha -> Id alhpa) This equation reduces to Id a ~ Id alpha. Our algorithm stops here. There is in general no single solution for alpha (*) in such an equation, as opposed to the above case. I hope this clarifies our algorithm. Cheers, Tom
All the best, Mark
Tom Schrijvers wrote:
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 very same type.
Type systems reject programs that don't go wrong. It's hard to understand on the basis of such a single program why it should be rejected. The problem is decidability. There is no algorithm that accepts all well-behaved programs and rejects all ill-behaved programs. There probably is an algorithm that accepts a particular program.
So far we haven't found an algorithm that accepts this example, that is decidable and sufficiently general to cover many other useful cases. This is our motivation for rejecting this program.
Consider it a challenge to find a better algorithm in the design space.
Cheers,
Tom
-- Tom Schrijvers
Department of Computer Science K.U. Leuven Celestijnenlaan 200A B-3001 Heverlee Belgium
tel: +32 16 327544 e-mail: tom.schrijvers@cs.kuleuven.be url: http://www.cs.kuleuven.be/~toms/ _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
-- Tom Schrijvers Department of Computer Science K.U. Leuven Celestijnenlaan 200A B-3001 Heverlee Belgium tel: +32 16 327544 e-mail: tom.schrijvers@cs.kuleuven.be url: http://www.cs.kuleuven.be/~toms/
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 that a program has a well-defined semantics). 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' :: IdC a b => b -> b bar' = bar In this program, both bar and bar' have ambiguous types (the variable 'a' in each of the contexts is not uniquely determined by the variable 'b' appearing on the right), and so *neither* one of these definitions is valid. This behavior differs from what has been described for your approach, so perhaps Manuel's example isn't really "equivalent" after all. Technically, one could ignore the ambiguous type signature for bar, because the *principal* type of bar (as opposed to the *declared type*) is not ambiguous. However, in practice, there is little reason to allow the definition of a function with an ambiguous type because such functions cannot be used in practice: the ambiguity that is introduced in the type of bar will propagate to any other function that calls it, either directly or indirectly. For this reason, it makes sense to report the ambiguity at the point where bar is defined, instead of deferring that error to places where it is used, like the definition of bar'. (The latter is what I mean by "delayed" ambiguity checking.) Hope that helps, Mark Tom Schrijvers wrote:
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 types, and hence both would be rejected. It sounds like your implementation may be using a relaxed approach to ambiguity checking that delays ambiguity checking from the point of definition to the point of use. Although this is probably still sound, it can lead to puzzling error diagnostics ...
On the algorithmic level I don't see a relaxed approach to ambiguity checking.
If alpha is a unifiction variable, you get for the first body
(Id a -> Id a) ~ (alpha ~ alpha)
where there is no ambiguity: the unique solution (modulo equality theory) is alpha := Id a.
For the second body you get
(Id a -> Id a) ~ (Id alpha -> Id alhpa)
This equation reduces to Id a ~ Id alpha. Our algorithm stops here. There is in general no single solution for alpha (*) in such an equation, as opposed to the above case.
I hope this clarifies our algorithm.
Cheers,
Tom
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' :: IdC a b => b -> b bar' = bar
In this program, both bar and bar' have ambiguous types (the variable 'a' in each of the contexts is not uniquely determined by the variable 'b' appearing on the right), and so *neither* one of these definitions is valid. This behavior differs from what has been described for your approach, so perhaps Manuel's example isn't really "equivalent" after all.
Technically, one could ignore the ambiguous type signature for bar, because the *principal* type of bar (as opposed to the *declared type*) is not ambiguous. However, in practice, there is little reason to allow the definition of a function with an ambiguous type because such functions cannot be used in practice: the ambiguity that is introduced in the type of bar will propagate to any other function that calls it, either directly or indirectly. For this reason, it makes sense to report the ambiguity at the point where bar is defined, instead of deferring that error to places where it is used, like the definition of bar'. (The latter is what I mean by "delayed" ambiguity checking.)
You are of course spot on, but this is a difference in how GHC handles functional dependencies compared to Hugs. Hugs does reject bar as being ambiguous, but GHC does not! In other words, it also uses "delayed" ambiguity checking for the FD version, and so raises an error only when seeing bar'. The implementation of type families just mirrors GHC's behaviour for FDs. (This is why I presented the FD example, but I should have mentioned that the equivalence is restricted to GHC.) The rational for the decision to use delayed ambiguity checking in GHC is that it is, in general, not possible to spot and report all ambiguous signatures and *only* those. So, there are three possible choices: (1) Reject all signatures that *may* be ambiguous (and hence reject some perfectly good programs). (2) Reject all signatures that are *guaranteed* to be ambiguous (and accept some programs with functions that can never be applied). (3) Don't check for ambiguity (or "delayed" ambiguity checking). As you wrote, all three choices are perfectly safe - we will never accept a type-incorrect program, but they vary in terms of the range of accepted programs and quality of error messages. Please correct me if I am wrong, but as I understand the situation, Hugs uses Choice (1) and GHC uses Choice (3). As an example, consider this contrived program:
class F a b | a -> b where f1 :: a -> b f2 :: b -> a
instance F Int Int where f1 = id f2 = id
class G x a b where g :: x -> a -> b
instance F a b => G Bool a b where g c v = f1 v
instance F b a => G Int a b where g c v = f2 v
foo1 :: (G Int a b) => a -> a foo1 v = v
foo2 :: (G Bool a b) => a -> a foo2 v = v
bar = foo2 (42::Int)
Here foo1 is actually ambiguous, but foo2 is fine due to the FD in the instance context of the (G Bool a b) instance. GHC accepts this program (not checking for ambiguity) and allows you to evaluate bar. In contrast, Hugs rejects both the signature of foo1 and of foo2, arguably being overly restrictive with foo2. Cheers, Manuel
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 that a program has a well-defined semantics).
[...]
Technically, one could ignore the ambiguous type signature for bar, because the *principal* type of bar (as opposed to the *declared type*) is not ambiguous. However, in practice, there is little reason to allow the definition of a function with an ambiguous type because such functions cannot be used in practice: the ambiguity that is introduced in the type of bar will propagate to any other function that calls it, either directly or indirectly. For this reason, it makes sense to report the ambiguity at the point where bar is defined, instead of deferring that error to places where it is used, like the definition of bar'. (The latter is what I mean by "delayed" ambiguity checking.)
Thanks for explaining the ambiguity issue, Mark. I wasn't thinking about that. We have thought about ambiguity. See Section 7.3 in our paper http://www.cs.kuleuven.be/~toms/Research/papers/draft_type_functions_2008.pd... Note that neither Definition 3 nor Definition 4 demands that all unification variables are substituted with ground types during type checking. So we do allow for a form of ambiguity: when any type is valid (this has no impact on the semantics). Consider the initial program type family F a foo :: F a -> F a foo = id You propose to reject function Foo because it cannot be used unambiguously. We propose to accept foo, because the program could be extended with type instance F x = Int and, for instance, this would be valid: foo2 :: F Char -> F Bool foo2 = foo If you look at the level of the equality constraints: (F Char -> F Bool) ~ (F alpha -> F alpha) we normalise first wrt the instance F x = Int, and get (Int -> Int) ~ (Int -> Int) which is trivially true. In this process we do not substitute alpha. So alpha is ambiguous, but any solution will do and not have an impact on program execution. GHC already did this before type functions, for this kind of ambiguity, it substitutes alpha for an arbitrary type. That's not unreasonable, is it? Cheers, Tom -- Tom Schrijvers Department of Computer Science K.U. Leuven Celestijnenlaan 200A B-3001 Heverlee Belgium tel: +32 16 327544 e-mail: tom.schrijvers@cs.kuleuven.be url: http://www.cs.kuleuven.be/~toms/
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 is potentially ambiguous assuming we encounter instance Foo Int Char instance Foo Bool Char But such instances might never arise. See Tom's example below which applies an optimistic ambiguity check. In the extreme case, the optimistic ambiguity check only checks for ambiguity when calling the ground top-level function main. At this point (latest), we must provide (unambiguously) evidence for type classes and type equations. In summary: - The pessimistic ambiguity check is more in line with Haskell's open world view (of type classes and type families/functions being open/extensible). Anything can happen in the future (we might add an new type instances). So let's assume the worst and immediately report any potential ambiguity. - The optimistic ambiguity check takes into account the set of available instance. Depending on the set of instances there may not be any ambiguity after all. Both strategies are backed up by theoretical results. See the Coherence Theorems in Mark's thesis and "A Theory of Overloading" (I'm happy to provide more concrete pointers if necessary). Martin Tom Schrijvers wrote:
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 that a program has a well-defined semantics).
[...]
Technically, one could ignore the ambiguous type signature for bar, because the *principal* type of bar (as opposed to the *declared type*) is not ambiguous. However, in practice, there is little reason to allow the definition of a function with an ambiguous type because such functions cannot be used in practice: the ambiguity that is introduced in the type of bar will propagate to any other function that calls it, either directly or indirectly. For this reason, it makes sense to report the ambiguity at the point where bar is defined, instead of deferring that error to places where it is used, like the definition of bar'. (The latter is what I mean by "delayed" ambiguity checking.)
Thanks for explaining the ambiguity issue, Mark. I wasn't thinking about that. We have thought about ambiguity. See Section 7.3 in our paper
http://www.cs.kuleuven.be/~toms/Research/papers/draft_type_functions_2008.pd...
Note that neither Definition 3 nor Definition 4 demands that all unification variables are substituted with ground types during type checking. So we do allow for a form of ambiguity: when any type is valid (this has no impact on the semantics). Consider the initial program
type family F a
foo :: F a -> F a foo = id
You propose to reject function Foo because it cannot be used unambiguously. We propose to accept foo, because the program could be extended with
type instance F x = Int
and, for instance, this would be valid:
foo2 :: F Char -> F Bool foo2 = foo
If you look at the level of the equality constraints:
(F Char -> F Bool) ~ (F alpha -> F alpha)
we normalise first wrt the instance F x = Int, and get
(Int -> Int) ~ (Int -> Int)
which is trivially true. In this process we do not substitute alpha. So alpha is ambiguous, but any solution will do and not have an impact on program execution. GHC already did this before type functions, for this kind of ambiguity, it substitutes alpha for an arbitrary type. That's not unreasonable, is it?
Cheers,
Tom
-- Tom Schrijvers
Department of Computer Science K.U. Leuven Celestijnenlaan 200A B-3001 Heverlee Belgium
tel: +32 16 327544 e-mail: tom.schrijvers@cs.kuleuven.be url: http://www.cs.kuleuven.be/~toms/ _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
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 valid to derive (a ~ b) from this. After all, Id could have the same result for different argument types. (That's not the case for your one instance, but maybe in another module, there are additional instances for Id, where that is the case.)
While in general (Id a ~ Id b) -/-> (a ~ b) , parametricity makes it "true" in the case of foo . For instance, let Id a ~ Int . Then, the signature specializes to foo :: Int -> Int . But due to parametricity, foo does not care at all what a is and will be the very same function for every a with Id a ~ Int . In other words, it's as if the type variable a is not in scope in the definition of foo .
Be careful, Id is a type-indexed type family and *not* a parametric type. Parametricity does not apply. For more details about the situation with GADTs alone, see Foundations for Structured Programming with GADTs. Patricia Johann and Neil Ghani. Proceedings, Principles of Programming Languages 2008 (POPL'08).
In full System F , neither definition would be a problem since the type a is an explicit parameter.
You can't generally translate type family/GADT programs into System F. We proposed an extension of System F called System F_C(X); see our TLDI'07 paper: http://www.cse.unsw.edu.au/~chak/papers/SCPD07.html Manuel
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 *not* be valid to derive (a ~ b) from this. After all, Id could have the same result for different argument types. (That's not the case for your one instance, but maybe in another module, there are additional instances for Id, where that is the case.)
While in general (Id a ~ Id b) -/-> (a ~ b) , parametricity makes it "true" in the case of foo . For instance, let Id a ~ Int . Then, the signature specializes to foo :: Int -> Int . But due to parametricity, foo does not care at all what a is and will be the very same function for every a with Id a ~ Int . In other words, it's as if the type variable a is not in scope in the definition of foo .
Be careful, Id is a type-indexed type family and *not* a parametric type. Parametricity does not apply. For more details about the situation with GADTs alone, see
Foundations for Structured Programming with GADTs. Patricia Johann and Neil Ghani. Proceedings, Principles of Programming Languages 2008 (POPL'08).
Yes and no. In the GADT case, a function like bar :: forall a . GADT a -> String is clearly not "parametric" in a, in the sense that pattern matching on the GADT can specialize a which means that we have some form of "pattern matching" on the type a . The resulting String may depend on the type a . So, by "parametricity", I mean "type arguments may not be inspected". Likewise, bar :: forall a . Show a => Phantom a -> String is not parametric in a since the result may depend on the type a . 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 String = .. type instance Id Int = .. .. So, in the special case of foo and foo' , solving Id b ~ Id a by guessing a ~ b is safe since foo is parametric in a . Every guess is fine. I don't think that this can be squeezed into a type inference/checking algorithm, though.
In full System F , neither definition would be a problem since the type a is an explicit parameter.
You can't generally translate type family/GADT programs into System F. We proposed an extension of System F called System F_C(X); see our TLDI'07 paper:
Yes of course. I just wanted to remark that the whole ambiguity stuff is only there because we don't (want to) have explicit type application à la System F(_C(X)). Regards, apfelmus
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 String = .. type instance Id Int = .. ..
But in a degenerate case there could be just this one instance: type instance Id x = GADT x which then reduces this example to the GADT case of which you said that is was "clearly parametric". Tom -- Tom Schrijvers Department of Computer Science K.U. Leuven Celestijnenlaan 200A B-3001 Heverlee Belgium tel: +32 16 327544 e-mail: tom.schrijvers@cs.kuleuven.be url: http://www.cs.kuleuven.be/~toms/
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" of a definition like
type instance Id String = .. type instance Id Int = .. ..
But in a degenerate case there could be just this one instance:
type instance Id x = GADT x
which then reduces this example to the GADT case of which you said that is was "clearly parametric".
Manuel M T Chakravarty wrote:
type instance Id [a] = GADT a
Oh right, just setting the instance to a GADT makes it non-parametric. Still, it's not the type family that is the problem, but "parametricity" is not the right word for that. What I want to say is that although the type signature bar :: forall a . Id a ~ b => b -> String looks ambiguous, it is not. A trivial example of "seeming" ambiguity would be (foo :: forall a . Int) . Here, parametricity tells us that this is not ambiguous. The proper formulation is probably: a value f :: forall a . t is /unambiguous/ iff any choices a1, a2 for a that yield the same static type necessarily also yield the same dynamic value t[a1/a] = t[a2/a] -- types are equal => f @ a1 = f @ a2 -- values are equal In the case of bar , this would mean that anything not injective like type instance Id Int = Int type instance Id Char = Int would not change the dynamic semantics of bar at all, i.e. (bar @ Int :: Int -> String) = (bar @ Char :: Int -> String). I believe that this is indeed the case for bar and for type synonym families in general. (Not so for type classes, of course.) Regards apfelmus
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, it would *not* be valid to derive (a ~ b) from this. After all, Id could have the same result for different argument types. (That's not the case for your one instance, but maybe in another module, there are additional instances for Id, where that is the case.)
While in general (Id a ~ Id b) -/-> (a ~ b) , parametricity makes it "true" in the case of foo . For instance, let Id a ~ Int . Then, the signature specializes to foo :: Int -> Int . But due to parametricity, foo does not care at all what a is and will be the very same function for every a with Id a ~ Int . In other words, it's as if the type variable a is not in scope in the definition of foo . Be careful, Id is a type-indexed type family and *not* a parametric type. Parametricity does not apply. For more details about the situation with GADTs alone, see Foundations for Structured Programming with GADTs. Patricia Johann and Neil Ghani. Proceedings, Principles of Programming Languages 2008 (POPL'08).
Yes and no. In the GADT case, a function like
bar :: forall a . GADT a -> String
is clearly not "parametric" in a, in the sense that pattern matching on the GADT can specialize a which means that we have some form of "pattern matching" on the type a . The resulting String may depend on the type a . So, by "parametricity", I mean "type arguments may not be inspected". [..] 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 String = .. type instance Id Int = .. ..
So, in the special case of foo and foo' , solving Id b ~ Id a by guessing a ~ b is safe since foo is parametric in a .
We don't know that. We could have type instance Id [a] = GADT a Just looking at the signature, we don't know. Manuel
participants (8)
-
apfelmus -
Ganesh Sittampalam -
Manuel M T Chakravarty -
Mark P Jones -
Martin Sulzmann -
Stefan Monnier -
Thomas M. DuBuisson -
Tom Schrijvers