"Generalized Algebraic Data Structures" have become a a hot new topic. They have recently been added to the GHC compiler. They support the construction, maintenance, and propagation of semantic properties of programs using powerful old ideas about types (the Curry-Howard Isomorphism) in surprisingly easy to understand new ways. The language Omega was designed and implemented to demonstrate their utility. Here a a few talks I gave that explains how they work. Also class lectures
demonstrates that sprintf and sscanf can indeed use exactly the same formatting specification, which is a first-class value. We demonstrate typed sprintf and typed sscanf sharing the same formatting specification. Our solution is surprisingly trivial: it defines a simple embedded domain-specific language of formatting patterns. The functions sprintf and sscanf are two interpreters of the language, to build or parse a string according to the given pattern. Our solution relies only on GADTs. We demonstrate that lambda-abstractions at the type level are expressible already in the Hindley-Milner type system; GADT with the included polymorphic recursion help us use the abstractions.
My existing research is mainly focused on lightweight generic programming techniques and the essence of (OO-style) design patterns. * Modular Visitor Components: A Practical Solution to the Expression Families Problem Bruno C. d. S. Oliveira ECOOP 2009. * Scala for Generic Programmers Bruno C. d. S. Oliveira, Jeremy Gibbons In Ralf Hinze, editor, Proceedings of the ACM SIGPLAN Workshop on Generic Programming (WGP'08) July 2008. * Objects to Unify Type Classes and GADTs Bruno C. d. S. Oliveira, Martin Sulzmann ICFP 2008
Dependent type systems, in which types can depend on values, admit detailed specifications of function behavior and data invariants. Programming languages based on System F do not have dependent types, and are therefore more limited in what structure or function invariants can be encoded in the type system. In this paper, we show how guarded algebraic datatypes can simulate dependent types. We formalize additions to a guarded-datatypes-enhanced System F that allow types to depend on values and discuss the programming style that results, which is similar to theorem proving. Our technique can be applied to multiple existing programming languages, including Haskell and C#. We also introduce an idiom for eliminating any execution cost from programming with simulated dependent types. We have developed a tool to automatically produce the boilerplate necessary for the simulation, and we have used it to enforce data structure invariants and to allow elision of run-time bounds checks.
S Peyton Jones, D Vytiniotis, S Weirich, and G Washburn, ICFP 2006, pp50-61 Generalized algebraic data types (GADTs), sometimes known as "guarded recursive data types" or "first-class phantom types", are a simple but powerful generalization of the data types of Haskell and ML. Recent works have given compelling examples of the utility of GADTs, although type inference is known to be difficult. Our contribution is to show how to exploit programmer-supplied type annotations to make the type inference task almost embarrassingly easy. Our main technical innovation is wobbly types, which express in a declarative way the uncertainty caused by the incremental nature of typical type-inference algorithms. [This is a version of Wobbly types: type inference for generalised algebraic data types. Relative to ICFP 2006, the PDF above also describes a simplification to the type system, at the cost of extra annotation burden. This simpler system is the one actually implemented in GHC 6.8]
GADTs are obviously currently a hot topic in functional programming research. Most of the papers focus only on the GADT mechanism (how type checking works etc.). The only example that one usually sees is the "typed evaluator". I am not an expert on this topic, and I'd like to know more about how they would actually be useful in practical programming. For example, I wonder how a parser would look like if it is impossible to construct "wrong" ASTs. Would type checking then effectively take place during parsing? How would a type error in the parsed program be detected and thrown? GADTs are a mechanism for defining more precise types. It helps you make stronger guarantees on an AST structure, which reduces the number of explicit consistency checks you have to perform in code. GADTs are very useful for deriving combinator libraries in the style of John Hughes. Andres Loh shows an embedded DSL for contracts in Haskell using GADTs in Typed Contracts for Functional Programming.
Chameleon (the language) is a Haskell style language to experiment with advanced type extensions such as type classes and generalized algebraic data types. The user can program her own type extensions via Constraint Handling Rules (CHRs). Chameleon (the system) is also a compiler framework. Chameleon has been applied in a number of project such as type error reporting, programming language program verification etc. In the XHaskell implementation we heavily rely on the compiler infrastructure provided by Chameleon. Language Features * LanguageOverview * HowtoinstallandrunChameleon The Compiler * CompilerOverview * ChameleonGecko * StandaloneSolver Applications *TypeErrorDiagnosis *ProgramVerification MartinSulzman
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.
The Curry-Howard isomorphism states that types are propositions and that programs are proofs. This allows programmers to state and enforce invariants of programs by using types. Unfortunately, the type systems of today's functional languages cannot directly express interesting properties of programs. To alleviate this problem, we propose the addition of three new features to functional programming languages such as Haskell: Generalized Algebraic Datatypes, Extensible Kind Systems, and the generation, propagation, and discharging of Static Propositions. These three new features are backward compatible with existing features, and combine to enable a new programming paradigm for functional programmers. This paradigm makes it possible to state and enforce interesting properties of programs using the type system, and it does this in manner that leaves intact the functional programming style, known and loved by functional programmers everywhere.
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.