User loginNavigation 
Interesting use cases for universal quantifiers in rank 2?Trevor Jim’s System P_{2} types the same terms as the secondrank System F_{2}, but function arguments can only be typed as (finite) intersections of simple types. This restriction is reasonable and also seems to correspond neatly to the inner workings of a compiler which specializes polymorphic functions for every usage (such as Rust’s, IIRC). What do we lose, relative to F_{2}? Here are the things that I can think of (in fact, they also apply to unrestricted System P, which prohibits universal quantifiers in negative positions):
Anything else? Side note: What is then the class of all datatypes whose induction principles fit into P_{2}? Is it interesting or any bigger than that for HM? I don’t understand what intersections could mean as eliminator arguments. By Alex Shpilkin at 20161023 00:23  LtU Forum  previous forum topic  next forum topic  other blogs  2154 reads

Browse archivesActive forum topics 
Recent comments
15 hours 15 min ago
15 hours 17 min ago
22 hours 36 min ago
1 day 13 hours ago
1 day 13 hours ago
1 day 14 hours ago
2 days 17 hours ago
2 days 22 hours ago
3 days 15 hours ago
3 days 17 hours ago