<div dir="ltr">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.<div><br></div><div>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.</div><div><br></div><div>For more information, see some of the lovely examples in <a href="https://www.ioc.ee/~tarmo/papers/msfp08.pdf">https://www.ioc.ee/~tarmo/papers/msfp08.pdf</a> like<br><br>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’)<br></div><div><br></div><div>-Edward</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Mon, Apr 2, 2018 at 11:36 PM, Timotej Tomandl <span dir="ltr"><<a href="mailto:timotomandl@gmail.com" target="_blank">timotomandl@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div>Hello,<br><br></div><div>So we need rank-2 type in <a id="m_-5180715040461405822gmail-v:runST" class="m_-5180715040461405822gmail-def">runST</a> :: (<span class="m_-5180715040461405822gmail-keyword">forall</span> s. <a href="https://hackage.haskell.org/package/base-4.11.0.0/docs/Control-Monad-ST.html#t:ST" title="Control.Monad.ST" target="_blank">ST</a> s a) -> a, to prevent s from appearing in a.<br></div><div><br>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.<br><br>The rank-3 example in here and any other I found, look very synthetic, i.e. limiting computation to id:<br><a href="https://ocharles.org.uk/blog/guest-posts/2014-12-18-rank-n-types.html" target="_blank">https://ocharles.org.uk/blog/<wbr>guest-posts/2014-12-18-rank-n-<wbr>types.html</a><br></div><div>and compared to the runST example of limiting a scope of a type variable for purposes of safety looks unnatural.<br></div><div>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?<br><br></div><div>I suspect there is a situation, where rank-3 is necessary for maintaining abstration exists, but I can't think of any.<br></div><div>Any ideas about such situations and even better situations where this is used on hackage?<span class="HOEnZb"><font color="#888888"><br></font></span></div><span class="HOEnZb"><font color="#888888"><div><br></div><div>Timotej Tomandl<br></div></font></span></div>
<br>______________________________<wbr>_________________<br>
Haskell-Cafe mailing list<br>
To (un)subscribe, modify options or view archives go to:<br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-<wbr>bin/mailman/listinfo/haskell-<wbr>cafe</a><br>
Only members subscribed via the mailman list are allowed to post.<br></blockquote></div><br></div>