One lesson learned painfully over the past twenty years is the perilous interaction of Curry-style refinement typing with evaluation order and side-effects. This led eventually to the value restriction on polymorphism in ML, as well as, more recently, to similar artifacts in prototype refinement type systems for ML with intersection and union types. For example, some of the traditional subtyping laws for unions and intersections are unsound in the presence of effects, while union-elimination requires an evaluation context restriction in addition to the value restriction on intersection-introduction.
This paper reexamines the interaction between refinement types and evaluation order from the perspective of computational duality. Building on recent work on the Curry-Howard interpretation of focusing proofs as pattern-matching programs written in infinitary, higher-order syntax, I give a simple explanation of intersection and union types in the presence of effects, reconstructing phenomena such as the value restriction and differing subtyping laws for call-by-value and call-by-name-- not as ad hoc artifacts, but indeed as logical theorems. However, this abstract account using infinitary syntax has the drawback that refinement checking is undecidable---to address this, I show how to systematically construct a finitary syntax via defunctionalization, and then give an algorithmic refinement checking system. Parallel to the text, a formalization in the dependently-typed functional language Agda is described, both for the sake of clarifying these ideas, and also because it was an important guide in developing them. As one example, the Agda encoding split very naturally into an intrinsic ("Church") view of well-typed programs, and an extrinsic ("Curry") view of refinement typing for those programs.
Code available here.
No comments:
Post a Comment