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

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
8 messages Options
Reply | Threaded
Open this post in threaded view
|

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

Timotej Tomandl-3
Hello,

So we need rank-2 type in runST :: (forall s. ST 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.
Reply | Threaded
Open this post in threaded view
|

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

Timotej Tomandl-3
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 <[hidden email]> wrote:
Hello,

So we need rank-2 type in runST :: (forall s. ST 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.
Reply | Threaded
Open this post in threaded view
|

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

Joachim Durchholz
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.
Reply | Threaded
Open this post in threaded view
|

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

Alex Rozenshteyn
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 <[hidden email]> 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.
Reply | Threaded
Open this post in threaded view
|

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

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

Erik

On 3 April 2018 at 17:10, Alex Rozenshteyn <[hidden email]> 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 <[hidden email]> 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.


_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

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

Alex Rozenshteyn
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 <[hidden email]> wrote:
The paper is here [1]. However, this is a sixth order function but not rank-6 polymorphism (rank 6 type) IIUC.

Erik

On 3 April 2018 at 17:10, Alex Rozenshteyn <[hidden email]> 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 <[hidden email]> 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.


_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

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

David Feuer
In reply to this post by Timotej Tomandl-3
Take a look at this PR:


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 <[hidden email]> wrote:
Hello,

So we need rank-2 type in runST :: (forall s. ST 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.

_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

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

Edward Kmett-2
In reply to this post by Timotej Tomandl-3
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 <[hidden email]> wrote:
Hello,

So we need rank-2 type in runST :: (forall s. ST 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.


_______________________________________________
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.