Typing Unmarshalling without Marshalling Types
| Autor: | Michel Mauny, Grégoire Henry, Pascal Manoury, Emmanuel Chailloux |
|---|---|
| Přispěvatelé: | Algorithmes, Programmes et Résolution (APR), Laboratoire d'Informatique de Paris 6 (LIP6), Université Pierre et Marie Curie - Paris 6 (UPMC)-Centre National de la Recherche Scientifique (CNRS)-Université Pierre et Marie Curie - Paris 6 (UPMC)-Centre National de la Recherche Scientifique (CNRS) |
| Jazyk: | angličtina |
| Rok vydání: | 2012 |
| Předmět: |
Parametric polymorphism
Theoretical computer science Computer science Type system 0102 computer and information sciences 02 engineering and technology computer.software_genre Data type 01 natural sciences Marshalling Type safety 0202 electrical engineering electronic engineering information engineering Type class [INFO]Computer Science [cs] Recursive data type Variant type Programming language Type inference 020207 software engineering Computer Graphics and Computer-Aided Design 010201 computation theory & mathematics Algebraic data type Compiler Generalized algebraic data type computer Software |
| Zdroj: | International Conference on Functional Programming International Conference on Functional Programming, Sep 2012, Copenhagen, Denmark. pp.287-298, ⟨10.1145/2364527.2364569⟩ ICFP |
| DOI: | 10.1145/2364527.2364569⟩ |
| Popis: | International audience; Unmarshalling primitives in statically typed language require, in order to preserve type safety, to dynamically verify the compatibility between the incoming values and the statically expected type. In the context of programming languages based on parametric polymorphism and uniform data representation, we propose a relation of compatibility between (unmarshalled) memory graphs and types. It is defined as constraints over nodes of the memory graph. Then, we propose an algorithm to check the compatibility between a memory graph and a type. It is described as a constraint solver based on a rewriting system. We have shown that the proposed algorithm is sound and semi-complete in presence of algebraic data types, mutable data, polymorphic sharing, cycles, and functional values, however, in its general form, it may not terminate. We have implemented a prototype tailored for the OCaml compiler [17] that always terminates and still seems sufficiently complete in practice. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|