Idris is an experimental language with full dependent types. Dependent types allow types to be predicated on values, meaning that some aspects of a program's behaviour can be specified precisely in the type. The language is closely related to Epigram and Agda. The aims of the project are: * To provide a platform for realistic programming with dependent types. By realistic, we mean the ability to interact with the outside world and use primitive types and operations. This includes networking, file handling, concurrency, etc. * To show that full dependent types do not mean we have to abandon the functional style we have come to know and love with languages like Haskell and OCaml. lightweight dependently typed programming means allowing the programmer full access to values in types, and letting the type checker do the hard work so you don't have to! Future plans include some more useful syntax (local definitions/where clauses being the most important), a compiler,
au:chlipala Ur introduces richer type system features into FP. Ur is functional, pure, statically-typed, and strict. Ur supports metaprogramming based on row types. Ur/Web is standard library and associated rules for parsing and optimization. Ur/Web supports construction of dynamic web applications backed by SQL databases. The signature of the standard library is such that well-typed Ur/Web programs "don't go wrong" in a very broad sense. They also may not: * Suffer from any kinds of code-injection attacks * Return invalid HTML * Contain dead intra-application links * Have mismatches between HTML forms and the fields expected by their handlers It is also possible to use metaprogramming to build significant application pieces by analysis of type structure - demo includes an ML-style functor for building an admin interface for an arbitrary SQL table. The Ur/Web compiler also produces very efficient object code that does not use gc
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.
J. Gibbons, and G. Jones. Proceedings of the third ACM SIGPLAN international conference on Functional programming - ICFP '98, page 273--279. New York, ACM Press, (1998)
T. Harris, S. Marlow, S. Peyton-Jones, and M. Herlihy. Proceedings of the tenth ACM SIGPLAN symposium on Principles and practice of parallel programming, page 48--60. New York, NY, USA, ACM, (2005)
R. Hinze, N. Wu, and J. Gibbons. Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming, page 209--220. New York, NY, USA, ACM, (2013)
M. Hofmann, E. Kitzelmann, and U. Schmid. German Conference on Artificial Intelligence (KI'08), volume 5243 of LNAI, page 78--86. Springer-Verlag, (2008)