Expansion for Universal Quantifiers

Details Expansion for Universal Quantifiers Expansion for Universal Quantifiers

2012-01-05

arxiv.org/abs/1201.1101v1

Computer Science

Programming Languages

Long version of the corresponding ESOP 2012 paper

Scientific paper

Expansion is an operation on typings (i.e., pairs of typing environments and result types) defined originally in type systems for the lambda-calculus with intersection types in order to obtain principal (i.e., most informative, strongest) typings. In a type inference scenario, expansion allows postponing choices for whether and how to use non-syntax-driven typing rules (e.g., intersection introduction) until enough information has been gathered to make the right decision. Furthermore, these choices can be equivalent to inserting uses of such typing rules at deeply nested positions in a typing derivation, without needing to actually inspect or modify (or even have) the typing derivation. Expansion has in recent years become simpler due to the use of expansion variables (e.g., in System E). This paper extends expansion and expansion variables to systems with forall-quantifiers. We present System Fs, an extension of System F with expansion, and prove its main properties. This system turns type inference into a constraint solving problem; this could be helpful to design a modular type inference algorithm for System F types in the future.

Affiliated with

Also associated with

No associations

Rating

Expansion for Universal Quantifiers does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Expansion for Universal Quantifiers, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Expansion for Universal Quantifiers will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-609499