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

Browse archivesActive forum topics 
Recent comments
11 hours 11 min ago
11 hours 15 min ago
11 hours 25 min ago
13 hours 4 min ago
1 day 8 hours ago
1 day 8 hours ago
1 day 10 hours ago
1 day 14 hours ago
1 day 21 hours ago
1 day 22 hours ago