Where are rank-3 types necessary in practice for maintaining abstraction?

newer
ThEdu'18: Second Call for Extended...

Timotej Tomandl

2 Apr 2018 2 Apr '18

11:36 p.m.

Hello, So we need rank-2 type in runST :: (forall s. ST https://hackage.haskell.org/package/base-4.11.0.0/docs/Control-Monad-ST.html... s a) -> a, to prevent s from appearing in a. I have been thinking about this for a bit, but I failed to come up with a practical situation, where rank-3 types are necessary for safety of some abstraction. The rank-3 example in here and any other I found, look very synthetic, i.e. limiting computation to id: https://ocharles.org.uk/blog/guest-posts/2014-12-18-rank-n-types.html and compared to the runST example of limiting a scope of a type variable for purposes of safety looks unnatural. Could anyone please point me to a practical example of rank-3 polymorphism, where it is necessary for safety of an abstraction, if it exists? I suspect there is a situation, where rank-3 is necessary for maintaining abstration exists, but I can't think of any. Any ideas about such situations and even better situations where this is used on hackage? Timotej Tomandl

Attachments:

attachment.html (text/html — 1.3 KB)

Show replies by date

Timotej Tomandl

3 Apr 3 Apr

2:54 a.m.

Ok, I thought about it a bit more and realized mask in Control.Exception is the one where rank-3 is necessary, which is the example I was looking for. Sorry for the spam. On Tue, Apr 3, 2018 at 4:36 AM, Timotej Tomandl wrote:

...

Hello,

So we need rank-2 type in runST :: (forall s. ST https://hackage.haskell.org/package/base-4.11.0.0/docs/Control-Monad-ST.html... s a) -> a, to prevent s from appearing in a.

I have been thinking about this for a bit, but I failed to come up with a practical situation, where rank-3 types are necessary for safety of some abstraction.

The rank-3 example in here and any other I found, look very synthetic, i.e. limiting computation to id: https://ocharles.org.uk/blog/guest-posts/2014-12-18-rank-n-types.html and compared to the runST example of limiting a scope of a type variable for purposes of safety looks unnatural. Could anyone please point me to a practical example of rank-3 polymorphism, where it is necessary for safety of an abstraction, if it exists?

I suspect there is a situation, where rank-3 is necessary for maintaining abstration exists, but I can't think of any. Any ideas about such situations and even better situations where this is used on hackage?

Timotej Tomandl

Joachim Durchholz

4:04 a.m.

New subject: Where are rank-3 types necessary in practice for maintaining abstraction?

Am 03.04.2018 um 08:54 schrieb Timotej Tomandl:

...

Ok, I thought about it a bit more and realized mask in Control.Exception is the one where rank-3 is necessary, which is the example I was looking for.

Given your newly acquired insights, do you expect that there will be ultimately a valid example for higher ranks? Is there a theoretical limit? Or a practical one? E.g. it might be too awkward to mentally handle higher-rank polymorphism - or maybe there's no real mental difference when dealing with higher-ranked polymorphism, I don't know because I didn't have to deal with that yet, so I'm curious.

...

Sorry for the spam.

Actually it was interesting. Regards, Jo

Alex Rozenshteyn

11:10 a.m.

New subject: Where are rank-3 types necessary in practice for maintaining abstraction?

There's an easy to read paper by Okasaki titled "Even higher-order functions for parsing or Why would anyone ever want to use a sixth-order function?". Unfortunatly I can't find a link to a non-paywalled version. It shows how parser combinators themselves use rank-3 types and how defining a monad instance requires rank-6. On Tue, Apr 3, 2018 at 1:05 AM Joachim Durchholz wrote:

...

Am 03.04.2018 um 08:54 schrieb Timotej Tomandl:

...
Ok, I thought about it a bit more and realized mask in Control.Exception is the one where rank-3 is necessary, which is the example I was looking for.

Given your newly acquired insights, do you expect that there will be ultimately a valid example for higher ranks? Is there a theoretical limit? Or a practical one? E.g. it might be too awkward to mentally handle higher-rank polymorphism - or maybe there's no real mental difference when dealing with higher-ranked polymorphism, I don't know because I didn't have to deal with that yet, so I'm curious.

...
Sorry for the spam.

Actually it was interesting.

Regards, Jo _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

Erik Hesselink

12:30 p.m.

New subject: Where are rank-3 types necessary in practice for maintaining abstraction?

The paper is here [1]. However, this is a sixth order function but not rank-6 polymorphism (rank 6 type) IIUC. Erik [1] https://www.westpoint.edu/eecs/SiteAssets/SitePages/ Faculty%20Publication%20Documents/Okasaki/jfp98sixth.pdf On 3 April 2018 at 17:10, Alex Rozenshteyn wrote:

...

There's an easy to read paper by Okasaki titled "Even higher-order functions for parsing or Why would anyone ever want to use a sixth-order function?". Unfortunatly I can't find a link to a non-paywalled version. It shows how parser combinators themselves use rank-3 types and how defining a monad instance requires rank-6.

On Tue, Apr 3, 2018 at 1:05 AM Joachim Durchholz wrote:

...
Am 03.04.2018 um 08:54 schrieb Timotej Tomandl:

...
Ok, I thought about it a bit more and realized mask in Control.Exception is the one where rank-3 is necessary, which is the example I was looking for.

Given your newly acquired insights, do you expect that there will be ultimately a valid example for higher ranks? Is there a theoretical limit? Or a practical one? E.g. it might be too awkward to mentally handle higher-rank polymorphism - or maybe there's no real mental difference when dealing with higher-ranked polymorphism, I don't know because I didn't have to deal with that yet, so I'm curious.

...
Sorry for the spam.

Actually it was interesting.

Regards, Jo _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

Alex Rozenshteyn

12:49 p.m.

New subject: Where are rank-3 types necessary in practice for maintaining abstraction?

Ah. My misrecollection. In that case, the highest rank example I can find is in "Practical type inference for arbitrary-rank types", and it's rank-3. On Tue, Apr 3, 2018, 09:30 Erik Hesselink wrote:

...

The paper is here [1]. However, this is a sixth order function but not rank-6 polymorphism (rank 6 type) IIUC.

Erik

[1] https://www.westpoint.edu/eecs/SiteAssets/SitePages/Faculty%20Publication%20...

On 3 April 2018 at 17:10, Alex Rozenshteyn wrote:

...
There's an easy to read paper by Okasaki titled "Even higher-order functions for parsing or Why would anyone ever want to use a sixth-order function?". Unfortunatly I can't find a link to a non-paywalled version. It shows how parser combinators themselves use rank-3 types and how defining a monad instance requires rank-6.

On Tue, Apr 3, 2018 at 1:05 AM Joachim Durchholz wrote:

...
Am 03.04.2018 um 08:54 schrieb Timotej Tomandl:

...
Ok, I thought about it a bit more and realized mask in Control.Exception is the one where rank-3 is necessary, which is the example I was looking for.

Given your newly acquired insights, do you expect that there will be ultimately a valid example for higher ranks? Is there a theoretical limit? Or a practical one? E.g. it might be too awkward to mentally handle higher-rank polymorphism - or maybe there's no real mental difference when dealing with higher-ranked polymorphism, I don't know because I didn't have to deal with that yet, so I'm curious.

...
Sorry for the spam.

Actually it was interesting.

Regards, Jo _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

David Feuer

11:35 p.m.

New subject: Where are rank-3 types necessary in practice for maintaining abstraction?

Take a look at this PR: https://github.com/haskell/primitive/pull/109/files The heterogeneous array creation functions I propose take rank-2 traversal functions as arguments and are therefore rank-3. In this case, the reason is a bit boring: the package in question can't depend on either (any?) of the packages offering rank-2 versions of Traversable. On Tue, Apr 3, 2018, 6:37 AM Timotej Tomandl wrote:

...

Hello,

So we need rank-2 type in runST :: (forall s. ST https://hackage.haskell.org/package/base-4.11.0.0/docs/Control-Monad-ST.html... s a) -> a, to prevent s from appearing in a.

I have been thinking about this for a bit, but I failed to come up with a practical situation, where rank-3 types are necessary for safety of some abstraction.

The rank-3 example in here and any other I found, look very synthetic, i.e. limiting computation to id: https://ocharles.org.uk/blog/guest-posts/2014-12-18-rank-n-types.html and compared to the runST example of limiting a scope of a type variable for purposes of safety looks unnatural. Could anyone please point me to a practical example of rank-3 polymorphism, where it is necessary for safety of an abstraction, if it exists?

I suspect there is a situation, where rank-3 is necessary for maintaining abstration exists, but I can't think of any. Any ideas about such situations and even better situations where this is used on hackage?

Timotej Tomandl _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

Edward Kmett

4 Apr 4 Apr

1:38 a.m.

New subject: Where are rank-3 types necessary in practice for maintaining abstraction?

The proper type for callCC would be rank-3. The current form is an under-approximation that only allows you to choose to use the continuation at one type. Going higher rank (usefully) is still pretty straight-forward. There is the Mendler-style encoding of functors that gets used every once in a while in recursion-schemes work. It adds a rank to get rid of a Functor constraint. This is basically replacing a functor f with (forall b. (a -> b) -> f b), which is the same as the Yoneda f a newtype. For more information, see some of the lovely examples in https://www.ioc.ee/~tarmo/papers/msfp08.pdf like update :: (forall c’. (forall y’. (y’ -> c’) -> (y’ -> Mu f) -> f y’ -> c’) -> y -> c’) -> (Mu f -> c) -> (forall c’. (forall y’. (y’ -> c) -> (y’ -> c’) -> f y’ -> c’) -> y -> c’) -Edward On Mon, Apr 2, 2018 at 11:36 PM, Timotej Tomandl wrote:

...

Hello,

So we need rank-2 type in runST :: (forall s. ST https://hackage.haskell.org/package/base-4.11.0.0/docs/Control-Monad-ST.html... s a) -> a, to prevent s from appearing in a.

I have been thinking about this for a bit, but I failed to come up with a practical situation, where rank-3 types are necessary for safety of some abstraction.

The rank-3 example in here and any other I found, look very synthetic, i.e. limiting computation to id: https://ocharles.org.uk/blog/guest-posts/2014-12-18-rank-n-types.html and compared to the runST example of limiting a scope of a type variable for purposes of safety looks unnatural. Could anyone please point me to a practical example of rank-3 polymorphism, where it is necessary for safety of an abstraction, if it exists?

I suspect there is a situation, where rank-3 is necessary for maintaining abstration exists, but I can't think of any. Any ideas about such situations and even better situations where this is used on hackage?

Timotej Tomandl

_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

2603

Age (days ago)

2604

Last active (days ago)

List overview

Download

7 comments

6 participants

participants (6)

Alex Rozenshteyn
David Feuer
Edward Kmett
Erik Hesselink
Joachim Durchholz
Timotej Tomandl

Where are rank-3 types necessary in practice for maintaining abstraction?

tags

participants (6)