Thorsten Altenkirch, Neil Ghani, Peter Hancock, Conor Mcbride, Peter Morris
Abstract. The search for an expressive calculus of datatypes in which canonical algorithms can be easily written and proven correct has proved to be an enduring challenge to the theoretical computer...
Chapter 1 Epigram Reloaded: (2008)
A Standalone, Typechecker Ett, James Chapman, Thorsten Altenkirch, Conor Mcbride
Abstract Epigram, a functional programming environment with dependent types, interacts with the programmer via an extensible high level language of programming constructs which elaborates...
Abstract Observational Equality, Now! (2008)
Thorsten Altenkirch, Conor Mcbride, Wouter Swierstra
This paper has something new and positive to say about propositional equality in programming and proof systems based on the Curry-Howard correspondence between propositions and types. We have found a...
Chapter 1 Epigram Reloaded: (2008)
A Standalone, Typechecker Ett, James Chapman, Thorsten Altenkirch, Conor Mcbride
Abstract Epigram, a functional programming environment with dependent types, interacts with the programmer via an extensible high level language of programming constructs which elaborates...
Applicative programming with effects (2008)
In this paper, we introduce Applicative functors—an abstract characterisation of an applicative style of effectful programming, weaker than Monads and hence more widespread. Indeed, it is the...
1 Motivation Epigram: Practical Programming with Dependent Types (2008)
Find the type error in the following Haskell expression: if null xs then tail xs else xs You can’t, of course: this program is obviously nonsense unless you’re a typechecker. The trouble is that...
Idioms: applicative programming with effects (2008)
In this paper, we introduce Idioms—an abstract characterisation of an applicative style of effectful programming, weaker than Monads and hence more widespread. Indeed, it is the ubiquity of this...
∂ for Data: Differentiating Data Structures (2008)
Michael Abbott, Neil Ghani, Thorsten Altenkirch, Conor Mcbride
This paper and our conference paper (Abbott, Altenkirch, Ghani, and McBride, 2003b) explain and analyse the notion of the derivative of a data structure as the type of its one-hole contexts based on...
Applicative programming with effects (2008)
In this paper, we introduce Applicative functors—an abstract characterisation of an applicative style of effectful programming, weaker than Monads and hence more widespread. Indeed, it is the...
1 INTRODUCTION Epigram Reloaded: (2008)
A Standalone, Typechecker Ett, James Chapman, Thorsten Altenkirch, Conor Mcbride
Thorsten Altenkirch, Neil Ghani, Peter Hancock, Conor Mcbride, Peter Morris
Abstract. The search for an expressive calculus of datatypes in which canonical algorithms can be easily written and proven correct has proved to be an enduring challenge to the theoretical computer...
Abstract Observational Equality, Now! (2008)
Thorsten Altenkirch, Conor Mcbride, Wouter Swierstra
This paper has something new and positive to say about propositional equality in programming and proof systems based on the Curry-Howard correspondence between propositions and types. We have found a...
Dependent types reflect the fact that validity of data is often a relative notion by allowing prior data to affect the types of subsequent data. Not only does this make for a precise type system, but...
First-order unification algorithms (Robinson, 1965) are traditionally implemented via general recursion, with separate proofs for partial correctness and termination. The latter tends to involve...
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,...
Eliminating dependent pattern matching (2006)
Healfdene Goguen, Conor Mcbride, James Mckinna
Abstract. This paper gives a reduction-preserving translation from Coquand’s dependent pattern matching [4] into a traditional type theory [11] with universes, inductive types and relations and the...
Eliminating dependent pattern matching (2006)
Healfdene Goguen, Conor Mcbride, James Mckinna
Abstract. This paper gives a reduction-preserving translation from Coquand’s dependent pattern matching [4] into a traditional type theory [11] with universes, inductive types and relations and the...
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...
Towards observational type theory (2006)
Thorsten Altenkirch, Conor Mcbride
Observational Type Theory (OTT) combines beneficial aspects of Intensional and Extensional Type Theory (ITT/ETT). It separates definitional equality, decidable as in ITT, and a substitutive...
Towards observational type theory (2006)
Thorsten Altenkirch, Conor Mcbride
Observational Type Theory (OTT) combines beneficial aspects of Intensional and Extensional Type Theory (ITT/ETT). It separates definitional equality, decidable as in ITT, and a substitutive...
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...
Generic programming with dependent types (2006)
Thorsten Altenkirch, Conor Mcbride, Peter Morris
In these lecture notes we give an overview of recent research on the relationship
Eliminating dependent pattern matching (2006)
Healfdene Goguen, Conor Mcbride, James Mckinna
Abstract. This paper gives a reduction-preserving translation from Coquand’s dependent pattern matching [4] into a traditional type theory [11] with universes, inductive types and relations and the...
Based on the ideas presented in [McBride and Paterson, 2005], Control.Applicative and Data.Traversable are now to be found in the Standard Library. This module delivers a collection of goodies which...
Why dependent types matter (2005)
Thorsten Altenkirch, Conor Mcbride, James Mckinna
We exhibit the rationale behind the design of Epigram, a dependently typed programming language and interactive program development system, using refinements of a well known program—merge sort—as...
A few constructions on constructors (2005)
Conor Mcbride, Healfdene Goguen, James Mckinna
Abstract. We present four constructions for standard equipment which can be generated for every inductive datatype: case analysis, structural recursion, no confusion, acyclicity. Our constructions...
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...
The Epigram Prototype: a nod and two winks (2005)
I intend this document as a guide to the prototype EPIGRAM system. As things stand, there are still a great many things which need to be done, but the system can now be
Haskell Communities and Activities Report (2005)
Andres Löh (ed, Perry Alexander, Lloyd Allison, Tiago Miguel, Laureano Alves, Krasimir Angelov, ...
You are reading the 8th edition of the Haskell Communities and Activities Report (HCAR). These are interesting times to be a Haskell enthusiast. Everyone seems to be talking about darcs ( → 6.3)...
Why dependent types matter (2005)
Thorsten Altenkirch, Conor Mcbride, James Mckinna
We exhibit the rationale behind the design of Epigram, a dependently typed programming language and interactive program development system, using refinements of a well known program—merge sort—as...
Exploring the regular tree types (2004)
Peter Morris, Thorsten Altenkirch, Conor Mcbride
Abstract. In this paper we use the Epigram language to define the universe of regular tree types—closed under empty, unit, sum, product and least fixpoint. We then present a generic decision...
Constructing polymorphic programs with quotient types (2004)
Michael Abbott, Thorsten Altenkirch, Neil Ghani, Conor Mcbride
Abstract. The efficient representation and manipulation of data is one of the fundamental tasks in the construction of large software systems. Parametric polymorphism has been one of the most...
Haskell Communities and Activities Report (2004)
Andres Löh (ed, Perry Alexander, Lloyd Allison, Krasimir Angelov, Alistair Bayley, Jérémy Bobbio, ...
Welcome to the Seventh edition of the Haskell Communities and Activities report. I can proudly announce that the report has survived yet another change of editor, and chances are good that this...
Exploring the regular tree types (2004)
Peter Morris, Thorsten Altenkirch, Conor Mcbride
Abstract. In this paper we use the Epigram language to define the universe of regular tree types—closed under empty, unit, sum, product and least fixpoint. We then present a generic decision...
Inductive families need not store their indices (2004)
Edwin Brady, Conor Mcbride, James Mckinna
Abstract. We consider the problem of efficient representation of dependently typed data. In particular, we consider a language TT based on Dybjer's notion of inductive families [11] and...
I am not a number: I am a free variable (2004)
In this paper, we show how to manipulate syntax with binding using a mixed representation of names for free variables (with respect to the task in hand) and de Bruijn indices [dB72] for bound...
Generic programming within dependently typed programming (2003)
Thorsten Altenkirch, Conor Mcbride
Abstract We show how higher kinded generic programming can be represented faithfully within a dependently typed programming system. This development has been implemented using the Oleg system. The...
Derivatives of containers (2003)
Michael Abbott, Thorsten Altenkirch, Neil Ghani, Conor Mcbride
Abstract. We are investigating McBride’s idea that the type of one-hole contexts are the formal derivative of a functor from a categorical perspective. Exploiting our recent work on containers we...
Derivatives of containers (2003)
Michael Abbott, Thorsten Altenkirch, Neil Ghani, Conor Mcbride
Abstract. We are investigating McBride’s idea that the type of one-hole contexts are the formal derivative of a functor from a categorical perspective. Exploiting our recent work on containers we...
Elimination with a Motive (2002)
Abstract. I present a tactic, BasicElim, for Type Theory based proof systems to apply elimination rules in a refinement setting. Applicable rules are parametric in their conclusion, expressing the...
Derivatives of Containers (2002)
Michael Abbott, Thorsten Altenkirch, Neil Ghani, Conor Mcbride
Abstract. We are investigating McBride's idea that the type of onehole contexts are the formal derivative of a functor from a categorical perspective. Exploiting our recent work on containers we...
The derivative of a regular type is its type of one-hole contexts. Unpublished manuscript (2001)
Polymorphic regular types are tree-like datatypes generated by polynomial type expressions over a set of free variables and closed under least fixed point. The `equality types ' of Core ML can...
Dependently Typed Functional Programs and their Proofs (2000)
Research in dependent type theories [ML71a] has, in the past, concentrated on its use in the presentation of theorems and theorem-proving. This thesis is concerned mainly with the exploitation of the...
Dependently Typed Functional Programs and their Proofs (2000)
Research in dependent type theories [ML71a] has, in the past, concentrated on its use in the presentation of theorems and theorem-proving. This thesis is concerned mainly with the exploitation of the...
Dependently Typed Functional Programs and their Proofs (1999)
Research in dependent type theories [M-L71a] has, in the past, concentrated on its use in the presentation of theorems and theorem-proving. This thesis is concerned mainly with the exploitation of...
Dependently Typed Functional Programs and their Proofs (1999)
Research in dependent type theories [M-L71a] has, in the past, concentrated on its use in the presentation of theorems and theorem-proving. This thesis is concerned mainly with the exploitation of...
Dependently Typed Functional Programs and their Proofs (1999)
Research in dependent type theories [M-L71a] has, in the past, concentrated on its use in the presentation of theorems and theorem-proving. This thesis is concerned mainly with the exploitation of...
Inverting inductively defined relations in LEGO (1998)
Inverting an inductively defined relation essentially consists of observing that any of its inhabitants must be derivable by at least one of its inference rules. For example, let us define...
Inverting Inductively Defined Relations in LEGO
this paper. Its specification is clear, it is sound and complete with respect to constructor forms and the tactic Qnify, to which it gives rise, has proved independently useful.