Research papers/Type systems

From HaskellWiki

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