I don't have a specific application that's crying out for this, but I sometimes shy away from using higher-rank polymorphism because of the extra effort it can require. A possibly related question is whether you would expect to make record selectors and updaters work for all record types at the same time? That would definitely be very useful. -----Original Message----- From: glasgow-haskell-users-bounces@haskell.org [mailto:glasgow-haskell-users-bounces@haskell.org] On Behalf Of Simon Peyton-Jones Sent: 10 September 2008 15:25 To: Wolfgang Jeltsch; glasgow-haskell-users@haskell.org Cc: Dimitrios Vytiniotis (t-dimitv@microsoft.com) Subject: RE: Is FPH implemented in GHC? Not yet. But Dimitrios has just started a postdoc at MSR, so we will be working on fixing, once and for all, the impredicative story in GHC. Meanwhile, why do you ask? Making impredicative polymorphism work seems to be the Right Thing, but it's something of a "technology push", perhpas a solution in search of a problem. Do you have an application that needs it? This is a general question to GHC users. (If you don't know what impredicative polymorphism is, think "can I have a type like (Maybe (forall a. [a] -> [a]))".) Simon | -----Original Message----- | From: glasgow-haskell-users-bounces@haskell.org | [mailto:glasgow-haskell-users- bounces@haskell.org] On Behalf Of | Wolfgang Jeltsch | Sent: 10 September 2008 15:21 | To: glasgow-haskell-users@haskell.org | Subject: Is FPH implemented in GHC? | | Hello, | | is FPH implemented in GHC? If yes, will it be part of GHC 6.10.1? | | Best wishes, | Wolfgang | _______________________________________________ | 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 ============================================================================== Please access the attached hyperlink for an important electronic communications disclaimer: http://www.credit-suisse.com/legal/en/disclaimer_email_ib.html ==============================================================================

| A possibly related question is whether you would expect to make record | selectors and updaters work for all record types at the same time? | That would definitely be very useful.

I'm not sure what you mean by this. Would you care to elaborate?

The most important thing for me is supporting record update for existentially quantified data records, as in the error below. In general I also find working with code that involves existential type variables quite hard work - for example I can't use foo as a record selector either, even if I immediately do something that seals the existential type back up again. I don't understand this stuff well enough to be sure whether it's an impredicativity issue or not, though. Cheers, Ganesh Foo.hs:11:8: Record update for the non-Haskell-98 data type `Foo' is not (yet) supported Use pattern-matching instead In the expression: rec {foo = id} In the definition of `f': f rec = rec {foo = id} {-# LANGUAGE Rank2Types #-} module Foo where data Foo = forall a . Foo { foo :: a -> a, bar :: Int } x :: Foo x = Foo { foo = id, bar = 3 } f :: Foo -> Foo f rec = rec { foo = id } g :: Foo -> Foo g rec = rec { bar = 3 } ============================================================================== Please access the attached hyperlink for an important electronic communications disclaimer: http://www.credit-suisse.com/legal/en/disclaimer_email_ib.html ==============================================================================

Am Mittwoch, 10. September 2008 16:24 schrieben Sie:

[…]

Meanwhile, why do you ask? Making impredicative polymorphism work seems to be the Right Thing, but it's something of a "technology push", perhpas a solution in search of a problem. Do you have an application that needs it?

Hello Simon, yes, I have one. It’s the Grapefruit FRP library. The background is as follows: If an FRP library provides first-class signals then often the problem arises that these are actually signal generators—their behavior might depend on the time they are started. To get rid of this deficiency, my signal types now have an additional type argument which denotes the starting time. This way, I’m able to fix the starting time using the type system. The idea is similar to the usage of the “state” type argument of ST. Now I have a switching combinator which takes a signal of signal transformations (a time-varying signal transformation). The signal transformations have to work with different starting times, so I use an explicit forall and get a type like SSignal t (forall t'. SignalFun t' a). To implement all this stuff, I had to do quite a bit of code obfuscation. That is, I introduced a lot of trivial functions only to give them an explicit impredicative/rank 2 type signature. Maybe my solution isn’t optimal but I didn’t see how to do this simpler. I hope that FPH will reduce the extra effort, I have to spend, dramatically. If you have further questions, please ask. Best wishes, Wolfgang

Am Donnerstag, 11. September 2008 00:09 schrieben Sie:

...

If an FRP library provides first-class signals then often the problem arises that these are actually signal generators—their behavior might depend on the time they are started. To get rid of this deficiency, my signal types now have an additional type argument which denotes the starting time. This way, I’m able to fix the starting time using the type system. The idea is similar to the usage of the “state” type argument of ST.

Dependencies on an absolute clock always caused trouble in Fran/FRP programming and were one of the things I tried to get rid of in my FunWorlds experiments (sigh, way too long ago..).

Hmm, maybe you misunderstood. The extra type argument cannot be instantiated to the current time since that would need dependent types or something similar. Actually, we never instantiate this argument but only force it to be independent to other such time arguments via forall, and force it to be equal to other such time arguments by using the same type variable multiple times in the same type. So the whole thing is only about whether something happens at the same time or not. It’s really similar to the first ST type argument without using RealWorld. You never instantiate it, you just put constraints on it in the form that it has to be equal to some other such argument.

Thinking of behaviours as functions from *all* times to values is an unimplementable theoretical ideal and completely at odds with FRP's more practical ideal of compositional programming (leading to the less sung about "arts" of actual programming in FRP, aging behaviours, start times, etc.).

At least, I try to help the FRP programmer to get aging etc. right by using the time argument trick to make wrong signal use result in a type error. In Grapefruit, a signal is a function from a time *interval* to values where the time interval is denoted by this type argument.

[…]

Many of the FunWorlds aspects would need revision, if I ever get round to that.. but dropping absolute time was the right thing to do (as if physics hadn't told us about that anyway;-).

In Grapefruit, you could implement a continous signal which represents an absolute clock. This is because you can make a continuous signal out of any continuous source that can be asked to tell its current value by means of an I/O action. But absolute time isn’t fundamental to Grapefruit. You could think of some totally ordered set representing time and continuous signals being functions from this set to values. But you can only access continuous signals by sampling them using a discrete signal. So you can only get the value of a continous signal at those times where some event occurs. You have the advantage that you can abstract from sampling rates and similar stuff by composing continuous signals. But at some point you have to sample explicitely.

Claus

Best wishes, Wolfgang