Research papers/Type systems

Haskell semantics

A static semantics for Haskell

SL Peyton Jones and PL Wadler, (draft), Department of Computing Science, University of Glasgow, 1992. (Cited by 20)

A Dynamic Semantics for Haskell

Kevin Hammond and Cordelia Hall, (draft), University of Glasgow, 1992, 23 pages.

Typing Haskell in Haskell

Mark P. Jones, In Proceedings of the 1999 Haskell Workshop, Paris, France, October 1999. Published in Technical Report UU-CS-1999-28, Department of Computer Science, University of Utrecht. (Cited by 66)

A static semantics for Haskell

Karl-Filip Faxén, KTH/IMIT/LECS, Kista, Sweden, 2002.

A Lexer for Haskell in Haskell

Thomas Hallgren, PacSoft Oregon Graduate Institute, 14 January, 2002

A Natural Semantics for Lazy Evaluation

John Launchbury, Conference Record of the Twentieth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Charleston, South Carolina, 144--154, 1993.

A Space Semantics for Core Haskell

Adam Bakewell. Proc. 2000 Haskell Workshop. September 2001.

A Systematic Derivation of the STG Machine Verified in Coq

Maciej Pirog and Dariusz Biernacki. Haskell Workshop, 2010.

Pure type systems

Henk: a typed intermediate language

SL Peyton Jones and E Meijer, Proceedings of the Types in Compilation Workshop, Amsterdam, June 1997.

Pure Type Systems for Functional Programming

Jan-Willem Roorda, Masters Thesis, University of Utrecht, INF/SCR-00-13, available online, 2000

Dependent Types

Why Dependent Types Matter

Thorsten Altenkirch and Conor McBride and James McKinna, Manuscript, available online, April, 2005. (Cited by 7)

Simply Easy! An Implementation of a Dependently Typed Lambda Calculus

Andres Löh, Conor McBride and Wouter Swierstra, 2007.

Unboxed values

Parametricity and Unboxing with Unpointed Types

John Launchbury and Ross Paterson, European Symposium on Programming, LNCS, vol. 1058, pp. 204-218, Springer, Linkping, Sweden, 1996.

Unboxed values as first class citizens

SL Peyton Jones and J Launchbury, Functional Programming Languages and Computer Architecture (FPCA'91), Boston, LNCS 523, Springer Verlag, Sept 1991, pp636-666. (Cited by 105)

Modules

A Formal Specification of the Haskell 98 Module System

Iavor S. Diatchki, Mark P. Jones, and Thomas Hallgren. Proceedings of the 2002 ACM SIGPLAN workshop on Haskell. Pittsburgh, Pennsylvania. 17 - 28 2002 ISBN 1-58113-605-6 (Cited by 12)

First class modules for Haskell

Mark Shields and Simon Peyton Jones; FOOL'02.

An exploration of modular programs

Electronic proceedings of the 1996 Glasgow Functional Programming Workshop, J Nicklisch and SL Peyton Jones, Ullapool, July 1996.

Modular monadic typechecker

Adaptable Software - Modular Extensible Monadic Entry-pointless Type Checker in Haskell

Ro/Haskell Group, Univ. “V.Alecsandri”, Bacau, Romania, 2011

Exceptions

An Extensible Dynamically-Typed Hierarchy of Exceptions

Simon Marlow. Haskell '06: Proceedings of the 2006 ACM SIGPLAN workshop on Haskell, Portland, Oregon, ACM Press, September 2006

Imprecise Exceptions, Co-Inductively

Andy Moran, Soeren Lassen, and Simon Peyton Jones. HOOTS'99.

A semantics for imprecise exceptions

Simon Peyton Jones, Alastair Reid, Tony Hoare, Simon Marlow, Fergus Henderson. Proc Programming Language Design and Implementation (PLDI'99), Atlanta.

Asynchronous exceptions in Haskell

Simon Marlow, Simon Peyton Jones, Andy Moran and John Reppy, PLDI'01.

Handling Exceptions in Haskell

A. Reid, Research Report YALEU/DCS/RR-1175, Yale University, August, 1998

Lexically scoped type variables

Lexically scoped type variables

Simon Peyton Jones and Mark Shields. 2004.

Records

Lightweight Extensible Records for Haskell

Mark Jones and Simon Peyton Jones, Haskell Workshop 1999.

Extensible records with scoped labels

Daan Leijen. The 2005 Symposium on Trends in Functional Programming (TFP'05), Tallin, Estonia, September 2005.

First-class labels for extensible rows

Daan Leijen. Technical Report UU-CS-2004-51, Departement of Computer Science, Universiteit Utrecht, 2004.

Haskell Records

J. Peterson, A. Reid, Proceedings of the Haskell Workshop, La Jolla, June 1995.

A Polymorphic Type System for Extensible Records and Variants

Benedict R. Gaster and Mark P. Jones. Department of Computer Science, University of Nottingham. Technical report NOTTCS-TR-96-3. November 1996.

Meta programming

Dynamic typing as staged type inference

MB Shields, T Sheard, and SL Peyton Jones, POPL98.

Template meta-programming for Haskell

Tim Sheard and Simon Peyton Jones, Proceedings of the Haskell Workshop, Pittsburgh, 2002

Optimising Embedded DSLs using Template Haskell

Sean Seefried, Manuel M. T. Chakravarty, and Gabriele Keller. In Gabor Karsai and Eelco Visser, editors, Third International Conference on Generative Programming and Component Engineering (GPCE'04), LNCS 3286, Springer-Verlag, pages 186-205, 2004. [An earlier draft was presented at the IFL 2003 - 15th International Workshop on the Implementation of Functional Languages, 2003.

Unrolling and Simplifying Expressions with Template Haskell

Ian Lynagh, May 2003.

Automatic skeletons in Template Haskell

Kevin Hammond, Jost Berthold and Rita Loogen, June 2003. Proceedings of 2003 Workshop on High Level Parallel Programming, Paris, France

Typing Template Haskell: Soft Types

Ian Lynagh, August 2004.

Dynamic typing

Typing dynamic typing

A. I. Baars and S. D. Swierstra. In S. Peyton Jones, editor, Proceedings of the seventh ACM SIGPLAN international conference on Functional programming, pages 157--166. ACM Press, 2002

Parametricity

Theorems for free!

Philip Wadler. 4'th International Conference on Functional Programming and Computer Architecture, London, September 1989.

Parametricity and Unboxing with Unpointed Types

John Launchbury and Ross Paterson, European Symposium on Programming, LNCS, vol. 1058, pp. 204-218, Springer, Linkping, Sweden, 1996.

GADTs, Functoriality, Parametricity: Pick Two

Patricia Johann, Enrico Ghiorzi, and Daniel Jeffries, 16th Logical and Semantic Frameworks with Applications (LSFA 2021) EPTCS 357, 2022, pp. 77–92.

The Impact of seq on Free Theorems-Based Program Transformations

Patricia Johann and Janis Voigtländer, Fundamenta Informaticae, vol. 69(1-2), pp. 63-102, 2006.

Selective strictness and parametricity in structural operational semantics, inequationally

Janis Voigtländer and Patricia Johann, Theoretical Computer Science, vol. 388(1-3), pp. 290-318, 2007.

Proving Correctness via Free Theorems: The Case of the destroy/build-Rule

Janis Voigtländer. Workshop on Partial Evaluation and Program Manipulation (PEPM'08), Proceedings, ACM Press, 2008.

A family of syntactic logical relations for the semantics of Haskell-like languages

Patricia Johann and Janis Voigtländer, Information and Computation, vol. 207(2), pp. 341-368, 2009.

Parametricity for Haskell with Imprecise Error Semantics

Florian Stenger and Janis Voigtländer. International Conference on Typed Lambda Calculi and Applications (TLCA'09), Proceedings, Springer-Verlag, 2009.

Free Theorems Involving Type Constructor Classes

Janis Voigtländer. International Conference on Functional Programming (ICFP'09), Proceedings, ACM Press, 2009.

Free Theorems for Functional Logic Programs

Jan Christiansen, Daniel Seidel, and Janis Voigtländer. Programming Languages meets Program Verification (PLPV'10), Proceedings, ACM Press, 2010.

Automatically Generating Counterexamples to Naive Free Theorems

Daniel Seidel and Janis Voigtländer. Functional and Logic Programming (FLOPS'10), Proceedings, Springer-Verlag, 2010.

Refined Typing to Localize the Impact of Forced Strictness on Free Theorems

Daniel Seidel and Janis Voigtländer, Acta Informatica, vol. 48(3), pp. 191-211, 2011.

Type classes

How to make ad-hoc polymorphism less ad hoc

Philip Wadler and Stephen Blott. 16'th Symposium on Principles of Programming Languages, ACM Press, Austin, Texas, January 1989.

Type classes in Haskell, CV Hall, K Hammond, SL Peyton Jones, and PL Wadler

European Symposium On Programming, LNCS 788, Springer Verlag, pp. 241-256, April 1994. (Cited by 131)

Implementing Type Classes

John Peterson and Mark P. Jones, In Proceedings of ACM SIGPLAN Symposium on Programming Language Design and Implementation, ACM SIGPLAN, June 1993. (Cited by 40)

Implementing Haskell overloading

Lennart Augustsson, 1993. FPCA. 65-73

Functional Programming with Overloading and Higher-Order Polymorphism

Mark P. Jones, First International Spring School on Advanced Functional Programming Techniques, Baastad, Sweden, Springer-Verlag Lecture Notes in Computer Science 925, May 1995.

Type classes: an exploration of the design space

Simon Peyton Jones, Mark Jones, Erik Meijer, Haskell Workshop 1997.

A system of constructor classes: overloading and implicit higher-order polymorphism

Mark P. Jones, In FPCA '93: Conference on Functional Programming Languages and Computer Architecture, Copenhagen, Denmark, June 1993.

A second look at overloading

Martin Odersky, Philip Wadler, Martin Wehr. 7'th International Conference on Functional Programming and Computer Architecture, ACM Press, San Diego, California, June 1995.

Combining Type Classes and Existential Types

Konstantin Laufer, Proceedings of the Latin American Informatic Conference (PANEL), 1994

Type Classes with Existential Types

Konstantin Laufer, Journal of Functional Programming, 1996, May

Modular Type Classes

Derek Dreyer, Robert Harper, Manuel M.T. Chakravarty and Gabriele Keller, 2006

Named instances for Haskell type classes

W Kahl, J Scheffczyk - Proc. Haskell Workshop, 2001 (Cited by 12)

Deriving type classes

Derivable Type classes

Ralf Hinze and Simon Peyton Jones, Haskell Workshop 2000.

RepLib: A Library for Derivable Type Classes

Stephanie Weirich 2006

Applications of type classes

Number-parameterized types

Oleg Kiselyov, The Monad.Reader. IssueFive. Oct 2nd, 2005

TypeCase: a design pattern for type-indexed functions

Bruno C. d. S. Oliveira, Jeremy Gibbons. Proceedings of the 2005 ACM SIGPLAN workshop on Haskell. Tallinn, Estonia. 98 - 109, 2005 ISBN:1-59593-071-X

Functional pearl: implicit configurations--or, type classes reflect the values of types

Oleg Kiselyov, Chung-chieh Shan, Proceedings of the 2004 ACM SIGPLAN workshop on Haskell, Snowbird, Utah, USA, 2004 ISBN 1-58113-850-4

Extracting Programs from Type Class Proofs

Martin Sulzmann, 2006

Co-induction and Type Improvement in Type Class Proofs

Martin Sulzmann, Jeremy Wazny and Peter J. Stuckey. 2005

Faking It (Simulating Dependent Types in Haskell)

Conor McBride, Journal of Functional Programming, 12(4&5):375-392, July 2002

Aspect-Oriented Programming with Type Classes

Martin Sulzmann and Meng Wang, 2006.

Asymptotic Improvement of Computations over Free Monads

Janis Voigtländer. Mathematics of Program Construction (MPC'08), Proceedings, LNCS 5133:388-403, Springer-Verlag, 2008.

Proving Properties About Functions on Lists Involving Element Tests

Daniel Seidel and Janis Voigtländer. Workshop on Algebraic Development Techniques (WADT'10), Revised Selected Papers, LNCS 7137:270-286, Springer-Verlag, 2012.

Undecidable instances

Undecidable instances

GHC User's Guide.

Multi-parameter type classes

Principal Type Inference for GHC-Style Multi-Parameter Type Classes

Martin Sulzmann, Tom Schrijvers and Peter J. Stuckey. In APLAS'06.

Type Inference for Multi-Parameter Type Classes

Martin Sulzmann and Peter J. Stuckey. 2005

Type-checking multi-parameter type classes

Dominic Duggan and John Ophel, Journal of Functional Programming, 12(2):133-158, March 2002

Functional dependencies

Type Classes with Functional Dependencies

Mark P. Jones, In Proceedings of the 9th European Symposium on Programming, ESOP 2000, Berlin, Germany, March 2000, Springer-Verlag LNCS 1782.

Sound and Decidable Type Inference for Functional Dependencies

Gregory J. Duck, Simon Peyton Jones, Peter J. Stuckey, and Martin Sulzmann, European Symposium on Programming 2004 (ESOP'04).

Understanding Functional Dependencies via Constraint Handling Rules

Martin Sulzmann, Gregory J. Duck, Simon Peyton-Jones and Peter J. Stuckey.j To appear in Journal of Functional Programming. 2006

Associated Functional Dependencies

Martin Sulzmann and Edmund Soon Lee Lam. 2005

Constraint Handling Rules

Type Processing by Constraint Reasoning

Peter J. Stuckey, Martin Sulzmann and Jeremy Wazny, In APLAS'06.

A Concurrent Constraint Handling Rules Implementation in Haskell with Software Transactional Memory

Edmund S.L. Lam and Martin Sulzmann

Observable Confluence for Constraint Handling Rules

Gregory J. Duck, Peter J. Stuckey and Martin Sulzmann

Generalised Algebraic Data Types (GADTs)

Simple unification-based type inference for GADTs

Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Geoffrey Washburn. Submitted to PLDI 2005

Wobbly types: type inference for generalised algebraic data types

S Peyton Jones, G. Washburn, and S. Weirich. 2004.

Translating Generalized Algebraic Data Types to System F

Martin Sulzmann and Meng Wang. 2005

Stratified type inference for generalized algebraic data types

François Pottier and Yann Régis-Gianas, 2006

Type Inference for GADTs via Herbrand Constraint Abduction

Martin Sulzmann, Tom Schrijvers and Peter J. Stuckey, 2006

A Framework for Extended Algebraic Data Types

Martin Sulzmann, Jeremy Wazny and Peter J. Stuckey, 2006

Complete and Decidable Type Inference for GADTs

Tom Schrijvers, Simon Peyton-Jones, Martin Sulzmann and Dimitrios Vytiniotis, 2009.

Pointwise Generalized Algebraic Data Types

Chuan-kai Lin and Tim Sheard, 2010.

See also the GADT page.

Parametric Regular Data Types

Type Inference and Compilation for Parametric Regular Data Types

Martin Sulzmann and Kenny Zhuo Ming Lu, 2006

The Marriage of Haskell and XDuce

Martin Sulzmann and Kenny Zhuo Ming Lu

Type Families and Associated types

Associated types with class

Manuel M. T. Chakravarty, Gabriele Keller, Simon Peyton Jones, Simon Marlow) POPL '05: Proceedings of the 32nd ACM SIGPLAN-SIGACT sysposium on Principles of programming languages, pages 1--13, Long Beach, California, USA, ACM Press, 2005

Associated Type Synonyms

Manuel M. T. Chakravarty, Gabriele Keller, and Simon Peyton Jones. In Proceedings of The Tenth ACM SIGPLAN International Conference on Functional Programming, ACM Press, pages 241-253, 2005.

ML Modules and Haskell Type Classes: A Constructive Comparison

Stefan Wehr Diplomarbeit. Albert-Ludwigs-Universitt Freiburg, Fakultt fr Angewandte Wissenschaften, Institut fr Informatik, November 2005.

System F with Type Equality Coercions

Martin Sulzmann, Manuel M. T. Chakravarty, and Simon Peyton Jones.

Towards Open Type Functions for Haskell

Tom Schrijvers, Simon Peyton Jones, Martin Sulzmann, and Manuel Chakravarty. In Proceedings of IFL' 07, Freiburg, Germany, 2007.

Type Checking with Open Type Functions for Haskell

Tom Schrijvers, Simon Peyton Jones, Manuel Chakravarty, and Martin Sulzmann. In Proceedings of ICFP' 08, Victoria, Canada, 2008.

Arbitrary-rank polymorphism

Putting type annotations to work

Martin Odersky and Konstantin Läufer. Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages. St. Petersburg Beach, Florida, United States. 54 - 67 1996 ISBN 0-89791-769-3

Practical type inference for arbitrary-rank types

SP Jones, M Shields - Submitted to the Journal of Functional Programming, 2005

Phantom types

First-class phantom types

James Cheney and Ralf Hinze. Technical Report TR2003-1901, Cornell University, 2003.

Phantom Types and Subtyping

Matthew Fluet and Riccardo Pucella. Submitted to the Journal of Functional Programming, 2006.

Implicit parameters

Implicit Parameters: Dynamic Scoping with Static Types

Jeffrey Lewis, Mark Shields, Erik Meijer and John Launchbury. POPL'00. 2000.

Global variables in Haskell

John Hughes. J. Funct. Program. 14(5): 489-502 (2004)

Explicit Implicit Parameters

A. Dijkstra and S. D. Swierstra. UU-CS 2004-059, 2004.

Object oriented Haskell

Object-Oriented Style Overloading for Haskell

Mark Shields and Simon Peyton Jones; BABEL workshop '01.

Interfacing Haskell with Object-Oriented Languages

Andr T. H. Pang and Manuel M. T. Chakravarty. In Greg Michaelson and Phil Trinder, editors, Implementation of Functional Languages: 15th International Workshop, IFL 2003, Edinburgh, UK, September 8-11, 2003, Revised Papers, LNCS 3145, Springer-Verlag, pages 20-36, 2004.

Haskell++: An Object-Oriented Extension of Haskell

Jan Sparud and John Hughes. Haskell Workshop 1995

Haskell's overlooked object system

Oleg Kiselyov and Ralf Lämmel, submitted for journal publication; online since 30 Sep. 2004;

Restricted Datatypes

Restricted datatypes

John Hughes. 1999 Haskell workshop

Patterns

First Class Patterns

Mark Tullsen. Practical Aspects of Declarative Languages, Second International Workshop, PADL 2000. volume 1753 of Lecture Notes in Computer Science. January 2000.

Pattern guards

Pattern Guards and Transformational Patterns

Martin Erwig and Simon Peyton Jones; Haskell Workshop 2000.

A new view of guards

Simon Peyton Jones, April 1997

Views

Views: An Extension to Haskell Pattern Matching

Warren Burton, Erik Meijer, Patrick Sansom, Simon Thompson and Phil Wadler.

Views: A way for pattern matching to cohabit with data abstraction

POPL 14 (1987), 307-313.

Qualified types

Qualified Types: Theory and Practice

Mark P. Jones. PhD. Thesis. Yale University. November 1994.

Simplifying and Improving Qualified Types

Mark P. Jones. FPCA '95: Conference on Functional Programming Languages and Computer Architecture. June 1995.

Simplifying and Improving Qualified Types

Mark P. Jones. Yale University. Research Report YALEU/DCS/RR-1040. June 1994.

Coherence for qualified types

Mark P. Jones. Yale University. Research Report YALEU/DCS/RR-989. September 1993.

A theory of qualified types

Mark P. Jones. ESOP '92: European Symposium on Programming. Lecture Notes in Computer Science, 582. February 1992. (Cited by 68)

Polymorphic recursion

Type inference with polymorphic recursion

F Henglein - ACM Transactions on Programming Languages and Systems (1993)

Practical Type Inference for Polymorphic Recursion: an Implementation in Haskell

C Vasconcellos, L Figueiredo, C Camarao - Journal of Universal Computer Science, 2003

Type Inference for Polymorphic Recursive Definitions: a Specification in Haskell

L Figueiredo, C Camarao