Simon Peyton Jones answered me:

| > do { a <- getChar | > ; rec { b <- f c | > ; c <- g b } | > ; putChar c | > ; return b }

| This last point notwithstanding, | I find the scoping rules very unintuitive! | (b and c appear to escape their apparently nested scope.)

well you are happy with ^^^^^

(Let's say: I got used to it...)

do { z <- getChar ; let { b = f c ; c = g b } ; putChar c ; return b }

It's just the same!

Indeed; I had not noticed that. (I am spoilt by layout, and had never ``seen'' those braces before.) However, if you write those braces, there is no reason anymore to omit the ``in do'' at the end! This variant of let is only motivated by layout... Analogously, is | > do { a <- getChar | > ; rec { b <- f c | > ; c <- g b } | > ; putChar c | > ; return b } equivalent to | > do { a <- getChar | > ; rec { b <- f c | > ; c <- g b } in do | > { putChar c | > ; return b } ? Is | > do { rec { b <- f c | > ; c <- g b } | > ; putChar c | > ; return b } equivalent to | > rec { b <- f c | > ; c <- g b } in do | > { putChar c | > ; return b } ? Would ``dorec'', in analogy with ``letrec'', perhaps be a better name? Wolfram

Friends One more update about GHC 6.12, concerning impredicative polymorphism. GHC has had an experimental implementation of impredicative polymorphism for a year or two now (flag -XImpredicativePolymorphism). But a) The implementation is ridiculously complicated, and the complexity is pervasive (in the type checker) rather than localized. I'm very unhappy about this, especially as we add more stuff to the type checker for type families. b) The specification (type system) is well-defined [1], but is also pretty complicated, and it's just too hard to predict which programs will typecheck and which will not. So it's time for a re-think. I propose to deprecate it in 6.12, and remove it altogether in 6.14. We may by then have something else to put in its place. (There is no lack of candidates [2,3,4]!) Fortunately, I don't think a lot of people use the feature in anger. Please yell if you *are* using impredicative polymorphism for something serious. But if you are, we need to think of a workaround. The current situation seems unsustainable. Simon [1] http://research.microsoft.com/en-us/um/people/simonpj/papers/boxy/ [2] http://research.microsoft.com/en-us/um/people/crusso/qml/ [3] http://research.microsoft.com/en-us/um/people/daan/pubs.html [4] http://gallium.inria.fr/~remy/mlf/

On Fri, 30 Oct 2009, Sittampalam, Ganesh wrote:

Simon Peyton-Jones wrote:

...

Fortunately, I don't think a lot of people use the feature in anger. Please yell if you *are* using impredicative polymorphism for something serious. But if you are, we need to think of a workaround. The current situation seems unsustainable.

I think darcs is using it. At least, I had to enable ImpredicativePolymorphism to successfully build darcs with GHC 6.11 (a snapshot from about February), although the flag is not required with GHC 6.10. I haven't had a chance to try with the RC yet, but will do this weekend.

I'll have to check the full details of why it's needed, but from memory I think it can be worked around at the cost of more verbosity by using some newtypes in appropriate places.

OK, I confirm the changes are fairly trivial. The main issue is that a couple of functions want to instantiate the argument to IO with a type scheme: restrictBoring :: IO (forall t m. FilterTree t m => t m -> t m) The newtype workaround works fine here and doesn't affect too much of the code. In one other place some code had type [(String, Foo)] where Foo is a type synonym for (forall x y . <something>), but it turned out the nested quantification wasn't required so (forall x y . [(String, <something>)]) was ok in this case, if a little uglier. (Patch sent to darcs-users) Cheers, Ganesh

| Is there any difference between "-XImpredicativePolymorphism" and "- | XImpredicativeTypes"? No there isn't. There's only one flag, -XImpredicativeTypes. | Hyena uses the latter, and we're using Hyena somewhat "in anger". Interesting. I hope you can get along without it, perhaps with a bit more newtype wrapping/unwrapping code. As I say, the current situation is not good. Simon

On Friday 30 October 2009 5:51:37 am Simon Peyton-Jones wrote:

One more update about GHC 6.12, concerning impredicative polymorphism.

GHC has had an experimental implementation of impredicative polymorphism for a year or two now (flag -XImpredicativePolymorphism). But

a) The implementation is ridiculously complicated, and the complexity is pervasive (in the type checker) rather than localized. I'm very unhappy about this, especially as we add more stuff to the type checker for type families.

b) The specification (type system) is well-defined [1], but is also pretty complicated, and it's just too hard to predict which programs will typecheck and which will not.

So it's time for a re-think. I propose to deprecate it in 6.12, and remove it altogether in 6.14. We may by then have something else to put in its place. (There is no lack of candidates [2,3,4]!)

This may be a side issue, but... Someone was asking in #haskell yesterday about what exactly ImpredicativeTypes did, as it's a bit difficult to tell at first. I eventually came to the conclusion that some of the notation GHC uses may be rather poor. In a lambda cube/pure type system setting, the difference between an impredicative and predicative system are the rules: ([], *, *) vs. ([], *, []) Where the first rule says that, for instance: (Pi a:*. a -> a) : * while the second says: (Pi a:*. a -> a) : [] The first is impredicative due to * containing (Pi a:*. a -> a) itself, so the expression quantifies over a 'set' containing itself. But, if we ask GHC the kind of: forall a. a -> a it tells us the answer is *, even without ImpredicativeTypes. But that *looks* like a statement that the type system is impredicative already. And in fact, we can stick a signature on the identity function like: id :: (forall a. a -> a) -> (forall a. a -> a) which appears to allow impredicative instantiation of variables as long as they're only used in functions. But, of course, this fails for datatypes without the relevant flag. Maybe :: * -> *, but we're not allowed to apply it to (forall a. a -> a), even though GHC tells us the latter has type * (although, asking the kind of Maybe (forall a. a -> a) does not blow up; only trying to use it as a type does). At some point in the discussion, someone quoted from the boxy paper that in HM, quantification ranges over monotypes. Presumably, GHC maintains such a distinction internally, which is roughly analogous[1] to tracking the difference between * and []. But, when it comes time to display sorts, it shows both * and [] as *, which makes it somewhat unclear why Maybe (forall a. a) is invalid. So, to get to the point, whatever implementation is decided upon in the future, if predicativity is still around, I think it'd be useful to make that predicativity noticeable in the types/kinds/sorts, rather than the current situation, which to an observer looks like, "* contains both monotypes and polytypes, but quantification over * only really ranges over the monotypes (maybe)." I don't know how this would complicate GHC's current kind system, as I know it isn't set up like a pure type system, but it might be something to think about. Cheers, -- Dan [1] It probably isn't a perfect correspondence. For instance (based on my experience implementing rather naive interpreters), in a predicative, lambda cube F2, the type: forall a. forall b. a -> b is invalid, because 'forall b. a -> b' has sort [], and so the additional quantifier requires the rule ([],[],[]), which gets you to Fomega. forall a. (forall b. b) -> a = (forall b. b) -> (forall a. a) are similarly invalid. But, it feels a bit accidental to me that the Fomega rule allows these, so one could probably keep a sort divide between monotypes and polytypes while allowing repeated and higher-rank quantification, and also not allowing higher-order types (although Haskell has the latter anyway).

| Hello Simon and others, | | unfortunately, I missed this e-mail. | | Yes, removal of impredicative polymorphism hurts me, since impredicativity | plays a crucial role in the Grapefruit FRP library at the moment. This is | described in section 5 of my paper “Signals, Not Generators!” [5]. It’s | probably possible to use a workaround involving a newtype wrapper, in case | polymorphic fields in newtypes are still supported. However, this makes things | more awkward for library users. I plan to support impredicative polymorphism in some form; but you may need more type annotations. I'll announce when there's something to test (it'll be a couple of months). Simon

Is there a good motivating example for recursive do? So far, I haven't grokked the various use cases, which are pretty terse. Maybe the syntax sugar gets in the way (dangling lets are a good case in point). It's a bit like grokking a Monad: it's the way to alter state, through a chain of binds, culminating in a return, where values can't escape outside the Monad itself. Using IO as the example w/the (hidden) realworld parameter makes the explanation more opaque than it need be. -scooter Sent from my Verizon Wireless BlackBerry -----Original Message----- From: Greg Fitzgerald Date: Thu, 29 Oct 2009 10:24:23 To: Simon Peyton-Jones Cc: GHC users Subject: Re: Update on GHC 6.12.1 _______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users