RE: rank 2-polymorphism and type checking
At 2001-10-24 01:08, Simon Peyton-Jones wrote:
So I'm interested to know: if GHC allowed arbitrarily-ranked types, who
would use them?
I would. Right now I have a class for 'IO lifted monads', that is, monads
from which one can call IO actions:
class (Monad m) = IOLiftedMonad m where
{
callIOWithMap :: ((m a - IO a) - IO b) - m b;
callIO :: IO a - m a;
callIO= callIOWithMap . const;
};
The 'callIOWithMap' function allows such things as 'catch' to be defined
over the monad:
class (IOLiftedMonad m) = IsJVMMonad m where
...
jvmCatch :: (IsJVMMonad m) = m a - (JThrowable - m a) - m a;
jvmCatch foo catchClause = callIOWithMap (\map - catch (map foo) (\x
- map (do
{
exRef - callIOWithEnv vmGetClearException;
noEx - callIO (getIsNothing exRef);
if noEx
then (callIO (ioError x))
else catchClause (MkJVMRef exRef);
})));
Now this is fine, because both occurences of 'map' have the same type.
But I recently discovered this doesn't work if the map is used with
different types. For instance, GHC 5.02 won't compile this:
test :: (IOLiftedMonad m) = m a - m b - m (a,b);
test ma mb = callIOWithMap (\map - do
{
a - map ma;
b - map mb;
return (a,b);
});
It looks like what I really need is this:
callIOWithMap :: ((forall a. (m a - IO a)) - IO b) - m b;
Is that correct? But GHC doesn't allow it...
--
Ashley Yakeley, Seattle WA
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell
RE: rank 2-polymorphism and type checking
Hello, and thanks for the various answers! Martin Odersky writes: Simon, You are correct to have doubts. Indeed our system would not handle this case, as type variables can only be instantiated to monomorophic types, not to type schemes. The closest you can get to it is to wrap the instance type in a type constructor. I.e. `t' could be instantiated to T (\c. forall d . (c-d) - d - d) where T was declared newtype T = T (\c. forall d . (c-d) - d - d) But I guess that does not solve Janis's problem. I'm not sure whether it would. To make things more complicated, the application I had in mind would not only require a rank-3 type and quantification over a type constructor, but also polymorphic recursion. Hmm, I wanted to use the free theorem of g's type, but rethinking I wonder what this actually *means* in the presence of quantification over type constructors. The whole story got so complicated, because I wanted to use a nested type of the form data D a = ... | forall b . F (b - a) (D b) If I settle for the less general but still useful data D a = ... | F (a - a) (D a) then I can do without any extensions :-) Regards, Janis. -- Janis Voigtlaender http://wwwtcs.inf.tu-dresden.de/~voigt/ mailto:[EMAIL PROTECTED] ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Re: rank 2-polymorphism and type checking
Iavor S. Diatchki writes: test :: (forall t . (forall a . t a) - t b) - b - b i am not an expert on this, but isnt this rank 3? Might be. Does this mean I cannot write it in Haskell? But, with data T a = C I can write: test' :: (forall t . (forall a . t a) - t b) - b - b test' g x = case g C of C - x Here, the type checker finds out on its own that t is instantiated to T. Still, why are the annotations in the following code not enough to let it also accept the definition of test (see my earlier message), respectively how can I tell it that t should be instantiated to t c = forall d . (c-d) - d - d ? test :: (forall t . (forall a . t a) - t b) - b - b test g x = (g :: (forall a . (forall d . (a-d) - d - d)) - (forall e . (b-e) - e - e)) ((\f y - y) :: (forall a . (forall d . (a-d) - d - d))) (id :: (b - b)) (x :: b) -- Janis Voigtlaender http://wwwtcs.inf.tu-dresden.de/~voigt/ mailto:[EMAIL PROTECTED] ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
RE: rank 2-polymorphism and type checking
Here's the story * GHC understands only rank-2 types; your type is rank 3 * The reason for this is that type inference for higher-rank types is tricky. GHC just squeezes through the door with rank-2 types by using a neat hack, but the hack just doesn't cope with higher ranks at all. * GHC 4.08 didn't *check* that the type is rank-2, whereas ghc 5.02 does. So all versions of your program will be rejected by GHC now, before it ever gets to type checking. * It's true that your test' *does* typecheck in GHC 4.08, but it's a coincidence! Certain very special programs will work even with higher rank types, but its jolly hard to explain which, so GHC 5 chucks them all out. * Nevertheless your program makes perfect sense. I believe that the Right Thing to do is to adopt Odersky/Laufer's idea of Putting Type Annotations To Work (POPL 96). They show how to typecheck arbitrarily high rank type provided there are enough type annotations, and Mark Shields has recently explained it all to me. But implementing this would be real work. So I'm interested to know: if GHC allowed arbitrarily-ranked types, who would use them? Simon | -Original Message- | From: Janis Voigtlaender [mailto:[EMAIL PROTECTED]] | Sent: 24 October 2001 08:00 | To: [EMAIL PROTECTED] | Subject: Re: rank 2-polymorphism and type checking | | | Iavor S. Diatchki writes: | |test :: (forall t . (forall a . t a) - t b) - b - b | i am not an expert on this, but isnt this rank 3? | | Might be. Does this mean I cannot write it in Haskell? But, with | | data T a = C | | I can write: | | test' :: (forall t . (forall a . t a) - t b) - b - b | test' g x = case g C of C - x | | Here, the type checker finds out on its own that t is | instantiated to T. Still, | why are the annotations in the following code not enough to | let it also accept | the definition of test (see my earlier message), | respectively how can I tell | it that t should be instantiated to t c = forall d . (c-d) | - d - d ? | | test :: (forall t . (forall a . t a) - t b) - b - b | test g x = (g :: (forall a . (forall d . (a-d) - | d - d)) - | (forall e . (b-e) - e - e)) | ((\f y - y) :: (forall a . (forall d . (a-d) - | d - d))) | (id :: (b - b)) | (x :: b) | | | -- | Janis Voigtlaender | http://wwwtcs.inf.tu-dresden.de/~voigt/ | mailto:[EMAIL PROTECTED] | | | ___ | Haskell mailing list | [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell | ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
RE: rank 2-polymorphism and type checking
Simon Peyton-Jones wrote: | So I'm interested to know: if GHC allowed | arbitrarily-ranked types, who would use them? I have certainly come across (very practical) situations where I would like to use rank-n types (with n 2). One example is the following. When using runST, I often end up with code that looks like: foo = runST ( do ... ... ... ) Because I think it is a bad idea to use parentheses like this, I would like to use $: foo = runST $ do ... ... ... Alas, the compiler complains, because it wants runST to have more arguments. So, one could define a special dollar operator: infixr 0 $+ ($+) :: ((forall s . m s a) - a) - (forall s . m s a) - a run $+ m = run m However, this has a rank-3 type. I have made the following observation. Richard Bird once wrote an article where he argues that allowing nested datatypes is useless unless one allows polymorphic recursion. I think the same is true for allowing functions with rank-2 polymorphism. If higher rank polymorphism is not allowed, then rank-2 polymorphic functions are just not first-class enough for all kinds of generalizations. /Koen ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Re: rank 2-polymorphism and type checking
So I'm interested to know: if GHC allowed arbitrarily-ranked types, who would use them? For Generic Haskell and for Generic Programming problems in general, arbitarily-ranked types would make life much easier. Therefore I guess that a couple of people here at Utrecht (including me) would highly appreciate such an extension. Best, Andres -- Andres Loeh, Universiteit Utrecht mailto:[EMAIL PROTECTED] mailto:[EMAIL PROTECTED] http://www.andres-loeh.de ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
RE: rank 2-polymorphism and type checking
PS to my earlier message. I am not at all certain that the Odersky/Laufer thing would in fact solve Janis's problem. You want not only a rank-3 type, but also higher-order unification, since you want to instantiate 't' to \c. forall d . (c-d) - d - d That may just be too hard. But I'm out of my depth here. Maybe a types expert can help. Simon | -Original Message- | From: Simon Peyton-Jones [mailto:[EMAIL PROTECTED]] | Sent: 24 October 2001 09:08 | To: Janis Voigtlaender; [EMAIL PROTECTED] | Subject: RE: rank 2-polymorphism and type checking | | | Here's the story | | * GHC understands only rank-2 types; your type is rank 3 | | * The reason for this is that type inference for higher-rank | types is tricky. |GHC just squeezes through the door with rank-2 types by | using a neat |hack, but the hack just doesn't cope with higher ranks at all. | | * GHC 4.08 didn't *check* that the type is rank-2, whereas | ghc 5.02 does. | So all versions of your program will be rejected by GHC now, before | it ever gets to type checking. | | * It's true that your test' *does* typecheck in GHC 4.08, but | it's a coincidence! | Certain very special programs will work even with higher | rank types, but |its jolly hard to explain which, so GHC 5 chucks them all out. | | * Nevertheless your program makes perfect sense. I believe | that the Right | Thing to do is to adopt Odersky/Laufer's idea of Putting | Type Annotations |To Work (POPL 96). They show how to typecheck | arbitrarily high rank |type provided there are enough type annotations, and Mark | Shields has |recently explained it all to me. But implementing this | would be real work. | | So I'm interested to know: if GHC allowed arbitrarily-ranked | types, who would use them? | | Simon | | | | | -Original Message- | | From: Janis Voigtlaender [mailto:[EMAIL PROTECTED]] | | Sent: 24 October 2001 08:00 | | To: [EMAIL PROTECTED] | | Subject: Re: rank 2-polymorphism and type checking | | | | | | Iavor S. Diatchki writes: | | | |test :: (forall t . (forall a . t a) - t b) - b - b | | i am not an expert on this, but isnt this rank 3? | | | | Might be. Does this mean I cannot write it in Haskell? But, with | | | | data T a = C | | | | I can write: | | | | test' :: (forall t . (forall a . t a) - t b) - b - b | test' g x = | | case g C of C - x | | | | Here, the type checker finds out on its own that t is | | instantiated to T. Still, | | why are the annotations in the following code not enough to | | let it also accept | | the definition of test (see my earlier message), | | respectively how can I tell | | it that t should be instantiated to t c = forall d . (c-d) | | - d - d ? | | | | test :: (forall t . (forall a . t a) - t b) - b - b | | test g x = (g :: (forall a . (forall d . (a-d) - | | d - d)) - | | (forall e . (b-e) - e - e)) | | ((\f y - y) :: (forall a . (forall d . (a-d) - | | d - d))) | | (id :: (b - b)) | | (x :: b) | | | | | | -- | | Janis Voigtlaender | | http://wwwtcs.inf.tu-dresden.de/~voigt/ | | mailto:[EMAIL PROTECTED] | | | | | | ___ | | Haskell mailing list | | [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell | | | | ___ | Haskell mailing list | [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell | ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
RE: rank 2-polymorphism and type checking
PS to my earlier message. I am not at all certain that the Odersky/Laufer thing would in fact solve Janis's problem. You want not only a rank-3 type, but also higher-order unification, since you want to instantiate 't' to \c. forall d . (c-d) - d - d Simon, You are correct to have doubts. Indeed our system would not handle this case, as type variables can only be instantiated to monomorophic types, not to type schemes. The closest you can get to it is to wrap the instance type in a type constructor. I.e. `t' could be instantiated to T (\c. forall d . (c-d) - d - d) where T was declared newtype T = T (\c. forall d . (c-d) - d - d) But I guess that does not solve Janis's problem. Cheers -- Martin ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Re: rank 2-polymorphism and type checking
Simon Peyton-Jones [EMAIL PROTECTED] writes: So I'm interested to know: if GHC allowed arbitrarily-ranked types, who would use them? I can't promise that I would use them, but it would certainly give me warm fuzzy feelings to know that they were there. :-) On the other hand, I believe that you can construct in GHC a type which is isomorphic to any arbitrarily-ranked type (with any combination of existential and universal quantification) by creating new data constructors. If this is true, then I'm reasonably content with that. Carl Witty ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Re: rank 2-polymorphism and type checking
hi test :: (forall t . (forall a . t a) - t b) - b - b i am not an expert on this, but isnt this rank 3? bye iavor -- == | Iavor S. Diatchki, Ph.D. student | | Department of Computer Science and Engineering | | School of OGI at OHSU | | http://www.cse.ogi.edu/~diatchki | == ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
