Well, three years later, I can only be happy that we made this decision (though I was accused for turning OCaml into Python). But the truth is that you have a rather unpleasant choice, either keep your AST untyped and always fear that is won’t be well-formed or add weak typing to it. It has to be weak because you will still need to unparse it from the untyped representation so you had to reify the typing into the language. However, after we recovered the type we might find ourselves in need to forget it. Yes, it is nice to have i32 bitv value and i8 bitv value so that the typechecker will prevent us from adding them together without proper casting (well, and the casting itself, requires casting on the host language), but we would also like to store all these values in a mapping or a set. Or, again, to serialize them. It is also important to notice, that our weak types are witnessed by concrete representations of sorts so you can’t cast an 8-bit value into 32-bit value.
Just by curiosity, how do you implement dynamic typing: with type trickery like this?
type _ dyn_typ = ..
type _ dyn_typ +=
| Int : int dyn_typ
| Float : float dyn_typ
| List : 'a dyn_typ -> 'a list dyn_typ
(* dynamically typed languages have only one type, namely top *)
type top = Any : 'a dyn_typ * 'a -> top
let typeof (Any (typ, _)) =
let rec aux : type a. a dyn_typ -> string = fun typ ->
match typ with
| Int -> "int"
| Float -> "float"
| List t -> Printf.sprintf "list of %s" (aux t)
| _ -> assert false
in aux typ
let any typ v = Any (typ, v)
typeof (any Int 3);;
- : string = "int"
typeof (any (List Int) [1; 3]);;
- : string = "list of int"
Not like this, this won’t work as we need to serialize the typing information and restore it back. And we need to do this across different compilations (compiled with different compiler versions on different architectures). So GADT is a no-no for us.
Before going further, we separate classes and sorts. Where class is a collection of sorts. For example, we have classes such as values, effects, and programs, and each class is further subdivided into a potentially infinite quotient set of sorts, e.g., we have i bitvec values, where i is the type index for the size of the bitvector, which is countably infinite. Correspondingly we have memories that are indexed with two types, e.g., (p bitvec, v bitvec) mem values which is a storage for v bitvec objects indexed with p bitvec addresses. And so on, the sorts could be quite complex, as for example a sort for IEEE754 floating-point values, which has to track the representation, such as the number of bits in the number’s constituents, whether it is binary or decimal and so on. The same is with effects, we distinguish between control effects and jump effects.
The classes are typed statically, and it is very important because the class defines what slots a value can have. Contrary, the sorts are weakly indexed with phantom types. That means that those types exist only in the signatures, and in the implementation, we’re free to mess with them. We represent sorts of values algebraically, as we need an infinite set of sorts and need them to keep the typing information. Therefore here is our representation of a sort,
type t =
| Sym of name
| Int of int
| App of {args : t list; name : name option}
[@@deriving bin_io, compare, sexp]
end
type +'a exp = Exp.t
type +'a t = 'a exp
type top = unit t
And sort equality is just derived from the equality of the sort constructors,
let refine witness t = match t with
| App {name=Some name}
| Sym name when [%compare.equal: name] name witness -> Some t
| _ -> None
let forget : 'a t -> unit t = ident
And the names, which are witnesses are private to each module that makes the module that defines the sort to be the only point of failure, which is fully responsibly for the type rules of that sort, as this module and only this can provide the type casting operator, e.g.,
module Bitv : sig
type 'a t
val define : int -> 'a t sort
val refine : unit sort -> 'a t sort option
val size : 'a t sort -> int
end
Yes, using variants to implement the polymorphism to which you refer makes it harder to add new shapes. You have to revise all existing functions, including those in other compilation units, which operate on the set of shapes in question in order to accommodate a new addition to the set. However, variants makes it easy to add new behaviors for any given set of shapes.
For completeness, here’s a simple object implementation:
module Surface = struct
type t
end
class point x y =
object (self)
val x : int = x
val y : int = y
method area : int = 1
method draw (surface : Surface.t) : unit = ()
end
class rectangle = object (self)
val bottom_left : point = new point 1 2
val top_right : point = new point 3 4
method area : int = 1
method draw (surface : Surface.t) : unit = ()
end
let l = [new point 1 2; new rectangle]
let areas = List.map (fun s -> s#area) l
They can be wrapped in modules to hide the details of the type:
module Surface = struct
type t
end
module type SHAPE = sig
type c = < area : int; draw : Surface.t -> unit >
val make : unit -> c
end
module Point : SHAPE = struct
class c x y = object (self)
val x : int = x
val y : int = y
method area : int = 1
method draw (surface : Surface.t) : unit = ()
end
let make () = new c 1 2
end
module Rectangle : SHAPE = struct
class c = object (self)
val bottom_left : Point.c = Point.make ()
val top_right : Point.c = Point.make ()
method area : int = 1
method draw (surface : Surface.t) : unit = ()
end
let make () = new c
end
let l = [Point.make (); Rectangle.make ()]
let areas = List.map (fun s -> s#area) l
I’m wondering if you really need classes for the object implementation – you’re not actually inheriting from them? When reading @kantian’s first class module version above I imagined the corresponding object oriented solution would define a class shape with virtual methods area and draw, inherited by point or rectangle methods.
You show that an object type can also be used for specifying the interface of point and rectangle.
How about this variation of your object implementation (Disclaimer: I have not actually used OCaml objects in real life, so this may contain obvious mistakes!)
module Surface = struct type t end
type shape = < area : int; draw : Surface.t -> unit >
module Point = struct
let make x y : shape = object
val x = x
val y = y
method area = ignore (x,y); 0
method draw surface = ()
end
end
module Rectangle = struct
let make lx ly ux uy : shape = object
val lx = lx val ly = ly val ux = ux val uy = uy
method area = (uy - ly) * (ux - lx)
method draw surface = ()
end
end
let areas = List.map (fun s -> s#area) [Point.make 1 2; Rectangle.make 1 2 3 4]
Maybe not, no. Force of habit. 
OCaml uses row polymorphism so you don’t need to use inheritance to implement an interface. If an object has the corresponding type it has the interface. Inheritance in OCaml is used only to inherit implementation and to enable open-recursion.
With that said, OCaml objects actually fit into ADT and are as well a detail of implementation that should ideally be hidden. My implementation above, could be using objects as existential, and this is what we were using before GADT (and even first class modules) came to OCaml. Today, GADT offer a much more efficient and syntactically convenient encoding.
Speaking of OCaml classes and class types, they also leak too much implementation and it is hard to use them in large programs. The only and very rare use case, when you might find classes useful is when you need an open recursion, e.g., when you would like to inherit implementation and override some of the base methods so that the other base methods would call to them. But this feature is rarely needed and is most confusing to support as it creates the tightest possible coupling between the components, which is hard to understand and debug.
To be honest, I must confess that I never read this book, I just skim over it. So, I decided to have a look at the chapter about first-class modules, and the solution I proposed is exactly what they did in this chapter : they just use the module type langage instead of the core type language to defined their notions.
So I can answer the previous @Chimrod question about documentation resources: chapter 10 of RWO about first-class modules.
RWO compare to my solution.
These two solutions are absolutely identical, all the types we use are isomorphic, we just not use the same language features to define them.
So let see on the above shape example. We start with this Shape algebra (a module type):
module type Shape = sig
type t
val area : t -> float
val draw : t -> unit
end
After that we use first-class modules to define the type class:
type 'a shape_methods = (module Shape with type t = 'a)
After that, I stick to the core language to define the rest of the types I need
type 'a shape_object = {meth : 'a shape_methods ; this : 'a}
type shape = Shape : 'a shape_object -> shape
What they did in RWO is that they stick to the module type language to define exactly the same notions:
module type Shape_object = sig
module Meth : Shape
val this : Meth.t
end
(* this way it's as if they have done as follow *)
type 'a shape_object_rwo = (module Shape_object with type Meth.t = 'a)
type shape_rwo = (module Shape_object)
And the build_instance function they define is exactly the family of type constructors that I named to_shape. That’s it : we’re doing exactly the same thing.
As @ivg said above : abstract types are existential types, so the type shape_rwo as I defined above is an existential type isomorphic to mine. The only difference is that for ergonomic reasons I prefer to stick to the core language as I’m not scared by existential GADT.
I have to admit I don’t really understand your widget implementation. What’s the benefit of the GADT here, compared to not using it? Especially in the context of polymorphism (List.map (fun s -> s.area) shapes).
GADT here work the same as non-PODT data structures in C++ or as classes in Java. They encapsulate a state and behavior in one object. E.g.,
type Widget = {
self : 'a;
draw : 'a -> Canvas.t -> unit;
}
It is a simple example that has only one method just as a showcase. Here are two more implementations of the Widget interface that are not using GADT
Using objects:
module Widget = struct
type t = < draw : Canvas.t -> unit >
let create draw self = object
method draw canvas = draw self canvas
end
let draw self canvas = self#draw canvas
end
as you can see, we eschew the underlying implementation type and capture the self value in the closure.
But nothing stops us from using plain records,
module Widget = struct
type t = {draw : Canvas.t -> unit}
let create draw self = {draw=draw self}
let draw {draw} canvas = draw canvas
end
well, in fact, since we have only function, why not just represent a widget as Canvas.t -> unit function,
module Widget = struct
type t = Canvas.t -> unit
let create draw self canvas = draw self canvas
let draw draw canvas = draw canvas
end
So now you might have a question why pick GADT even we have much simpler solutions? A good question, as indeed in our example all our methods were covariant, i.e., the were consuming widgets but not producing. But in general, we would like to have methods that are contravariant, i.e., that create widgets, or, invariant that consume and produce widgets. For example, suppose that we added a quite natural method called move (and also decided to encode our interface as a module type),
So here is our new Widget module type,
module Widget : sig
type t
module type S = sig
type t
val draw : t -> Canvas.t -> unit
val move : t -> Point.t -> t
end
val create : (module S with type t = 'a) -> 'a -> t
val draw : t -> Canvas.t -> unit
end
Notice that move is an invariant method it takes a widget and returns a widget. Now let’s solve this challenge using GADT,
module Widget = struct
module type S = sig
type t
val draw : t -> Canvas.t -> unit
val move : t -> Point.t -> t
end
type t = Widget : {
methods : (module S with type t = 'obj);
self : 'obj;
} -> t
let create methods self = Widget {self; methods}
let draw (Widget {methods=(module W); self}) canvas =
W.draw self canvas
let move (Widget {methods=(module W); self}) p = Widget {
self = W.move self p;
methods=(module W);
}
end
So far so good. But now let’s try to tackle it with objects, we define our abstract type as,
type t = <
draw : Canvas.t -> unit;
move : Point.t -> t;
>
and we fail even on the create function,
let rec create (module W : S) self = object
method draw canvas = W.draw self canvas
method move point =
create (module W) (W.move self point)
end
as it yields,
This expression has type 'a but an expression was expected of type W.t
The type constructor W.t would escape its scope
We can cope with this by using locally abstract data types and a recursive function,
let rec create : type o. (module S with type t = o) -> o -> t =
fun (type obj) (module W : S with type t = obj)
(self : obj) ->
object
method draw canvas = W.draw self canvas
method move point =
create (module W : S with type t = obj) (W.move self point)
end
But this looks unnecessary painful and also this recursion… it doesn’t look nice. And the further we go the more painful it will.
So the main feature of GADT is that (1) it enables us to easily implement t -> t transformations. Moreover, we can even recover the original type, when necessary. And even implement an abstract type without storing methods in its representation.
That is because the book was written in 2011-2013, and GADT landed in the language only in 2012. By that time first-class modules were the best way of implementing existential.
That’s why I always found that using objects to solve this design question has been one of the worst idea I’ve ever seen in the history of human thought. Since I’m a mathematician, this is not your widget example I have in mind, but a basic algebraic structure hierarchy, starting for instance with the notion of group:
module type Group = sig
type t
val zero : t
val add : t -> t -> t
val neg : t -> t
end
And when I said previously that the first book that illustrate this methodology was Book V of Eucid’s Elements, I refer to the work of Eudoxus of Cnidus that was perfectly described by Jean Dieudonné in this conference (p.14-15, sorry but it’s in french).
Sometimes I have the impression that programmers are reinvented the wheel, but make it square. And I’m still not convinced that a square is a perfect shape for a wheel.
It took me some times to find a response to this question that I hope will be suitable and intelligible.
TL; DR : the existential is the limit of the series of types you will define if you use the technique with extensible variants or polymorphic ones. Each time you add a new shape with one of this technique, you end up with a type which has a finite number of shape’s kind., and any of this finite sum type is a subtype of this existential. In others words, any kind of shape you will ever imagine already belongs to this existential sum type.
A little bit more explanation. Consider this module:
module M : sig
type t
int : int -> t
float : float -> t
end = struct
type t = Int of int | Float of float | String of string
let int i = Int i
let float j = Float j
end
The type int and float are subtypes of the type M.t, and the two functions int and float are the way we inject them in it. But for sure, there is non useful constructor String. Even if M.t is a common supertype of int and float, it is not the best one. Among all their common supertypes, the lowest one is their sum (up to isomorphism). With polymorphic variants, there is a built-in notion of subtyping, but it is very restricted: the only isomorphism it considers is the identity.
Now we have a notion of 'a shape_object, and we can define for instance a point shape_obejct, a circle shape_object and so on. Then comes this question: what is the lowest supertype of this infinity of shape_objects? Answer: the existential I define.
You can think of this existential as a variant with an infinity of constructors. And you can ask: where are this infinity of constructors? Answer: they are here:
to_shape : (module Shape with type t = 'a) -> 'a -> shape
Hence, the constructor for a point is to_shape (module Point), the one for a circle is to_shape (module Circle), and so on. No need for extensible variants or polymorphic ones to define this infinity of shape’s kind. To define a new shape’s kind you only need to implement a compilation unit that satisfies the Shape interface and apply the to_shape constructor.
When I wrote this
[to_shape (module Point) p1; to_shape (module Circle) r1]
it is conceptually similar to this one:
[(p1 :> shape); (r1 :> shape]
in order to define an homogeneous list of shapes.
I hope this time, it is clear to you what this existential really is.
While this might well all be true I think the question “What’s the benefit of the GADT here, compared to not using it?” was being asked in order to raise a practical issue. Instead of using a GADT to provide an existential type capturing the ‘self’ object, you can do what functional programmers have been doing for decades and have ‘self’ closed over by the function which operates on ‘self’. I think @ivg was suggesting that some issues might arise in a case of contravarience, but they seem unlikely to apply in the shapes issue posed by the OP.
They do, try to implement Widget.move or Widget.compare functions. Closures are good only when the type is not escaping it.
OK, that’s the OP’s answer: closures are only as good as the function closing over them. Thank you incidentally for your tour of the landscape. I enjoyed it.
Indeed, in the case of the OP there is no variance issue, but we don’t know how the system can evolve.
On the other hand, even if Golang uses this technique with its interface system, they never have variance issue as the type on which the method operates cannot appear in their type.
One caveat though on ADTs. You don’t need to expose them to the interface if you use standard (non-polymorphic ADTs) with casting functions along the lines of your ‘widget’ function. You do need to expose them in the interface if using polymorphic variants for sub-typing, but that doesn’t mean the user actually has to delve into them. If the interface is good enough the provided functions can often do that.
I think I have an answer to this : if you use object you will end up with a very poor type hierarchy with only one type. The problem is not the use of object as existential but to define a point (or any other shape) as an object even without variance issue.
Let see, what appends with first-class module type.
(* first-class modules and GADT *)
module type Shape = sig
type t
val area : t -> float
val draw : t -> unit
end
type 'a shape_methods = (module Shape with type t = 'a)
type 'a shape_object = {meth : 'a shape_methods ; this : 'a}
type shape = Shape : 'a shape_object -> shape
And now we define the notion of shape as class:
type shape_oop = < area : float ; draw : unit -> unit >
What I claim is that my shape type is a subtype of this shape_oop (it is not therefore the best, i.e the lowest, one we could concive). And more importantly, with this design this will be the only one we’ll have in our type hierarchy, which will cause problem as soon as we want to add new behavior or new shapes.
Proof of my claim: the type of this following function
let f (Shape shape) : shape_oop =
let module Meth = (val shape.meth) in
object
val this = shape.this
method area = Meth.area this
method draw () = Meth.draw this
end
;;
val f : shape -> shape_oop = <fun>
All very interesting, thank you. I suspect though that the OP’s question was more to do with “why use a GADT’s existentially quantified type to hold a ‘self’ object and a function to operate on it when other mechanisms, such as holding the ‘self’ object as a closure, can be used?” If so, that has now been answered.
On the more general point, in a case where you are more likely to want to add new shapes to existing behaviors rather than add new behaviors to existing shapes, I think I would adopt @ivg’s proposal for a ‘widget’ function which generates proxy objects. I think I would tweak it slightly to allow direct dispatch where the concrete type of the shape object is known to avoid the overhead of virtual dispatch, and reserve virtual dispatch via the proxy object for cases where the proxy object needs to be held in a container or passed to another function in order to obtain genericity.
If the problem area is more likely to add new behaviors to existing shapes, then I think I would probably use polymorphic variants.