What is the "right" way to add constraints on a type, to handle recursive structures with variants and to combine fragments of types?

Learning
, ,
11

You’re asking too many questions :slight_smile: It is hard to address them all, so this may scare people away, my suggestion would be to split your question into several small and well-scoped questions.

Anyway, you are indeed using OCaml a little bit incorrectly because you’re confusing data and types. Records, tuples, and variants represent data, an algebra of data close under very few operations (basically union and set multiplication). If your field of knowledge could be encoded in terms of two this set operations, then you’re fine with algebraic data types.

For less simple cases, you need to start thinking differently and use different mechanisms. You shall invoke the Curry-Howard isomorphism and start thinking of types as of theorems. Where one type is a theorem, a collection of types (a signature) will become a theory. Once you’re in this paradigm it is quite easy to express your domain knowledge using types, e.g.,

module type System = sig 
  type human
  type company

  (* theorem: all humans have one name *)
  val name : human -> string

   (* theorem: all humans have and id card *)
   val name : human -> id

   (* all companies have a set of clients, possibly empty *)
   val clients : company -> human list
end

You can express complex relationships between different entities. You can employ subtyping by using type constructors, e.g.,


type 'a entity
type human
type company


(* all entities have an identity *)
val id : 'a entity -> id

(* a human with id is an entity *)
val human : id -> human entity

(* a company with id is an entity *)
val company : id -> company entity

Once you start to reason in signatures and writing your code on the module level you will uncover the whole power of OCaml. Remember: if you’re not using mli files, then you’re not programming OCaml.

Where a signature is a theory which is a set of theorems which can express many complex ideas, the module implementation, aka structure is a set of proofs. Constructive proofs. Since OCaml is not a theorem prover, but is more known as a programming language, it would be hard to force OCaml to verify all your proofs. Indeed, OCaml can try to verify some simple cases, as it knows some theories of algebraic data types, and GADT give enough power to prove stuff that in general requires dependent typing. You can even prove Russel Paradox in OCaml. But at the end of the day you will still find that some terms could not be verified by OCaml. For example, if we want to create a theory of nat1, i.e., natural strictly positive numbers, we can express it with a signature:

module type Nat1 = sig 
   type t

  (* nat1 is a subset of integers *)
  val of_int : int -> t option

  (* the set of nat1 is closed under addition *)
  val add : t -> t -> t

  (* but not under subtraction *)
  val sub : t -> t -> t option
end

Now, when we have to write the implementation it would be natural to use int as an underlying implementation. (You can of course use church numerals, and indeed prove the provided theorems, but it wouldn’t be practical or efficient). So the implementation would look like this:

module NatAsInt : Nat1 = struct 
   type t = int
   let of_int x = if x > 0 then Some x else None

   (* here the compiler does not have a proof that `x` and `y` are positive, 
       however, since the only valid way to obtain an instance of type t 
       _outside_ of our module is via `of_int` or `add`, and `sub` we can prove
      though not mechanically, that `x` and `y` are always positive here. *)
   let add x y = x + y

   (* the same is here, we know that they are positive as this is an invariant
      of the module *)
   let sub x y = if y >= x then None else Some (x - y)
end
9 Likes