Chapter 6: Epigram Reloaded: A Standalone Typechecker for ETT

Chapman, James; Altenkirch, Thorsten; McBride, Conor
January 2007
Trends in Functional Programming Volume 6;2007, Vol. 6, p79
Epigram, a functional programming environment with dependent types, interacts with the programmer via an extensible high level language of programming constructs which elaborates incrementally into Epigram's Type Theory, ETT, a rather spartan λ-calculus with dependent types, playing the rôle of a 'core language'. We implement a standalone typechecker for ETT in Haskell, allowing us to reload existing libraries into the system safely without re-elaboration. Rather than adopting a rewriting approach to computation, we use a glued representation of values, pairing first-order syntax with a functional representation of its semantics, computed lazily. This approach separates β-reduction from βη- conversion. We consequently can not only allow the η-laws for λ-abstractions and pairs, but also collapse each of the unit and empty types.


Related Articles

  • The language of social software. Van Eijck, Jan // Synthese;Dec2010 Supplement, Vol. 177, p77 

    Computer software is written in languages like C, Java or Haskell. In many cases social software is expressed in natural language. The paper explores connections between the areas of natural language analysis and analysis of social protocols, and proposes an extended program for natural language...

  • POSSIBILITY OF FUNCTIONAL PROGRAMS VERIFICATION THROUGH APPLICATION OF MODEL CHECKING. Archvadze, Natela; Pkhovelishvili, Merab // Computer Science & Telecommunications;2013, Vol. 40 Issue 4, p51 

    The overall, ubiquitous computerization of all patterns of life makes the citizenry more and more vulnerable and dependent to the technology created by human. In this regards, the achievement of the required quality of the system software for the critical application is becoming the most...

  • A Taste of Functional Programming -- 2. Mukund, Madhavan // Resonance: Journal of Science Education;Sep2007, Vol. 12 Issue 9, p40 

    Functional programming has its roots in Alonzo Church's lambda calculus. In the first part of this article, we explored some basic notions of functional programming using the language Haskell. We now examine some more advanced concepts, including polymorphism, infinite data types and...

  • Chapter 2: A Static Checker for Safe Pattern Matching in Haskell. Mitchell, Neil; Runciman, Colin // Trends in Functional Programming Volume 6;2007, Vol. 6, p15 

    A Haskell program may fail at runtime with a pattern-match error if the program has any incomplete (non-exhaustive) patterns in definitions or case alternatives. This paper describes a static checker that allows non-exhaustive patterns to exist, yet ensures that a pattern-match error does not...

  • Chapter 4: A Purely Functional Implementation of ROBDDs in Haskell. Christiansen, Jan; Huch, Frank // Trends in Functional Programming Volume 7;2007, Vol. 7, p55 

    This paper presents an implementation of the ROBDD data structure in Haskell. It shows that lazy evaluation can be used to improve the performance of some ROBDD algorithms. While standard implementations construct the whole structure no matter which parts are demanded we use lazy evaluation to...

  • Chapter 1: Proof Support for General Type Classes. Van Kesteren, Ron; Van Eekelen, Marko; De Mol, Maarten // Trends in Functional Programming Volume 5;2006, Vol. 5, p1 

    We present a proof rule and an effective tactic for proving properties about HASKELL type classes by proving them for the available instance definitions. This is not straightforward, because instance definitions may depend on each other. The proof assistant ISABELLE handles this problem for...

  • Mining Frequent Patterns with Functional Programming. Kerdprasop, Nittaya; Kerdprasop, Kittisak // Enformatika;2007, Vol. 19, p282 

    Frequent patterns are patterns such as sets of features or items that appear in data frequently. Finding such frequent patterns has become an important data mining task because it reveals associations, correlations, and many other interesting relationships hidden in a dataset. Most of the...

  • Modular Polymorphic Defunctionalization. Fourtounis, Georgios; Papaspyrou, Nikolaos S.; Theofilopoulos, Panagiotis // Computer Science & Information Systems;Oct2014, Vol. 11 Issue 4, p1417 

    Defunctionalization is generally considered a whole-program transformation and thus incompatible with separate compilation. In this paper, we formalize a modular variant of defunctionalization which can support separate compilation for a functional programming language with parametric...

  • A Taste of Functional Programming -- 1. Mukund, Madhavan // Resonance: Journal of Science Education;Aug2007, Vol. 12 Issue 8, p27 

    The article explores some basic notions of functional programming via the programming language Haskell. John Backus, the inventor of the language FORTRAN, hypothesized that programming languages based on von Neumann bottleneck architecture were obliged to describe computation as a sequence of...


Read the Article


Sorry, but this item is not currently available from your library.

Try another library?
Sign out of this library

Other Topics