VSL 2014: VIENNA SUMMER OF LOGIC 2014

Type Classes for Lightweight Substructural Types

Authors: Edward Gan, Jesse A. Tov and Greg Morrisett

PapersPapers with AbstractsPrefaceAuthor IndexKeyword Index

Paper Information

Title:Type Classes for Lightweight Substructural Types
Authors:Edward Gan, Jesse A. Tov and Greg Morrisett
Proceedings:Linearity 2014 Informal Proceedings
Editors: Sandra Alves and Iliano Cervesato
Keywords:Substructural Types, Type Classes, Linear Types, Haskell, Strong Update
Abstract:

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 for Clamp in Haskell.

Pages:8
Talk:Jul 13 15:30
Paper:
Disclaimer | Powered by EasyChair Smart Program