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

Browse archivesActive forum topics 
Recent comments
2 hours 5 min ago
2 hours 54 min ago
5 hours 2 min ago
20 hours 7 min ago
1 day 22 min ago
4 days 7 hours ago
1 week 1 day ago
1 week 1 day ago
1 week 2 days ago
1 week 4 days ago