I have a set of Ocaml types to represent a syntax tree. There are types for the program, classes, methods, expressions etc. For example, a method is represented by a record type like this:
type method = { return:typeid; args:typeid list; body:expr }
It includes a return type, a type for each argument, and the body definition. I want to type check the syntax tree, and produce a new kind of tree that looks very much like the old one, except every expression has an explicit typeid (known only after type-checking) associated with it.
One option is to declare a parallel set of types:
type typed_expr = expr * typeid
type typed_method = { return:typeid; args:typeid list; body:typed_expr }
(* ... there are more types *)
The typed_method is necessary because the typed_expr is a different type. But I don't want to maintain two almost identical sets of types for an unchecked AST and a checked AST.
An alternative approach is to define expression as follows:
type expr = {...; typ:typeid option}
This enables me to use the same type definitions for both the input to the checker and the output. The difference is that I move lots of checks to the consumer code of the checked syntax tree. There is a contract here that the typ field will never be None in the type-checker output, and will always be None in the type-checker input.
Now, every time I used the typed tree, the only way to access the typ field's inner value is to first check if it is None (which it shouldn't be). This makes all later consumer code ugly because of the extra checks.
Neither of these approaches seems satisfying to me. How would you model this?
