John Hughes wrote: > What we need is different binding syntax for monomorphic and polymorphic > bindings. Roll on := and = ... I agree absolutely that we need such a distinction. Although it's worth clarifying a point. The monomorphism restriction doesn't exclude polymorphism, just overloading, e.g. I can bind `x = []' with no problem. So is your proposal to have := bind non-overloaded (and non-implicitly parameterized terms), or do you really mean that it will only bind monomorphic terms? (thus `x := []' would be problematic, unless there's a type sig). --Jeff My proposal is that := should bind *monomorphically* -- just like lambda binding. The motivation for that is that a polymorphic function can easily become overloaded after a small change to the program, such as adding removal of duplicate elements from a list. Such changes shouldn't cause wholesale differences in typing -- which the MR currently can. Another way to look at it is that = should imply type generalisation (including qualification), and := should mean no generalisation. It's a little odd to support *two kinds* of generalisation (with and without qualification). `x := []' wouldn't be problematic, just monomorphic. That is, x must be used consistently as a list of a particular type. But that need not prevent the type that x has from being inferred from its uses. John
John Hughes wrote: | `x := []' wouldn't be problematic, just monomorphic. | That is, x must be used consistently as a list of a | particular type. Just to check if I understand you correctly. In your proposal, does the following thing share `x'? let x = fac 100 in x + x (My understanding is that, in order to do this in your proposal, we have to say: let x := fac 100 in x + x Correct?) Does this also mean that it becomes impossible to share polymorphic values? I.e. the following contrived example will not behave as usual: wrong :: Either String a wrong = Left (show (fac 100)) -- not shared? example1 :: Either String Int example1 := do wrong return 1 example2 :: Either String Char example2 := do wrong return 'a' (With the usual Either monad instance.) Of course, in this case, there is a perfect remedy, just lifting out `show (fac 100', which is a monomorphic expression. However, this is not always possible, we might have a datatype like this: data PolyMonoList a = Poly Int (Foo a) | Mono a (Foo a) | Nil We can construct rather large polymorphic values, which have to be converted in linear time to the same value of a different type. I guess we already have the problem of not being able to share monomorphic values polymorphically. In fact, the Either monad instance is a good example: instance Monad (Either e) where return = Right Left x >>= k = Left x Right a >>= k = k a In the definition of `>>=', it is impossible to share `Left x'. /Koen.
On Thursday 25 October 2001 07:21 am, John Hughes wrote:
My proposal is that := should bind *monomorphically* -- just like lambda binding. The motivation for that is that a polymorphic function can easily become overloaded after a small change to the program, such as adding removal of duplicate elements from a list. Such changes shouldn't cause wholesale differences in typing -- which the MR currently can. Another way to look at it is that = should imply type generalisation (including qualification), and
:= should mean no generalisation. It's a little odd to support *two kinds*
of generalisation (with and without qualification).
`x := []' wouldn't be problematic, just monomorphic. That is, x must be used consistently as a list of a particular type. But that need not prevent the type that x has from being inferred from its uses.
Another place where `:=' bindings are badly needed is the recursive do-notation (mdo, as supported in hugs.) In an mdo, let bindings have to be monomorphic, because they are passed back to the mfix loop in a lambda binding. Hence, if we had :=, we can simply say that mdo only allows let bindings of the `:=' form, and that would clear up the whole issue. I'm no expert, but I think the new proposal for the arrow notation, if it allows recursive binding forms, can make use of this facility as well. Just take this as another vote in favor of `:=' bindings. -Levent.
On Thu, Oct 25, 2001 at 09:47:31AM +0000, Levent Erkok wrote:
Another place where `:=' bindings are badly needed is the recursive do-notation (mdo, as supported in hugs.) In an mdo, let bindings have to be monomorphic, because they are passed back to the mfix loop in a lambda binding. Hence, if we had :=, we can simply say that mdo only allows let bindings of the `:=' form, and that would clear up the whole issue.
I'm no expert, but I think the new proposal for the arrow notation, if it allows recursive binding forms, can make use of this facility as well.
Yes, let bindings in arrow notation must also be monomorphic, but it's nothing to do with recursion. It's because the value being defined is passed as input to the next arrow.
Hi! The binding form := must absolutely have a completely monomorphic type. A while back I posted the result that the MR kills principal types in Haskell. The problem with the MR is exactly that it introduces types which may be polymorphic but not overloaded. So if we want to regain principal types, := must be completely monomorphic. What we could have is that := is allowed to be polymorphic if and only if an explicit type signature is given. I do not thing this would hurt principality, and we could still have Koen's example, but like this: wrong :: Either String a wrong := Left (show (fac 100)) -- shared and polymorphic due to signature! example1 :: Either String Int example1 := do wrong return 1 example2 :: Either String Char example2 := do wrong return 'a' How does that sound? /kff
participants (5)
-
John Hughes -
Karl-Filip Faxen -
Koen Claessen -
Levent Erkok -
Ross Paterson