This is joint work with Jeremy Yallop.
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.
Our examples include:
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.
caml-list
on Fri, 10 Jul 2009 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 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.
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.
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 -> stringThe 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 = ()
Repr
for most OCaml types and several sample generic functions such as generic show and generic equality.oleg-at-okmij.org
Your comments, problem reports, questions are very welcome!
Converted from HSXML by HSXML->HTML