Skip to main content

Embedding a full linear Lambda calculus in Haskell

DOI 10.1145/2804302.2804309 dblp BibTeX

Abstract

We present an encoding of full linear lambda calculus in Haskell using higher order abstract syntax. By making use of promoted data kinds, multi-parameter type classes and functional dependencies, the encoding allows Haskell to do both linear type checking and linear type inference.

Related papers

Embedding session types in Haskell Haskell 2016
Type classes with more higher-order polymorphism ICFP 2002
Solo: a lightweight static analysis for differential privacy OOPSLA 2022
Purity of an ST monad: full abstraction by semantically typed back-translation OOPSLA 2022
Effects as sessions, sessions as effects POPL 2016
Linearly Used Effects: Monadic and CPS Transformations into the Linear Lambda Calculus APLAS 2001
Relational Parametricity for a Polymorphic Linear Lambda Calculus APLAS 2010
Compiling to categories ICFP 2017