Type classes for lightweight substructural types

Edward Gan, Jesse A. Tov, Greg Morrisett

Research output: Contribution to journalConference article

3 Scopus citations

Abstract

Linear and substructural types are powerful tools, but adding them to standard functional programming languages often means introducing extra annotations and typing machinery. We propose a lightweight substructural type system design that recasts the structural rules of weakening and contraction as type classes; we demonstrate this design in a prototype language, Clamp. Clamp supports polymorphic substructural types as well as an expressive system of mutable references. At the same time, it adds little additional overhead to a standard Damas–Hindley–Milner type system enriched with type classes. We have established type safety for the core model and implemented a type checker with type inference in Haskell.

Original languageEnglish (US)
Pages (from-to)34-48
Number of pages15
JournalElectronic Proceedings in Theoretical Computer Science, EPTCS
Volume176
DOIs
StatePublished - Feb 16 2015
Event3rd International Workshop on Linearity, LINEARITY 2014 - Vienna, Austria
Duration: Jul 13 2014 → …

ASJC Scopus subject areas

  • Software

Fingerprint Dive into the research topics of 'Type classes for lightweight substructural types'. Together they form a unique fingerprint.

  • Cite this