We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

cs.PL

Change to browse by:

cs

References & Citations

DBLP - CS Bibliography

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Programming Languages

Title: Kind Inference for Datatypes: Technical Supplement

Abstract: In recent years, languages like Haskell have seen a dramatic surge of new features that significantly extends the expressive power of their type systems. With these features, the challenge of kind inference for datatype declarations has presented itself and become a worthy research problem on its own.
This paper studies kind inference for datatypes. Inspired by previous research on type-inference, we offer declarative specifications for what datatype declarations should be accepted, both for Haskell98 and for a more advanced system we call PolyKinds, based on the extensions in modern Haskell, including a limited form of dependent types. We believe these formulations to be novel and without precedent, even for Haskell98. These specifications are complemented with implementable algorithmic versions. We study soundness, completeness and the existence of principal kinds in these systems, proving the properties where they hold. This work can serve as a guide both to language designers who wish to formalize their datatype declarations and also to implementors keen to have principled inference of principal types.
This technical supplement to Kind Inference for Datatypes serves to expand upon the text in the main paper. It contains detailed typing rules, proofs, and connections to the Glasgow Haskell Compiler (GHC).
Comments: Technical supplement for POPL2020 paper Kind Inference for Datatypes
Subjects: Programming Languages (cs.PL)
DOI: 10.1145/3371121
Cite as: arXiv:1911.06153 [cs.PL]
  (or arXiv:1911.06153v1 [cs.PL] for this version)

Submission history

From: Ningning Xie [view email]
[v1] Tue, 12 Nov 2019 02:26:22 GMT (122kb)

Link back to: arXiv, form interface, contact.