Untangling Typechecking of Intersections and Unions

Details Untangling Typechecking of Intersections and Unions Untangling Typechecking of Intersections and Unions

2011-01-24

arxiv.org/abs/1101.4428v1

EPTCS 45, 2011, pp. 59-70

Computer Science

Programming Languages

In Proceedings ITRS 2010, arXiv:1101.4104

Scientific paper

10.4204/EPTCS.45.5

Intersection and union types denote conjunctions and disjunctions of properties. Using bidirectional typechecking, intersection types are relatively straightforward, but union types present challenges. For union types, we can case-analyze a subterm of union type when it appears in evaluation position (replacing the subterm with a variable, and checking that term twice under appropriate assumptions). This technique preserves soundness in a call-by-value semantics. Sadly, there are so many choices of subterms that a direct implementation is not practical. But carefully transforming programs into let-normal form drastically reduces the number of choices. The key results are soundness and completeness: a typing derivation (in the system with too many subterm choices) exists for a program if and only if a derivation exists for the let-normalized program.

Affiliated with

Also associated with

No associations

Rating

Untangling Typechecking of Intersections and Unions 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 Untangling Typechecking of Intersections and Unions, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Untangling Typechecking of Intersections and Unions will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-635564