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