Show simple item record

dc.contributor.authorPašalić, Emir
Siek, Jeremy G.
Taha, Walid
dc.date.accessioned 2017-08-02T22:03:05Z
dc.date.available 2017-08-02T22:03:05Z
dc.date.issued 2006-07-28
dc.identifier.urihttps://hdl.handle.net/1911/96359
dc.description.abstract This paper addresses the question of how to extend OCaml’s Hindley-Milner type system with types indexed by logical propositions and proofs of the Coq theorem prover, thereby providing an expressive and extensible mechanism for ensuring fine-grained program invariants. We propose adopting the approached used by Shao et al. for certified binaries. This approach maintains a phase distinction between the computational and logical languages, thereby limiting effects and non-termination to the computational language, and maintaining the decidability of the type system. The extension subsumes language features such as impredicative first-class (higher-rank) polymorphism and type operators, that are notoriously difficult to integrate with the Hindley-Milner style of type inference that is used in OCaml. We make the observation that these features can be more easily integrated with type inference if the inference algorithm is free to adapt the order in which it solves typing constraints to each program. To this end we define a novel “order-free” type inference algorithm. The key enabling technology is a graph representation of constraints and a constraint solver that performs Hindley-Milner inference with just three graph rewrite rules.
dc.format.extent 25 pp
dc.language.iso eng
dc.rights You are granted permission for the noncommercial reproduction, distribution, display, and performance of this technical report in any format, but this permission is only for a period of forty-five (45) days from the most recent time that you verified that this technical report is still available from the Computer Science Department of Rice University under terms that include this permission. All other rights are reserved by the author(s).
dc.title Mixing Indexed Types and Hindley-Milner Type Inference
dc.type Technical report
dc.date.note July 28, 2006
dc.identifier.digital TR07-09
dc.type.dcmi Text
dc.identifier.citation Pašalić, Emir, Siek, Jeremy G. and Taha, Walid. "Mixing Indexed Types and Hindley-Milner Type Inference." (2006) https://hdl.handle.net/1911/96359.


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record