G'Caml -- evaluation with types --

Introduction

G'Caml is a variant of O'Caml compiler which extends ML parametric polymorphism to non-parametric one, called extensional polymorphism. Freed from the clear but simple parametricity, G'Caml provides many useful features which were impossible or very hard to achieve in O'Caml, such as overloading, type safe value marshalling, ML value printer, etc., etc.. With these long awaited functionalities, G'Caml will improve ML programming experience.

Distribution

G'Caml is a modification of O'Caml. With a special permission from the author of O'Caml, projet Cristal at INRIA Rocquencourt, G'Caml is distributed as a self-contained source archive:

cvs repository
Available as a branch "gcaml3101" at anonymous cvs server at camlcvs.inria.fr:
cvs -d :pserver:anoncvs@camlcvs.inria.fr:/caml co -r gcaml3101 ocaml

Contact

Please, do not ask G'Caml related questions to the original O'Caml authors. Such questions and reports are welcome at pj.ca.oykot-u.s.si.ly(a)esuruf.

G'Caml feature hightlights

Overloading
Values of different types can be overloaded to one identifier, i.e. (+) and (+.) will be unified!
Built-in ML value printer
Gprint.print prints your ML value as if you were in toplevel. You no longer need to define trivial but boring printers by yourself.
Type safe value input/output
Value marshaling (serialization) is now type-safe. Types of types are now checked at input, so that ill-typed value input is rejected at run-time, instead of crashing the program.

Overloading

Simple overloading

Let's start with an example:
let plus = generic (+) | (+.)
will define an overloaded function plus. This works as adding function for integers and floats, using (+) and (+.):
# plus 1 2;;
- : int = 3
# plus 2.3 4.5;;
- : float = 6.8

When plus is defined, its type also tells that you can use as int -> int -> int or float -> float -> float:

# let plus = generic (+) | (+.);;
val plus : [| int -> int -> int
| float -> float -> float |] = <generic>

Derived overloading

Using already defined overloaded values, you can define other overloaded values with the normal let:
# let double x = plus x x;;
val double :
{ 'a -> 'a -> 'a < [| int -> int -> int
| float -> float -> float |] } =>
'a -> 'a = <generic>
This double is also extensional polymorphic:
# double 1;;
- : int = 2
# double 1.2;;
- : float = 2.4

The type of double tells that it is basically a polymorphic function of the type 'a -> 'a, but its instantiation is actually constrained, which is explained inside {...} part. It saids that the instantiation is permitted only when 'a -> 'a -> 'a becomes a proper instance of the type of plus, [| int -> int -> int | float -> float -> float |]. This implies that double can be used for int -> int and float -> float.

Recursive overloading

Combinating overloading with recursion, you can write even more complex things: recursion over types:
# let rec print = generic
| print_int
| print_float
| : 'a list -> unit => function [] -> ()
| x::xs -> print x; print xs;;
val print :
[| int -> unit | float -> unit
| { 'b -> unit < 'a, 'b list -> unit < 'a } => 'b list -> unit |]
as 'a = <generic>
This overloaded value print works for printing integers and floats and their list of any depth!
# print 1;;
1- : unit = ()
# print 1.2;;
1.2- : unit = ()
# print [1; 2; 3];;
123- : unit = ()
# print [1.2; 3.4; 5.6];;
1.23.45.6- : unit = ()
# print [[1]; [2; 3]; [4; 5; 6]];;
123456- : unit = ()
# print [[[1.2]; [3.4; 5.6]]; [[7.89]]];;
1.23.45.67.89- : unit = ()

The trick is in the last overload case definition, whose code is a function over lists, function [] -> () | x::xs -> ... . It calls print twice recursively. The second one is the usual recursive call of print, in the same type of the caller. The first one is special: it is recursion over types.

The type annotation : 'a list -> unit => for the third case is required, when the case uses the overloaded value polymorphic-recursively.

Run time types

G'Caml has run time types, values which represent ML types. Definition of the run time types is given in stdlib/rtype.mli. It is almost identical to the representation of G'Caml's types, but the completely internal informations which are usually invisible to the users are removed.

Addition to the original contents of G'Caml's types, data type declaration information is attached to variant types. Using this type declaration values, we can define generic functions which works for various data types, for example. Type declaration information of data type t is obtained by the following typedecl expression:

typedecl t

NOTE

Type declaration contains recursive reference to itself when it is defined recursively. So be careful if you write a function which traverses type declaration values. You will be fallen into an infinite loop, unless you make a note of alrady visited type declarations.

LIMITATION

Only the basic part of types are supported at this moment, no fancy, modern class, object, polymorphic variant types! But they will be supported gradually.

Run time type construction syntax

You can build a value of run time type t using the notation [: t :]. For example,

[: int -> int :]

is the run time type representation of the type int -> int.

The scope of type variables inside [: :] notation is independent from the outside context. For instance, in the following expression,

fun (x:'a) -> [: int -> 'a :]

the first and second occurrences of the type variable 'a have no relationship each other. Even if the first 'a is instantiated to some other type, the second remains as a type variable:

fun (x:'a) -> [: int -> 'a :], x + 1

You can use ^x notation inside [: :], to substitute a run time type bound to a variable x. Ex:

let x = [: int :] in
[: ^x -> ^x :]

will return [: int -> int :]. This ^ notation can only take identifiers. For simplicity, you cannot write any other expressions, though they might be useful. For example, the following is NOT permitted:

[: ^(List.assoc "type" type_table) -> unit :]

You can use this [: :] notation also as patterns. For example:

match t with
| [: int :] -> ...
| [: float :] -> ...
| [: ^x -> ^y :] -> ...

As always, you cannot use one pattern variable ^x or one type variable 'a more than once.

Generic primitives

You can define "generic primitives". Ex:

generic val dyn : {'a} => 'a -> dyn =
fun ty v -> (ty,v)

generic val x : t = e defines a generic primitive x whose type scheme is t, whose semantics is given by the expression e. The expression e will first take run time type arguments, which inform the type instantiations of generalized type variables, specially listed in the constraint { } => of the type scheme t. In the above example, the expression (fun ty v -> (ty,v)) will takes a run time type of the instantiation of the generalized type variable 'a of the value dyn, then create a tuple of the type and the value.

Note that the type annotation t is not a type constraint, but the true type scheme of the defined value.

Bugs and non-implemented features