Experimental OCaml

We can find tentative answers to many of the questions raised here by experiment with the OCaml REPL (read-eval-print-loop) program. We begin with the code of the tutorial:

module type MonadRequirements = sig
    type 'a t
    val bind : 'a t -> ('a -> 'b t) -> 'b t
    val return : 'a -> 'a t
end;;

and:

module OptionMonad = struct
    type 'a t = 'a option;;

    let bind opt f =
        match opt with
            | Some(x) -> f x
            | None -> None;;

    let return x = Some x;;
end;;

and the confluence:

module Aa = (OptionMonad : MonadRequirements);;

Many of the questions whose answers I have not found in the manual can be answered by simple REPL queries. Unlike most REPls, OCaml reports the type of a value that it prints. It also recapitulates the meaning of a command declaring a type such as “type 'a t;;”. I shall postulate that when the recapitulations are the same then the meanings of the commands are the same.

Postulate: The meaning of the definition of MonadRequirements is invariant under systematic substitutions of the type parameters, within one line of the text. Thus

module type MonadRequirements = sig
    type 'sr t
    val bind : 'awe t -> ('awe -> 'zz t) -> 'zz t
    val return : 'rt -> 'rt t
end;;

yields the same as the original MonadRequirements which is:

module type MonadRequirements =
  sig
    type 'a t
    val bind : 'a t -> ('a -> 'b t) -> 'b t
    val return : 'a -> 'a t
  end

It remains to be seen what syntactic categories one can make such systematic substitutions. The number of type parameters to a type constructor must be the same thru out the sig … end construct.

The typeconstr-name “t” is becomes part of the value of MonadRequirements. OptionMonad must use the same identifier for the confluence to work.

“type 'y t = 'z list;;” produces a complaint about the undefined type paraneter: “'z”. It would seem that the “'y” in “type 'y t” establishes a scope for “'y” in any type-information in the same typedef.

The BNF produces “type r = A of int” thus allowing “A 56” to which REPL responds “- : r = A 56”.

type 'a optioN = None | Some of 'a;;
None;;
Some 25;;

It works!

The following takes some explaining. It evidently has to do with type inference.

# let a = ref None in (a := (Some 3.4); a := (Some 3.3); !a);;
let a = ref None in (a := (Some 3.4); a := (Some 3.3); !a);;
# let a = ref None in (a := (Some 3.4); a := (Some 3); !a);;
Error: This expression has type int but an expression was expected of type float
# let a = ref None in if 1<0 then a := (Some 3.4) else a := (Some 3); !a;;
Error: This expression has type int but an expression was expected of type float
# if 1<0 then Some 3.5 else None;;
- : float option = None

It is curious that these two definitions seem to produce different types:

# type w = N of int * float;;
type w = N of int * float
# type w1 = N1 of (int * float);;
type w1 = N1 of (int * float)