Value specifications in structures

Git branch: valspecs

Outline

This is a project to allow value specifications to appear in structures. This supports a style of programming more similar to Haskell's:

val map : ('a -> 'b) -> 'a list -> 'b list
let map f = function
  [] -> []
| a :: rest -> f a :: map f rest

it would also allow more interesting recursive definitions:

val f: 'a -> 'a list
module M = struct
  let g x l = f x :: l
  let h x = [x] 
end
let f x = M.h x

These recursive definitions work similarly to recursive definitions of values: a value that has been declared but not defined can only be used in "statically constructive" positions (see OCaml manual).

If a value's definition references a value that has been declared and not yet defined, then that value is also considered undefined until the original value has been defined.

Note that a predeclared value must have exactly one definition in the module, so the following would produce an error:

val x : int
let x = 4
let x = 5 (* ERROR: x has a value specification and multiple definitions *)

Things to be done

Add value specifications to structures in the parser and parsetree

• Expertise: ★★☆☆☆
• Time: ★★☆☆☆
• Mantis: None
• Mentor: Leo
• Who is working on this: ???
• What needs to be done: Add value specifications to the syntax for structures. This will require adding a constructor for value specifications to the parsetree.

Add values specifications to the environment

• Expertise: ★★★☆☆
• Time: ★★★☆☆
• Mantis: None
• Mentor: Leo
• Who is working on this: ???
• What needs to be done: Value specifications need to be added to the environment so that subsequent definitions can be checked against them. They should be replaced in the environment by their definition.

Add undefined values to the environment

• Expertise: ★★★★☆

• Time: ★★★★☆

• Mantis: None

• Mentor: Leo

• Who is working on this: ???

• What needs to be done: As well as the value specifications, the undefined value should also be put in the environment so that it can be used as part of a recursive definition. Undefined values should be usable as long as they are used in a statically constructive position. Definitions that use an undefined value should also be marked as undefined.

  Note that the check for "statically constructive" for recursive values is currently done in bytecomp/translcore, and operates on lambda code, rather than in the type-checker. This is probably not the correct way to handle value specifications, so it will have to be re-written to operate on the typedtree.

  The current check is also a post-processing pass of the definitions. Ideally the type-checker would keep track of its current context, so that a use can be determined as statically constructive or not during normal type-checking.

Use new statically constructive test for recursive value definitions

• Expertise: ★★★★☆
• Time: ★★☆☆☆
• Mantis: None
• Mentor: Leo
• Who is working on this: ???
• What needs to be done: Since we will have to rewrite the "statically constructive" test to operate on the typedtree, we should also change the handling of recursive value definitions to use our new definition.