• Introduction
• Simplistic GADTs in OCaml
• GADTs
• Towards open GADTs: extensible evaluator for a typed object language
  
• Generics for the OCaml masses

This is joint work with Jeremy Yallop.

---

Introduction

First-class modules introduced in OCaml 3.12 make type constructors first-class, permitting type constructor abstraction and polymorphism. It becomes possible to manipulate and quantify over types of higher kind. We demonstrate that as a consequence, full-scale, efficient generalized algebraic data types (GADTs) become expressible in OCaml 3.12 as it is, without any further extensions. Value-independent generic programming along the lines of Haskell's popular ``Generics for the masses'' become possible in OCaml for the first time. We discuss extensions such as a better implementation of polymorphic equality on modules, which can give us intensional type analysis (aka, type-case), permitting generic programming frameworks like SYB.

References

first-class-modules.pdf [69K]
first-class-modules-talk.pdf [126K]
first-class-modules-talk-notes.pdf [160K]
The extended abstract and the (annotated) slides of the talk presented at the 2010 ACM SIGPLAN Workshop on ML. Baltimore, MD, September 26, 2010. The talk illustrates using GADTs to implement n-morphic data structures.

Alain Frisch and Jacques Garrigue: First-class modules and composable signatures in Objective Caml 3.12
< http://www.math.nagoya-u.ac.jp/~garrigue/papers/ml2010.pdf >
< http://www.math.nagoya-u.ac.jp/~garrigue/papers/ml2010-show.pdf >
The extended abstract and the slides of the talk by the implementors of the first-class modules. The talk was given at the 2010 ACM SIGPLAN Workshop on ML. Baltimore, MD, September 26, 2010.

Simplistic GADTs in OCaml

We illustrate one simplistic, pure, magic-free implementation of a form of GADTs in OCaml that is sufficient for the common applications of GADTs such as data structures with embedded invariants, typed printf/scanf, tagless interpreters. The implementation is a simple module, requiring no changes to the OCaml system. The implementation, based on the common technique of term witnesses of type equality, is so trivial that it should work on any ML system (although, like nested data types, GADTs aren't very useful on an SML system without support for polymorphic recursion).

Our examples include:

• enforcing invariants on data structures: statically ensuring that in a tree representation of an HTML document, a link node is never an ancestor of another link node;
• typed printf/scanf sharing the same format descriptor, which is first-class and can be built incrementally;
• simply typed lambda-calculus with constants and higher-order abstract syntax. This is essentially the example of Hongwei Xi's et al. POPL 2003 paper.

We see that common GADTs are available in OCaml here and now. We can truly write the published examples that motivated GADTs, without too much violence to their notation. We can translate GADT code from Haskell, more or less mechanically. No changes to the OCaml type system or the type checker are necessary. Of course changes such as explicit existential quantification, better support for rank-2 types, etc. shall be greatly appreciated -- but they are not necessary to start using and enjoying GADTs. First-class modules introduced in OCaml 3.12 let us implement genuine Leibniz equality and better GADTs.

Version

The current version is 1.1, July 10, 2009.

References

GADT.txt [7K]
The introductory article posted on the caml-list on 2009年7月10日 20:05:10 -0700 (PDT)

GADT.ml [15K]
Complete, commented OCaml code for the library and three examples

Patricia Johann and Neil Ghani: Foundations for Structured Programming with GADT. POPL 2008.

Formatted IO as an embedded DSL: the initial view
The article demonstrates typed printf and scanf sharing the same format descriptor, implemented as interpreters of the DSL defined via GADT. We re-implement that Haskell code in OCaml.

GADTs

GADTs

First-class modules -- first-class functors -- permit type constructor abstraction and polymorphism. Type constructor polymorphism makes it possible to encode genuine Leibniz equality. The latter, along with existentials and polymorphic recursion (both of which can also be encoded with first-class modules), let us implement GADTs. We can now work with ``real'' GADTs in OCaml, without the need for extensions.

GADTs let us express a form of bounded polymorphism, where only some instances of a type schema are populated. The populated instances represent a relation among types -- the role GADTs share with type classes.

The injectivity of our GADTs is, alas, rather restricted: it holds only for functors, and only after we downgrade GADTs to simplistic GADTs.

Version

The current version is June 2010.

References

polyrec.ml [5K]
Six encodings of polymorphic recursion in OCaml 3.12, including two hitherto unavailable encodings using first-class modules

existentials.ml [7K]
Encoding of existentials via first-class modules, including existentials over higher-kinded types

leibniz.ml [5K]
Genuine Leibniz equality

gadts.ml [10K]
GADTs in OCaml, via Leibniz equality.
The code includes common examples of GADTs: typed printf/scanf and an evaluator for a typed object language.

first-class-modules-talk.pdf [126K]
first-class-modules-talk-notes.pdf [160K]
The ML 2010 talk develops an extended example of using GADTs to implement n-morphic data structures.

Generics for the OCaml masses

Generic programming in ML typically relies on the value representation of types. In most generic programming libraries so far the type representation was a collection of generic functions specialized for that particular type. First-class modules permit for the first time value-independent generic programming. A type s is represented as a value of the type s repr:

 module type Interpretation : sig
 type 'a tc
 val unit : unit tc
 val int : int tc
 val ( * ) : 'a tc -> 'b tc -> ('a * 'b) tc
 (* ... *)
 end
 
 module type Repr = sig
 type a
 module Interpret (I : Interpretation) : sig val result : a I.tc end
 end
 
 type 'a repr = (module Repr with type a = 'a)
 
 val show : 'a. 'a repr -> 'a -> string

The type representation Repr contains no information about specific generic functions such as show. Rather, Repr receives the interpretation from the user and selects the one that pertains to the represented type. A generic function like show takes the type representation s repr and supplies the Interpretation argument, describing how to show primitive and composite types.

Here is a simple example of using generics:

 ~/first-class-modules> ocamlc -c generics.ml 
 ~/first-class-modules> ocaml generics.cmo
 Objective Caml version 3.12.0
 
 # open Generics;;
 # print_endline (show (option int * string) (Some 3, "four"));;
 (Some 3,"four")
 - : unit = ()

Version

The current version is June 2010.

References

generics.ml [18K]
The fully developed Repr for most OCaml types and several sample generic functions such as generic show and generic equality.

Towards open GADTs: extensible evaluator for a typed object language

References

open_gadts.ml [7K]
Building typed interpreters by composing fragments

Last updated October 7, 2010

This site's top page is http://okmij.org/ftp/

Converted from HSXML by HSXML->HTML