Logically Qualified Data Types, abbreviated to Liquid Types, a system that combines Hindley-Milner type inference with Predicate Abstraction to automatically infer dependent types precise enough to prove a variety of safety properties. Liquid types allow programmers to reap many of the benefits of dependent types, namely static verification of critical properties and the elimination of expensive run-time checks, without manual annotation. We have implemented liquid type inference in Dsolve, which takes as input an Ocaml program and a set of logical qualifiers and infers dependent types for the expressions in the Ocaml program.We describe experiments using Dsolve to statically verify the safety of array accesses on a set of Ocaml benchmarks that were previously annotated as part of the DML project. When used with a simple set of bounds checking qualifiers, Dsolve reduces manual annotation required from 31% of program text to under 1%.
Dependent type theory is rich enough to express that a program satisfies an input/output relational specification, but it could be hard to construct the proof term. On the other hand, squiggolists know very well how to show that one relation is included in another by algebraic reasoning. We demonstrate how to encode functional and relational derivations in a dependently typed programming language. A program is coupled with an algebraic derivation from a specification, whose correctness is guaranteed by the type system. Code accompanying the paper has been developed into an Agda library AoPA.
popl2008 ** 1. GADTs are syntactic sugar. The real structures at work are existentially quantified types and the equality GADT. 2. Indexing by a set, rather than a category, as GADTs do means that really this is dependently typed programming faked in Haskell by using kind level proxies for types 3. As a result, Haskell ends up with a curious "logic programming" feel to its type level computation and functional programming feel to its term-level computation. PJohann and NGhani ** his main point (which worked with me) is that we should pay more attention Kan extensions. We already know and love (strong) functors, (co)monads, adjunctions and the Yoneda lemma.
Total Functional Programming Here's an interesting paper recently mention in another thread: Total Functional Programming... Abstract: The driving idea of functional programming is to make programming more closely related to mathematics. A program in a functional language such as Haskell or Miranda consists of equations which are both computation rules and a basis for simple algebraic reasoning about the functions and data structures they define. The existing model of functional programming, although elegant and powerful, is compromised to a greater extent than is commonly recognized by the presence of partial functions. We consider a simple discipline of total functional programming designed to exclude the possibility of non-termination. Among other things this requires a type distinction between data, which is finite, and codata, which is potentially infinite. I presume that the bogus definiton of "fib" is a subtle reminder of the importance of eliminating bottom.