A Tutorial Implementation of a Dependently Typed Lambda Calculus Andres Löh, Conor McBride and Wouter Swierstra We present the type rules for a dependently-typed core calculus together with a straightforward implementation in Haskell. We explicitly highlight the changes necessary to shift from a simply-typed lambda calculus to the dependently-typed lambda calculus. We also describe how to extend our core language with data types and write several small example programs. The paper is accompanied by an executable interpreter and example code that allows immediate experimentation with the system we describe. Download Draft Paper (submitted to FI) Haskell source code (executable Haskell file containing all the code from the paper plus the interpreter; automatically generated from the paper sources) prelude.lp (prelude for the LambdaPi interpreter, containing several example programs) Instructions (how to get started with the LambdaPi interpreter)
August 6, 2007 I am curious about the possibility of developing Haskell programs spontaneously with proofs about their properties and have the type checker verify the proofs for us, in a way one would do in a dependently typed language. In the exercise below, I tried to redo part of the merge-sort example in Altenkirch, McBride, and McKinna’s introduction to Epigram: deal the input list into a binary tree, and fold the tree by the function merging two sorted lists into one. The property I am going to show is merely that the length of the input list is preserved. To begin with, we define the usual type-level representation of natural numbers and lists indexed by their lengths.
In the previous post, we talked about some of the basics of functional programming unit testing. That post mostly focused around HUnit, which is a traditional xUnit testing framework. This time, let's focus on type-based property testing, which is to create specs which assert logical properties about a function, and then to generate data to test in an attempt to falsify these assertions, through the use of a tool called QuickCheck. Much like the traditional xUnit frameworks, this tool helps us flush out the specifications of our software through the use of tests. Unlike the xUnit frameworks, however, this framework allows us to create generators to help flush out our behaviors and capture our edge cases as we look for ways to falsify our tests. These generators could use either random data or well structured data that you can craft. Let's dive a little deeper into what that means.
Efficiently translating Haskell to JVM Bytecode using GHC's intermediate language, STG. LambdaVM is the proof that complete and efficient translation is possible. LambdaVM is a set of patches to GHC's which extend it to fully support generating useable JVM bytecode. It modifies the three primary components of GHC: * The compiler itself: The compiler has been modified to transform STG, one of GHC's many intermediate languages, to JVM bytecode. * The runtime system (RTS): GHC's RTS implemented as a mix of C and C-- has been reimplemented in Java. * The base libraries: GHC's base libraries have been modified to run on top of Java's standard libraries rather than ANSI C/POSIX libraries. October, 2008 Update LambdaVM is coming back! I've fixed all the GHC 6.8.x build problems and the instructions below should once again work. LambdaVM itself is still based on a circa November, 2007 GHC HEAD but moving all my changes to the current HEAD is next
There are two schools of thought when it comes to documenting programs and libraries: some embed fragments of code within the documentation (so called “literate programming”) and others embed fragments of documentation in their code (i.e. comments). The “comments” approach makes it easy to generate API documentation and the like (a feature built-in to Haskell’s Hackage system) but help me write blog posts and other documents containing code, which is where literate programming shines. Happily, Haskell supports both of these approaches and has a few rather useful tools available to make both easier. In this post, I’ll describe how to take literate Haskell with Markdown formatted text and produce syntax highlighted documents in HTML and PDF.
One of the pleasant new features in GHC 6.10 is the long-awaited addition of view patterns. This feature is usually advertised as making it possible to pattern match against the values of an abstract type. An essential aspect of modular software design is that we don't want to expose the implementation of complex code. Someone will surely come along and start making decisions based on bits of our code that they can see, thus limiting our future room to manoeuvre. This is all amply explained on the view pattern wiki page and in the GHC User's Guide. how do they diff from f# active pats
This article is part three in a series on introductory Haskell programming. In the first article, we wrote a small program to recursively scan file-system directories and print their contents as ASCII-art trees. In the second article, we refactored the program to make its logic more reusable by separating the directory-scanning logic from the tree-printing logic. In this article, we will address a shortcoming of the refactored version: It must scan directory hierarchies completely before printing their trees, i.e., it must scan and then print, when doing both simultaneously is both more efficient and more user friendly. Recall from the previous article that our directory-printing program is factored into three pieces of logic:
Haskell's overloaded numerical classes can be (ab)used to do some symbolic maths. This is in no way a new discovery, but I thought I'd write a few lines about it anyway since I've been playing with it the last few days. First we need a data type to repres
Haskell lets you write some strange-looking programs in a style known as "circular programming." Imagine transforming a tree with integer leaves into a tree that replaces all the leaves with the minimum leaf value. Normally we'd do this in two passes: first find the minimum leaf, and then traverse the tree a second time, replacing the leaves with the minimum value. In a lazy language you can do this in one go
DoCon is a program for symbolic computation in mathematics - package of modules DoCon joins the categorial approach to the mathematical computation expressed via the Haskell type classes, and explicit processing of the domain description terms. It implements recently a good piece of commutative algebra: linear algebra, polynomial gcd, factorization, Groebner bases, and other functions. They are programmed under the very generic assumptions , like "over any Euclidean ring", over any GCD-ring, any field, and so on. DoCon also supports the constructions on domains: Fraction, Polynomial, Residue ring, and others. That is certain set of operations on a constructed domain is built automatically.