Hi, I'm trying to understand what fundeps do and don't let me do. One particular source of confusion is why the following program doesn't typecheck: {-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-} module Fundeps where class Dep a b | a -> b, b -> a conv :: (Dep a b1,Dep a b2) => b1 -> b2 conv = id {- end of program -} It seems as if inferring that b1 = b2 is precisely what "improvement" is about, but I'm not really sure when GHC actually applies that. Is there any documentation of that? I've read Mark Jones' paper, the haskell-prime wiki entry about Fundeps and the GHC manual but am still rather lost. Cheers, Ganesh
| I'm trying to understand what fundeps do and don't let me do. One | particular source of confusion is why the following program doesn't | typecheck: | | {-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-} | module Fundeps where | | class Dep a b | a -> b, b -> a | | conv :: (Dep a b1,Dep a b2) => b1 -> b2 | conv = id | {- end of program -} GHC implements "improvement" by *identifying* the two equal types. Here they cannot be identified because they are separate type variables. A good way to think of this is to imagine translating the program into System F: you can't do it. Functional dependencies guide type inference by adding extra unifications, resolving types that would otherwise be under-constrained and ambiguous -- but fundeps (or at least GHC's implementation thereof) does not deal with the case where the types become *over*-constrained. GHC's new intermediate language, System FC, is specifically designed to do this. Currently we're in transition: equality constraints are starting to work, but fundeps are implemented as they always were. I hope we can eventually switch over to implementing fundeps using equality constraints, and then the above program will work. Meanwhile, in the HEAD you can write conv :: (a~b) => a -> b conv = id Which, IHMO, is a much clearer way to say it! You may also like to try the paper that Martin and I and others wrote about fundeps: http://research.microsoft.com/%7Esimonpj/papers/fd-chr Simon
On Dec 3, 2007, at 4:02 AM, Simon Peyton-Jones wrote:
GHC's new intermediate language, System FC, is specifically designed to do this. Currently we're in transition: equality constraints are starting to work, but fundeps are implemented as they always were. I hope we can eventually switch over to implementing fundeps using equality constraints, and then the above program will work.
Meanwhile, in the HEAD you can write conv :: (a~b) => a -> b conv = id
Which, IHMO, is a much clearer way to say it!
Is it really a good idea to permit a type signature to include equality constraints among unifiable types? Does the above type signature mean something different from a ->a? Does the type signature: foo :: (a~Bar b) => a -> Bar b mean something different from: foo :: Bar b -> Bar b ? I know that System FC is designed to let us write stuff like: foo :: (Bar a ~ Baz b) => Bar a -> Baz b Which is of course what we need for relating type functions. But I'm wondering if there's a subtlety of using an equality constraint vs just substitution that I've missed---and if not why there are so many ways of writing the same type, many of them arguably unreadable! Hoping this will give me a bit of insight into SystemFC, -Jan-Willem Maessen
You may also like to try the paper that Martin and I and others wrote about fundeps: http://research.microsoft.com/%7Esimonpj/papers/fd-chr
Simon _______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
| Is it really a good idea to permit a type signature to include | equality constraints among unifiable types? Does the above type | signature mean something different from a ->a? Does the type signature: | foo :: (a~Bar b) => a -> Bar b | mean something different from: | foo :: Bar b -> Bar b | ? I know that System FC is designed to let us write stuff like: | foo :: (Bar a ~ Baz b) => Bar a -> Baz b | Which is of course what we need for relating type functions. But I'm | wondering if there's a subtlety of using an equality constraint vs | just substitution that I've missed No, you didn't miss anything. I wouldn't expect anyone to write these types directly. But it can happen: class C a b | a->b instance C Int Bool class D x where op :: forall y. C x y => x -> y instance D Int where op = ... In the (D Int) instance, what's the type of op? Well, it must be op :: forall y. C Int y => Int -> y And here we know that y=Bool; yet since we don't write the type sig directly we can't say it. So GHC's implementation of fundeps rejects this program; again it can't be translated into System F. Simon
On Mon, 3 Dec 2007, Simon Peyton-Jones wrote:
No, you didn't miss anything. I wouldn't expect anyone to write these types directly. But it can happen:
class C a b | a->b instance C Int Bool
class D x where op :: forall y. C x y => x -> y
instance D Int where op = ...
In the (D Int) instance, what's the type of op? Well, it must be op :: forall y. C Int y => Int -> y
And here we know that y=Bool; yet since we don't write the type sig directly we can't say it. So GHC's implementation of fundeps rejects this program; again it can't be translated into System F.
Conveniently, this is a good example of my other problem with fundeps :-) I can work around the problem from my first email with an unsafeCoerce, but is there any way I can get around the issue above at the moment in either 6.8 or the HEAD? I actually plan to recast the code in question using associated type synomyms once they're working properly, but would like to be able to make some progress now. Cheers, Ganesh
| > And here we know that y=Bool; yet since we don't write the type sig | > directly we can't say it. So GHC's implementation of fundeps rejects | > this program; again it can't be translated into System F. | | Conveniently, this is a good example of my other problem with fundeps :-) | I can work around the problem from my first email with an unsafeCoerce, | but is there any way I can get around the issue above at the moment in | either 6.8 or the HEAD? I actually plan to recast the code in question | using associated type synomyms once they're working properly, but would | like to be able to make some progress now. I think that if you use the HEAD, much of this will work, if you use the type-equality notation. But you will probably encounter bugs too. And in so doing, and reporting them, you'll be doing us a service. Simon
Jan-Willem Maessen:
Is it really a good idea to permit a type signature to include equality constraints among unifiable types? Does the above type signature mean something different from a ->a? Does the type signature: foo :: (a~Bar b) => a -> Bar b mean something different from: foo :: Bar b -> Bar b ? I know that System FC is designed to let us write stuff like: foo :: (Bar a ~ Baz b) => Bar a -> Baz b Which is of course what we need for relating type functions. But I'm wondering if there's a subtlety of using an equality constraint vs just substitution that I've missed---and if not why there are so many ways of writing the same type, many of them arguably unreadable!
Simon answered most of your question, but let me make a remark regarding "why there are so many ways of writing the same type, many of them arguably unreadable!" Equalities of the form "a ~ someType" are essentially a form of let-bindings for types - you can give a type a name and then use the name in place of the type. Just like with value-level let bindings, you can abuse the notation and write unreadable terms. However, this is no reason to remove let-bindings from the value level, so why should it be different at the type level? Manuel
conv :: (a~b) => a -> b conv = id
is there any particular reason that '~' is the symbol for type equality constraints? I would think '=' would be the obvious choice, (although perhaps it is already over-used, and is normally asymmetric in Haskell!)? Isaac
Nothing deep. Just that "=" means so many things that it seemed better to use a different notation. S | -----Original Message----- | From: glasgow-haskell-users-bounces@haskell.org [mailto:glasgow-haskell-users-bounces@haskell.org] On Behalf Of | Isaac Dupree | Sent: 04 December 2007 15:59 | To: Jan-Willem Maessen | Cc: Glasgow-haskell-users@haskell.org; Simon Peyton-Jones | Subject: type equality symbol | | >> conv :: (a~b) => a -> b | >> conv = id | | is there any particular reason that '~' is the symbol for type equality | constraints? I would think '=' would be the obvious choice, (although | perhaps it is already over-used, and is normally asymmetric in Haskell!)? | | Isaac | _______________________________________________ | Glasgow-haskell-users mailing list | Glasgow-haskell-users@haskell.org | http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
On Wed, 5 Dec 2007, Simon Peyton-Jones wrote:
Nothing deep. Just that "=" means so many things that it seemed better to use a different notation.
How about ==? Only one meaning so far, and that both on the term level and equivalent to the constraint. -- flippa@flippac.org Ivanova is always right. I will listen to Ivanova. I will not ignore Ivanova's recomendations. Ivanova is God. And, if this ever happens again, Ivanova will personally rip your lungs out!
| > Nothing deep. Just that "=" means so many things that it seemed better | > to use a different notation. | > | | How about ==? Only one meaning so far, and that both on the term level and | equivalent to the constraint I'm quite happy with "~"! It's sufficiently different from "=" that someone meeting it for the first time is going to thing "hmm, better read the manual"; and they'd be right. Anyway, while on this subject, I am considering making the following change: make all operator symbols into type constructors (currently they are type variables) That would allow you to write data a * b = Prod a b data a + b = Left a | Right b and write natural-looking types like f :: a*b -> a When we have indexed type families working, this will be even more natural. As things stand, only operators starting with a ":" are type constructors, thus data a :*: b = Prod a b etc. By analogy with the term language, operators are currently classified as "type variables", so you could write (oddly) data T (+) x = MkT (+) x [this may not even work today, but it should] to mean the same as data T y x = MkT y x But this is pretty useless! Very occasionally one might want a type variable with kind (*->*->*), but much much more often you want a type *constructor* with that kind. I thought I'd mention this here in case people have ideas. Simon
Simon Peyton-Jones wrote:
| > Nothing deep. Just that "=" means so many things that it seemed better | > to use a different notation. | > | | How about ==? Only one meaning so far, and that both on the term level and | equivalent to the constraint
I'm quite happy with "~"! It's sufficiently different from "=" that someone meeting it for the first time is going to thing "hmm, better read the manual"; and they'd be right.
I think this is the most important distinction: whether they will need to read the manual. I suppose it usually doesn't need to be written explicitly, so when it is, manual-reading (or a comment in the code) would be more likely to be important. (also (==) is generally a non-reserved symbol, though that could perhaps be changed like forall's (.))
Anyway, while on this subject, I am considering making the following change:
make all operator symbols into type constructors (currently they are type variables)
That would allow you to write data a * b = Prod a b data a + b = Left a | Right b and write natural-looking types like f :: a*b -> a
When we have indexed type families working, this will be even more natural.
As things stand, only operators starting with a ":" are type constructors, thus data a :*: b = Prod a b etc. By analogy with the term language, operators are currently classified as "type variables", so you could write (oddly) data T (+) x = MkT (+) x [this may not even work today, but it should] to mean the same as data T y x = MkT y x But this is pretty useless! Very occasionally one might want a type variable with kind (*->*->*), but much much more often you want a type *constructor* with that kind.
I've seen "~>" after (Arrow (~>)) =>, as a type variable... and find it confusing! for the (unimplementable) reverseArrow :: (Arrow a) => a b c -> a c b sometimes written as reverseArrow :: (Arrow (~>)) => (b ~> c) -> (c ~> b) , I'd prefer, if infix notation is going to be used, the backtick version for variables (as well as being allowed for types e.g. (b `SF` c)) reverseArrow :: (Arrow a) => (b `a` c) -> (c `a` b) Also, '->' doesn't start with a colon. (and is currently lowest-precedence, the way (::) in expressions is? or do we know what we're doing with precedences/associativity? To give infix declaration explicitly, must define (+)-type in a different module than (+)-value if it's different fixity...) I support that (+)-etc-as-type-constructor change! (hmm, is there any additional difficulty in it if experimenting with language features mixing type and term expressions - which already has lexical ambiguity anyway?) Isaac
Hello Simon, Wednesday, December 5, 2007, 7:05:22 PM, you wrote:
Anyway, while on this subject, I am considering making the following change: make all operator symbols into type constructors (currently they are type variables)
i like it. will the same apply to the type functions? i.e. will it be possible to define +, *, etc type functions? -- Best regards, Bulat mailto:Bulat.Ziganshin@gmail.com
Am Mittwoch, 5. Dezember 2007 17:05 schrieb Simon Peyton-Jones:
[…]
Anyway, while on this subject, I am considering making the following change:
make all operator symbols into type constructors (currently they are type variables)
This would be highly problematic! Concerning syntax, everything that holds for values should also hold for types. For values, identifiers starting with a capital letter and operators starting with a colon denote “constants”, everything else denotes variables. Exactly the same should hold for types since otherwise we would get a very confusing result. So we should keep things as they are concerning type constructors and type variables. And we should think about type functions being denoted by lower case identifiers and operators not starting with a colon because they are similar to non-constructor functions on the value level. We should strive for a systematic language and therefore not make ad-hoc decisions which for the moment seem to serve a purpose in some specific cases.
[…]
Best wishes, Wolfgang
I don't think it's highly problematic. I agree that it would be nice to
have the type and value levels have a similar structure, but if there are
compelling reasons to do otherwise that fine too.
You could still allow symbol type variables if they have an explicit binding
occurence, which you can always(?) do with type variables.
-- Lennart
On Dec 5, 2007 11:34 PM, Wolfgang Jeltsch
Am Mittwoch, 5. Dezember 2007 17:05 schrieb Simon Peyton-Jones:
[…]
Anyway, while on this subject, I am considering making the following change:
make all operator symbols into type constructors (currently they are type variables)
This would be highly problematic!
Concerning syntax, everything that holds for values should also hold for types. For values, identifiers starting with a capital letter and operators starting with a colon denote "constants", everything else denotes variables. Exactly the same should hold for types since otherwise we would get a very confusing result. So we should keep things as they are concerning type constructors and type variables. And we should think about type functions being denoted by lower case identifiers and operators not starting with a colon because they are similar to non-constructor functions on the value level.
We should strive for a systematic language and therefore not make ad-hoc decisions which for the moment seem to serve a purpose in some specific cases.
[…]
Best wishes, Wolfgang _______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Wolfgang Jeltsch:
Am Mittwoch, 5. Dezember 2007 17:05 schrieb Simon Peyton-Jones:
[…]
Anyway, while on this subject, I am considering making the following change:
make all operator symbols into type constructors (currently they are type variables)
This would be highly problematic!
Concerning syntax, everything that holds for values should also hold for types. For values, identifiers starting with a capital letter and operators starting with a colon denote “constants”, everything else denotes variables. Exactly the same should hold for types since otherwise we would get a very confusing result. So we should keep things as they are concerning type constructors and type variables. And we should think about type functions being denoted by lower case identifiers and operators not starting with a colon because they are similar to non-constructor functions on the value level.
The problem is that Haskell 98 already messed that up. If type functions are to use lower-case letters, vanilla type synonyms should use lower case-letters; eg, type string = [Char] Unfortunately, such a change would break about every single Haskell program. So, unless we make some rather drastic changes breaking backwards compatibility, we will not be able to get an entirely clean solution. Manuel
Simon Peyton-Jones:
Nothing deep. Just that "=" means so many things that it seemed better to use a different notation.
Also, using "=" would have entailed significant changes to GHC's parser. Type constraints are in the same syntactic category as types and types can appear as part of expressions in type annotations (such as "e::t") and on the lhs of let-bindings (such as "let x::t = e in e'"). Especially, considering the later, imagine "t" can now also contain the symbol "=" which in the grammar serves as a separator between the lhs and the rhs of a let bindings. I actually did try using "=", but it got too messy. Manuel
| -----Original Message----- | From: glasgow-haskell-users-bounces@haskell.org [mailto:glasgow-haskell-users-bounces@haskell.org ] On Behalf Of | Isaac Dupree | Sent: 04 December 2007 15:59 | To: Jan-Willem Maessen | Cc: Glasgow-haskell-users@haskell.org; Simon Peyton-Jones | Subject: type equality symbol | | >> conv :: (a~b) => a -> b | >> conv = id | | is there any particular reason that '~' is the symbol for type equality | constraints? I would think '=' would be the obvious choice, (although | perhaps it is already over-used, and is normally asymmetric in Haskell!)? | | Isaac | _______________________________________________ | Glasgow-haskell-users mailing list | Glasgow-haskell-users@haskell.org | http://www.haskell.org/mailman/listinfo/glasgow-haskell-users _______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Manuel M T Chakravarty wrote:
Simon Peyton-Jones:
Nothing deep. Just that "=" means so many things that it seemed better to use a different notation.
Also, using "=" would have entailed significant changes to GHC's parser. Type constraints are in the same syntactic category as types and types can appear as part of expressions in type annotations (such as "e::t") and on the lhs of let-bindings (such as "let x::t = e in e'"). Especially, considering the later, imagine "t" can now also contain the symbol "=" which in the grammar serves as a separator between the lhs and the rhs of a let bindings.
I actually did try using "=", but it got too messy.
oh, because it doesn't require parentheses: f :: a ~ b => a -> b f = id and also because, it sounds like you say, current parser looks at "type-class" and "type" expressions the same, so one doesn't really want to distinguish them just for this. x :: a = b => c = x really is too confusing, even if I can't see any way to make it ambiguous given current set of available language extensions. okay! Isaac
Isaac Dupree:
Manuel M T Chakravarty wrote:
Simon Peyton-Jones:
Nothing deep. Just that "=" means so many things that it seemed better to use a different notation.
Also, using "=" would have entailed significant changes to GHC's parser. Type constraints are in the same syntactic category as types and types can appear as part of expressions in type annotations (such as "e::t") and on the lhs of let-bindings (such as "let x::t = e in e'"). Especially, considering the later, imagine "t" can now also contain the symbol "=" which in the grammar serves as a separator between the lhs and the rhs of a let bindings. I actually did try using "=", but it got too messy.
oh, because it doesn't require parentheses: f :: a ~ b => a -> b f = id and also because, it sounds like you say, current parser looks at "type-class" and "type" expressions the same, so one doesn't really want to distinguish them just for this. x :: a = b => c = x really is too confusing, even if I can't see any way to make it ambiguous given current set of available language extensions.
For example, let {x :: t1 = t2 = e} in ... Now, this is not type correct, as x cannot have a type "t1 = t2", but the parser cannot know that. For the parser, a type constraint is a type like any other. Manuel
participants (9)
-
Bulat Ziganshin -
Ganesh Sittampalam -
Isaac Dupree -
Jan-Willem Maessen -
Lennart Augustsson -
Manuel M T Chakravarty -
Philippa Cowderoy -
Simon Peyton-Jones -
Wolfgang Jeltsch