Manifest Contracts for Datatypes

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 for all (λy.y > 0) l} in the former, whereas by a user-defined datatype pos list with cons of type {x int x > 0} × 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 λH dt to formalize the semantics of the casts ...

• Type: Journal
• Year: 2015
• Where: POPL
• Authors: Taro Sekiyama, Yuki Nishida, Atsushi Igarashi
• Keywords: POPL 2015, Programming Languages