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  2375 reads

Browse archivesActive forum topics 
Recent comments
47 min 18 sec ago
10 hours 52 min ago
16 hours 40 min ago
18 hours 21 min ago
1 day 4 hours ago
1 day 4 hours ago
1 day 5 hours ago
1 day 5 hours ago
1 day 6 hours ago
1 day 8 hours ago