Manifest Contracts for Datatypes

作者：Sekiyama Taro^*; Nishida Yuki; Igarashi Atsushi

来源：ACM Sigplan Notices, 2015, 50(1): 195-207.

DOI：10.1145/2676726.2676996

• Languages
• Design
• Theory
• algebraic datatypes
• datatype translation
• contract checking
• refinement types

We study algebraic datatypes in a manifest contract system, a software contract system where contract information occurs as refinement types. We first compare two simple approaches: refinements on type constructors and refinements on data constructors. For example, lists of positive integers can be described by {l:int list vertical bar for all (lambda(y.y) > 0) l} in the former, whereas by a user-defined datatype pos_list with cons of type {x:int vertical bar x > 0} x pos_list -> pos_list in the latter. The two approaches are complementary: the former makes it easier for a programmer to write types and the latter enables more efficient contract checking. To take the best of both worlds, we propose (1) a syntactic translation from refinements on type constructors to equivalent refinements on data constructors and (2) dynamically checked casts between different but compatible datatypes such as int list and pos_list. We define a manifest contract calculus lambda(H)(dt) to formalize the semantics of the casts and prove that the translation is correct.

• 出版日期2015-1