Mathematical Platonists think that 3, √(−1) and the set of real numbers are real things that exist. They imagine a Platonic universe that holds these things and many more. They can thus comfortably say that there exists an x such that x2 = −1. I am not a mathematical Platonist, yet I have no other way to talk about mathematics. I think and talk as a Platonist.

I find the OCaml manual excellent at guiding me, by example, to solving familiar programming problems but I am left with no fundamental conceptual tools with which to mentally explore the limits of what OCaml can do. When I read about Phantom Types for OCaml I realized that I had not learned enough from the OCaml manual to have invented such mechanism. In retrospect I can still not find the necessary information in the manual.

The Algol 68 manual, for all its faults, gives a platonic description of a program and its state of execution. Values of expressions are always some point in this Platonic space. There are crisp and accessible notions such as ‘Every value is of exactly one type.’. This is not true of all languages and I have not been able to figure out if it is true of OCaml. Each Algol 68 type or value is a point in the Platonic space of Algol68, approximately as real as π. There are, I suspect, perhaps a dozen other clouds in my view of OCaml. All the questions that have occurred to me can be answered by writing small programs for the Inria OCaml system. The problems lie in the questions that have not occurred to me. I do not greatly fear writing wrong things here; having a wrong idea is better than having no idea. Perhaps someone will correct me. I plan to seek empirical corroboration for my ontology.

In Algol 68 “INT” designates the type integer, just as “4”, “2+2” both designate 4. Henceforth I write as a Platonist! (second thoughts)

Platonic OCaml

Here is a list of top level categories so far So far these categories are disjoint. Programmer chosen identifiers can designate specific members of these categories. Section 6.3 of the manual list the categories of things which identifiers can identify. They forgot type parameters that occur in definitions of modules.

The provided REPL responds "- : bool = false" to "false" which suggests that values are of exactly one type. Thus viewed as sets of values, types are disjoint—they partition the set of values. 

specification ::= type-definition
definition ::= type-definition
Koans: 
type q1 = A | N | B and q2 = U | N | E5;;
Warning 30: the constructor N is defined in both types q1 and q2.
The Platonic stuff is fun and it might be important but I think the first level confusions are about scope of identifiers and the closely related questions of which ID occurrences are defining and which are applied. In “let e = 4 in e+1” the first “e” is defining and 2nd is applied. I will write this “let e = 4 in e+1”. It would be natural to include this information in the BNF.

I gather that OCaml ‘records’ and ‘variant values’ are roughly and respectively like C’s ‘structs’ and ‘unions’. Like C and unlike other OCaml types, records and variant values cannot arise in an OCaml program except in the scope of a type declaration which provides the field names for the constituent records or variant types. Some differences between OCaml and C:

The C expression A = “struct {int a; float b;}” establishes an identifier “a” whose ‘scope’ is unlike those above. We call these latter scopes “scattered” here by contrast with the “contiguous” scopes established by “int a;”. The expression A makes the expression B = “x.a” valid depending indirectly on other occurrences of “x”, but B and those other occurrences must be in the scope of A. 

{struct {int a; float b;} x; x.a;}

With scope shadowing, contiguous scopes can have holes consisting of a subtree where a scope is interrupted by the scope of another identifier spelled the same.

C++ has yet other sorts of scopes.

Best I can tell OCaml has just the contiguous and scattered scopes.

We need an index of syntactic categories!

Exploring an interest presentation of syntax