Re: Rank2Types

Date: 2016-05-20 04:50 am (UTC)From: [personal profile] winterkoninkje
winterkoninkje: shadowcrane (clean) (Default)
No, Hugs supported both iirc. Though I vaguely recall something about Hugs being part of the reason why GHC followed suit about calling rank-2 special. Too vague to be helpful; mpj would know more.

Because of the issues about stability under extra annotations & decent error messages, if any compiler is going so far as to deal with rank-N types I'd say it's prolly good not to actually treat rank-2 specially (since this will be unintuitive to / unhelpful for users). It's more of a technical curiosity for folks who really care about fine-grained boundaries of power/provability, and are willing to sacrifice everything else to map out the cliff's edge. This used to be a big concern in the late 20th century, though I'm not sure how popular it is anymore. In CS circles at least we've kinda thrown all that to the wind and keep looking for more and more powerful systems (MLTT, CIC, IR, ...), willing to discard all but the most crucial forms of decidability (keeping only decidability of checking type-annotations, but even that is starting to show fault lines). Most pure logicians I know are similarly focused on other issues, whether they're following the CS folks or doing their own stuff. Don't hang out with enough philosophers to know what their current foci are.
From:
Anonymous( )Anonymous This account has disabled anonymous posting.
OpenID( )OpenID You can comment on this post while signed in with an account from many other sites, once you have confirmed your email address. Sign in using OpenID.
User
Account name:
Password:
If you don't have an account you can create one now.
Subject:
HTML doesn't work in the subject.

Message:

If you are unable to use this captcha for any reason, please contact us by email at support@dreamwidth.org


 
Notice: This account is set to log the IP addresses of everyone who comments.
Links will be displayed as unclickable URLs to help prevent spam.

April 2017

S M T W T F S
      1
2 345678
9101112131415
161718192021 22
23242526272829
30      

Tags

Page generated 30 May 2017 01:30 am
Powered by Dreamwidth Studios