Tom Schrijvers, Simon Peyton Jones, Martin Sulzmann, Dimitrios Vytiniotis
GADTs have proven to be an invaluable language extension, a.o. for ensuring data invariants and program correctness. Unfortunately, they pose a tough problem for type inference: we lose the...
Type checking with open type functions (2009)
Tom Schrijvers, Simon Peyton Jones, Manuel Chakravarty, Martin Sulzmann
We report on an extension of Haskell with open type-level functions and equality constraints that unifies earlier work on GADTs, functional dependencies, and associated types. The contribution of the...
Type Checking with Open Type Functions (2009)
Tom Schrijvers, Simon Peyton Jones, Manuel Chakravarty, Martin Sulzmann
We report on an extension of Haskell with open type-level functions and equality constraints that unifies earlier work on GADTs, functional dependencies, and associated types. The contribution of the...
Restoring confluence of functional dependencies via type families (2009)
Tom Schrijvers, Martin Sulzmann
Haskell-style functional dependencies [2] provide a relational specification of user-programmable type improvement [1] connected to type class instances. The more recent type families (also known as...
Unified Type Checking for Type Classes and Type Families (2009)
Tom Schrijvers, Martin Sulzmann
Haskell, type checking, type classes, type families Haskell has a rich type system with various complementary, interacting and overlapping features. In particular we think of the established type...
Chapter 2 Restoring Confluence for Functional Dependencies (2009)
Tom Schrijvers, Martin Sulzmann
Abstract: Haskell-style functional dependencies allow the programmer to influence the type inference process by automatically deriving type improvement rules from class and instance declarations....
Chapter 2 Confluence for Non-Full Functional Dependencies (2009)
Tom Schrijvers, Martin Sulzmann
Abstract: Previous work on type inference for functional dependencies demands that the dependency must fully cover all parameters of a type class to guarantee that the constraint solver is confluent....
Transactions in Constraint Handling Rules (2009)
Tom Schrijvers, Martin Sulzmann
Abstract. CHR is a highly concurrent language, and yet it is by no means a trivial task to write correct concurrent CHR programs. We propose a new semantics for CHR, which allows specifying and...
Type Structure General Terms Algorithms, Languages (2009)
Simon Peyton Jones, Martin Sulzmann
Type Checking with Open Type Functions We report on an extension of Haskell with open type-level functions and equality constraints that unifies earlier work on GADTs, functional dependencies, and...
ML 2005 Preliminary Version A Type-Safe Embedding of XDuce into ML (2009)
Martin Sulzmann, Kenny Zhuo, Ming Lu
Key words: Semi-structured data handling, programtransformation, language integration/extension. 1 Introduction There has been some notable interest in making use of typed programming languages for...
Complete and decidable type inference for GADTs (2009)
Peyton Jones, Simon, Sulzmann, Martin, Vytiniotis, Dimitrios
GADTs have proven to be an invaluable language extension, for ensuring data invariants and program correctness among others. Unfortunately, they pose a tough problem for type inference: we lose the...
Type Inference for Multi-Parameter Type Classes (2008)
Martin Sulzmann, Peter J. Stuckey
We observe that the combination of multi-parameter type classes with existential types and type annotations leads to a loss of principal types. As a consequence type inference in implementations such...
Parallel Execution of Multi Set Constraint Rewrite Rules (2008)
Abstract. Multi-set constraint rewriting allows for a highly parallel computational model and has been used in a multitude of application domains such as constraint solving, agent specification etc....
General Terms Languages, theory (2008)
We consider the problem of adding aspects to a strongly typed language which supports type classes. We show that type classes as supported by the Glasgow Haskell Compiler can model an AOP style of...
Actors with Multi-Headed Message Receive Patterns (2008)
Martin Sulzmann, Peter Van, Weert Programming, Semantics Group, Rued Langgaards Vej, ...
A Type-Safe Embedding of Constraint Handling (2008)
Rules Into Haskell, Wei-ngan Chin, Martin Sulzmann, Meng Wang
Actors with Multi-Headed Message Receive Patterns (2008)
Martin Sulzmann, Peter Van Weert
Abstract. The actor model provides the programmer with high-level concurrency abstractions to coordinate simultaneous computations by sending and receiving messages. Languages implementing the actor...
Exception Analysis, Non-strict Languages, Kevin Glynn, Peter J. Stuckey, Martin Sulzmann, Computer Science, ...
Abstract In this paper we present the first exception analysis for a non-strictlanguage. We augment a simply-typed functional language with exceptions, and show that we can define a type-based...
GADTless Programming in Haskell 98 (2008)
Abstract. Generalized algebraic data types (GADTs) allow to write sophisticated, type-safe programs and transformations. But not many languages, respectively their underlying implementations, support...
Martin Sulzmann, Gregory J. Duck, Simon Peyton-jones, Peter J. Stuckey
Functional dependencies are a popular and useful extension to Haskell style type classes. We give a reformulation of functional dependencies in terms of Constraint Handling Rules (CHRs). In previous...
Translating Generalized Algebraic Data Types (2008)
To System F, Martin Sulzmann, Meng Wang
1 Introduction Generalized algebraic data types (GADTs) are an extension of (boxed) existen-tial types [17]. The novelty of GADTs is that we may include syntactic type equality constraints, i.e....
Abstract Aspect-Oriented Programming with Type Classes (2008)
We study aspect-oriented programming (AOP) in the context of the strongly typed language Haskell. We show how to support AOP via a straightforward type class encoding. Our main result is that...
Martin Sulzmann, Tom Schrijvers
What’s this talk about? Principal types guarantee that any other valid type can be derived from the principal type. Type inference is a very important property. (type inference = inference in the...
Martin Sulzmann, Kenny Zhuo, Ming Lu, ...
<!DOCTYPE addrbook [ <!ELEMENT addrbook (person) *> <!ELEMENT person (name, tel?, (email)*)> <!ELEMENT name (#PCDATA)> <!ELEMENT tel (#PCDATA)> <!ELEMENT email...
Abstract A Framework for Extended Algebraic Data Types (2008)
Extended forms of algebraic data types allow for sophisticated type extensions. A number of proposals exists and its often hard to understand what has been achieved. Here, we present a unifying...
Martin Sulzmann, Gregory J. Duck, Simon Peyton-jones, Peter J. Stuckey
Functional dependencies are a popular and useful extension to Haskell style type classes. We give a reformulation of functional dependencies in terms of Constraint Handling Rules (CHRs). In previous...
Martin Sulzmann, Csregular Expressions P
Pattern search: Find words (strings) according to a pattern. grep: Unix commando to search for words matching a pattern defined in files. grep ’M[ae][iy]er ’ names searches for all Meiers,...
Towards Open Type Functions for Haskell — DRAFT — (2008)
Tom Schrijvers, Martin Sulzmann, Simon Peyton-jones
Abstract. We report on an extension of Haskell with type(-level) functions and equality constraints. We illustrate their usefulness in the context of phantom types, GADTs and type classes. Problems...
We introduce System FC, which extends System F with support for non-syntactic type equality. There are two main extensions: (i) explicit witnesses for type equalities, and (ii) open, non-parametric...
CHR Grammars with multiple constraint stores (2008)
Thom Frühwirth, Marc Meister (eds, Sciendo Docendo Curando, Henning Christiansen, Tom Schrijvers, ...
The Constraint Handling Rules (CHR) language has become a major specification and implementation language for constraint-based algorithms and applications. Algorithms are often specified using...
AADEBUG2003 XXX1 The Chameleon Type Debugger (Tool Demonstration) (2008)
Peter J. Stuckey, Martin Sulzmann, Jeremy Wazny
In this tool demonstration, we give an overview of the Chameleon type debugger. The type debugger’s primary use is to identify locations within a source program which are involved in a type error....
Martin Sulzmann, Peter J. Stuckey
The HM(X) system is a generalization of the Hindley/Milner system parameterized in the constraint domain X. Type inference is performed by generating constraints out of the program text which are...
Martin Sulzmann, Gregory J. Duck, Simon Peyton-jones, Peter J. Stuckey, Martin Sulzmann, Gregory J. Duck, ...
Functional dependencies are a popular and useful extension to Haskell style type classes. We give a reformulation of functional dependencies in terms of Constraint Handling Rules (CHRs). In previous...
Towards Open Type Functions for Haskell (2008)
Tom Schrijvers, Martin Sulzmann, Simon Peyton-jones
Abstract. We report on an extension of Haskell with type(-level) functions and equality constraints. We illustrate their usefulness in the context of phantom types, GADTs and type classes. Problems...
Martin Sulzmann, Tom Schrijvers, Peter J. Stuckey, Martin Sulzmann, Tom Schrijvers, Peter J. Stuckey, ...
Type inference for Hindley/Milner and variants is well understood as a constraint solving problem. Recent extensions to Hindley/Milner such as generalized algebraic data types (GADTs) force us to go...
The Tableau-based Theorem Prover (2007)
Version Bernhard Beckert, Bernhard Beckert, Reiner Hahnle, Peter Oel, Martin Sulzmann
This paper gives an overview of the system with a special focus on the new features of 3 T A P Version 4.0, including: efficient completion-based equality reasoning, methods for handling redundant...
In this short note, we provide proofs of soundness and completeness of constraint{ based type inference in HM(X). We rely on previous notations and refer to [Sul00] for details. We nd the following...
Bernhard Beckert, Reiner Hahnle, Peter Oel, Martin Sulzmann
3 T A P is a tableau-based theorem prover for many-valued first-order logics with sorts (in the two-valued version with equality); it is implemented in Prolog. This paper gives an overview of the...
Type inference with constrained types. (2007)
Sulzmann, Martin, Odersky, Martin, Wehr, Martin
In this paper we present a general framework HM(X) for Hindley/Milner style type systems with constraints, analogous to the CLP(X) framework in constrained logic programming. We present sufficient...
Haskell Communities and Activities Report (2007)
Andres Löh (ed, Lloyd Allison, Tiago Miguel, Laureano Alves, Krasimir Angelov, Carlos Areces, ...
You are reading the twelfth edition of the Haskell Communities and Activities Report – as always, containing entries from enthusiastic Haskellers all over the world. This edition has 138 entries,...
System F with type equality coercions (2007)
Martin Sulzmann, Simon Peyton Jones, Kevin Donnelly
We introduce System FC, which extends System F with support for non-syntactic type equality. There are two main extensions: (i) explicit witnesses for type equalities, and (ii) open, non-parametric...
Towards Open Type Functions for Haskell (2007)
Tom Schrijvers, Martin Sulzmann, Simon Peyton Jones
Abstract. We report on an extension of Haskell with type(-level) functions and equality constraints. We illustrate their usefulness in the context of phantom types, GADTs and type classes. Problems...
System f with type equality coercions (2007)
We introduce System �� � , which extends System F with support for non-syntactic type equality. There are two main extensions: (i) explicit witnesses for type equalities, and (ii)...
Haskell Communities and Activities Report (2006)
Andres Löh (ed, Lloyd Allison, Tiago Miguel, Laureano Alves, Krasimir Angelov, Dmitry Astapov, ...
Welcome to the eleventh edition of the Haskell Communities and Activities Report – a collection of entries about everything that is going on and related to Haskell in some way that appears twice a...
Principal type inference for GHCstyle multi-parameter type classes (2006)
Martin Sulzmann, Tom Schrijvers, Peter J. Stuckey
Abstract. We observe that the combination of multi-parameter type classes with existential types and type annotations leads to a loss of principal types and undecidability of type inference. This may...
Type processing by constraint reasoning (2006)
Peter J. Stuckey, Martin Sulzmann, Jeremy Wazny
Abstract. Herbrand constraint solving or unification has long been understood as an efficient mechanism for type checking and inference for programs using Hindley/Milner types. If we step back from...
Observable confluence for constraint handling rules (2006)
Gregory J. Duck, Peter J. Stuckey, Martin Sulzmann
Abstract. Constraint Handling Rules (CHR) are a powerful rule based language for specifying constraint solvers. Critical for any rule based language is the notion of confluence, and for terminating...
Haskell Communities and Activities Report (2006)
Andres Löh (ed, Lloyd Allison, Tiago Miguel, Laureano Alves, Krasimir Angelov, Dmitry Astapov, ...
This is the tenth edition of the Haskell Communities and Activities Report (HCAR) – a collection of entries about everything that is going on and related to Haskell in some way that appears twice a...
Observable confluence for constraint handling rules (2006)
Gregory J. Duck, Peter J. Stuckey, Martin Sulzmann
Abstract. Constraint Handling Rules (CHR) are a powerful rule based language for specifying constraint solvers. Critical for any rule based language is the notion of confluence, and for terminating...
A framework for extended algebraic data types (2006)
Martin Sulzmann, Jeremy Wazny, Peter J. Stuckey
Abstract. There are a number of extended forms of algebraic data types such as type classes with existential types and generalized algebraic data types. Such extensions are highly useful but their...
Type processing by constraint reasoning (2006)
Peter J. Stuckey, Martin Sulzmann, Jeremy Wazny
Abstract. Herbrand constraint solving or unification has long been understood as an efficient mechanism for type checking and inference for programs using Hindley/Milner types. If we step back from...
Principal type inference for GHCstyle multi-parameter type classes (2006)
Martin Sulzmann, Tom Schrijvers, Peter J. Stuckey
Abstract. We observe that the combination of multi-parameter type classes with existential types and type annotations leads to a loss of principal types and undecidability of type inference. This may...
Peter J. Stuckey, Martin Sulzmann, Jeremy Wazny, Hindley Milner, Type Inference, Peter J. Stuckey, ...
Chameleon is Haskell-style language ◮ treats type problems using constraints ◮ gives expressive error messages ◮ has a programmable type system ◮ Developers: Martin Sulzmann, Jeremy Wazny
A framework for extended algebraic data types (2006)
Algebraic data types (and variants): (Boxed) existential types. Type classes with existential types. Generalized algebraic data types (GADTs). Extended algebraic data types (EADTs)
Aspect-oriented programming with type classes. http://www.comp.nus.edu.sg/˜ sulzmann (2006)
What’s this talk about? Aspect-oriented programming (AOP) is an emerging paradigm to aid the user in the modularization of cross-cutting concerns. Type classes are an established concept to support...
Improved Inference for Checking Annotations (2005)
Stuckey, Peter J, Sulzmann, Martin, Wazny, Jeremy
We consider type inference in the Hindley/Milner system extended with type annotations and constraints with a particular focus on Haskell-style type classes. We observe that standard inference...
Type Inference for Guarded Recursive Data Types (2005)
Stuckey, Peter J., Sulzmann, Martin
We consider type inference for guarded recursive data types (GRDTs) -- a recent generalization of algebraic data types. We reduce type inference for GRDTs to unification under a mixed prefix. Thus,...
C++ Templates/Traits versus Haskell Type Classes (2005)
Sunil Kothari, Martin Sulzmann
This article presents an in-depth study of the close connection between Haskell type classes and C++ template/traits mechanism- two different facilties for implementing generic programming concepts....
Haskell Communities and Activities Report (2005)
Andres Löh (ed, Lloyd Allison, Tiago Miguel, Laureano Alves, Krasimir Angelov, Alistair Bayley, ...
Finally, here is the 9th edition of the Haskell Communities and Activities Report (HCAR), almost three weeks after the submission deadline. This delay is entirely my own fault. In fact, I have to...
Dean of School C++ templates/traits versus Haskell type classes (2004)
Sunil Kothari, Martin Sulzmann, Jaffar Joxan, Sunil Kothari, Martin Sulzmann
tutorial article, which has been submitted for publication in a journal or for consideration by the commissioning organization. The report represents the ideas of its author, and should not be taken...
ABSTRACT XHaskell: Regular Expression Types for Haskell (2004)
Kenny Zhuo, Ming Lu, Martin Sulzmann, Jaffar Joxan, Kenny Zhuo, Ming Lu
tutorial article, which has been submitted for publication in a journal or for consideration by the commissioning organization. The report represents the ideas of its author, and should not be taken...
Peter J. Stuckey, Martin Sulzmann, Jeremy Wazny
We give an overview of the major features of the Chameleon programming language, as well as use of the system, from a Haskell programmer's point of view. Chameleon supports typeclass overloading...
The Chameleon Type Debugger (Tool Demonstration) (2003)
Stuckey, Peter J., Sulzmann, Martin, Wazny, Jeremy
In this tool demonstration, we give an overview of the Chameleon type debugger. The type debugger's primary use is to identify locations within a source program which are involved in a type error. By...
Resource usage verification (2003)
Kim Marriott, Peter J. Stuckey, Martin Sulzmann
Abstract. We investigate how to automatically verify that resources such as files are not used improperly or unsafely by a program. We employ a mixture of compile-time analysis and run-time testing...
A theory of overloading part II: semantics and coherence (2002)
Andreas Rossberg, Martin Sulzmann
This paper is a complement to \A Theory of Overloading " by Stuckey and Sulzmann. The authors introduce a general overloading framework based on Constraint Handling Rules (CHRs). The main...
A theory of overloading (2002)
Peter J. Stuckey, Martin Sulzmann, Jeremy Wazny
Abstract We introduce a novel approach for debugging ill-typed programs in the Hindley/Milner system. We map the typing problem for a program to a system of constraints each attached to program code...
Andreas Rossberg, Martin Sulzmann
We discuss type classes in the context of the Chameleon language, a Haskell-style language where overloading resolution is expressed in terms of the meta-language of Constraint Handling Rules (CHRs)....
A Theory of Overloading (2002)
Peter J. Stuckey, Martin Sulzmann
We present a minimal extension of the Hindley/Milner system to allow for overloading of identi ers. Our approach relies on a combination of the HM(X) type system framework with Constraint Handling...
Effective strict-ness analysis with Horn constraints (2001)
Kevin Glynn, Peter J. Stuckey, Martin Sulzmann
Abstract. We introduce a constraint-based framework for strictness analysis applicable to ML style languages supporting higher-order functions, let-style polymorphism and algebraic datatypes. The...
Boolean constraints for binding-time analysis (2001)
Kevin Glynn, Peter J. Stuckey, Martin Sulzmann
Abstract. To achieve acceptable accuracy, many program analyses for functional programs are \property polymorphic". That is, they can infer dierent input-output relations for a function at...
Type Classes and Constraint Handling Rules (2000)
Glynn, Kevin, Sulzmann, Martin, Stuckey, Peter J.
Type classes are an elegant extension to traditional, Hindley-Milner based typing systems. They are used in modern, typed languages such as Haskell to support controlled overloading of symbols....
Type classes and constraint handling rules (2000)
Kevin Glynn, Peter J. Stuckey, Martin Sulzmann
Type classes are an elegant extension to traditional, Hindley-Milner based typing systems. They are used in modern, typed languages such as Haskell to support controlled overloading of symbols....
Type Classes and Constraint Handling Rules (2000)
Kevin Glynn, Peter J. Stuckey, Martin Sulzmann
Type classes give a clean approach to dene overloading in programming languages such as Haskell. Haskell 98 supports only single-parameter and constructor type classes. Other extensions such as...
A General Framework for Hindley/Milner Type Systems with Constraints (2000)
with constraints. The basic idea is to factor out the common core of previous extensions of the Hindley/Milner system. I present a Hindley/Milner system where the constraint part is a parameter....
Type Inference with Constrained Types (1999)
Odersky, Martin, Sulzmann, Martin, Wehr, Martin
In this paper we present a general framework HM(X) for Hindley/Milner style type systems with constraints, analogous to the CLP(X) framework in constrained logic programming. We show that the type...
A general framework for Hindley/Milner type systems with constraints / (1999)
Thesis (Ph. D.)--Yale University, 2000.
Hindley/Milner style type systems in constraint form (1999)
Martin Sulzmann, Martin Müller, Christoph Zenger
This papers describes Hindley/Milner style type systems in constraint form. Previously, many type descriptions have still been partially represented in the type language. We argue that this can lead...
Type Inference with Constrained Types (1999)
Martin Odersky, Martin Sulzmann, Martin Wehr
this paper we present a general framework HM(X) for Hindley/Milner style type systems with constraints, analogous to the CLP(X) framework in constraint logic programming [JM94]. Particular type...
Type Inference with Constrained Types (1999)
Martin Sulzmann, Martin Odersky, Martin Wehr
this paper we present a general framework HM(X) for Hindley/Milner style type systems with constraints, analogous to the CLP(X) framework in constraint logic programming [JM94]. Particular type...
Type Inference with Constrained Types (1999)
Martin Sulzmann, Martin Odersky, Martin Wehr
In this paper we present a general framework HM(X) for Hindley/Milner style type systems with constraints. We give a generic type inference algorithm for HM(X). Under sufficient conditions on X, type...
A constraint-based View of Dependent Types (1998)
In this paper we discuss a constraint--based view of dependent types. We survey several systems that deal with a form of dependent types. We are interested in the use of dependent types for indexed...
Analysis of Architectures using Constraint-Based Types (1998)
John Peterson, Martin Sulzmann
Constraint--based types provide a formal foundation for many varieties of architectural analysis. A software architecture, typically defined using an Architecture Definition Language (ADL), exposes...
Type Systems for Records revisited (1998)
We explore the design space for type systems with polymorphic records. We design record systems for extension, concatenation and removal of fields. Furthermore, we design a record system where field...
Polymorphism in Hindley/Milner Style Type Systems with Constraints (1998)
In this paper we study the impact of polymorphism in Hindley /Milner style type systems that deal with some form of constraints. Previous approaches use a syntactic notion of constraints. This can...
Analysis of Architectures using Constraint-Based Types (1998)
John Peterson, Martin Sulzmann
Constraint--based types provide a formal foundation for many varieties of architectural analysis. A software architecture, typically defined using an Architecture Definition Language (ADL), exposes...
Polymorphism in Hindley/Milner Style Type Systems with Constraints (1998)
. In this paper we consider Hindley/Milner style type systems that deal with some form of constraints. We study the interplay between polymorphism and constraints in such systems. Previous approaches...
Proofs of Properties about HM(X) (1998)
We present full of the properties about HM(X). HM(X) is a general framework for Hindley/Milner type systems with constraints. Specific type systems can be obtained by instantiating the constraint...
Designing record systems (1997)
We explore the design space for type systems with polymorphic records. We design record systems for extension, concatenation and removal of fields. Furthermore, we design a record system where field...
Type inference with constrained types (1997)
Martin Odersky, Martin Sulzmann, Martin Wehr
We present a general framework HM(X) for type systems with constraints. The framework stays in the tradition of the Hindley/Milner type system. Its type system instances are sound under a standard...
Proofs of Soundness and Completeness of Type Inference for HM(X) (1997)
this technical report one can find full proofs of soundness and completeness of type inference for the HM(X) type system [SOW97]. In Section 2 we introduce the notion of constraint systems. The HM(X)...
Type Inference with Constrained Types (1997)
Martin Sulzmann, Martin Odersky, Martin Wehr
In this paper we present a general framework HM(X) for Hindley/Milner style type systems with constraints. HM(X) stays in the tradition of the Hindley/Milner type system. Type systems in HM(X) are...