Skip to content

Commit 4f4d77e

Browse files
committed
revised RFC based on discussions at the type-system meeting
1 parent 308ebe9 commit 4f4d77e

File tree

1 file changed

+138
-0
lines changed

1 file changed

+138
-0
lines changed

rfcs/val_annotations.md

Lines changed: 138 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,138 @@
1+
# `val` declarations in structures
2+
3+
## Context
4+
5+
Advanced OCaml features often require writing type
6+
annotations. However, writing type annotations on definitions today
7+
can be awkward, as it forces to write the rest of the definition in
8+
a different style than we would normally use: adding an annotation on
9+
a function definition
10+
11+
```ocaml
12+
let f arg1 arg2 arg3 =
13+
<body>
14+
```
15+
16+
typically requires adding the annotation after `f`, in the form `:
17+
<type> =` and then adding a `fun`, and then turning the trailing equal
18+
sign into a right-arrow (and making an awkward decision on
19+
indentation):
20+
21+
```ocaml
22+
let f : <type> =
23+
fun arg1 arg2 arg3 ->
24+
<body> (* extra indentation *)
25+
26+
(* or possibly *)
27+
let f : <type>
28+
= fun arg1 arg2 arg3 ->
29+
<body>
30+
```
31+
32+
(Note: we are not talking about per-argument annotations here. They can
33+
be simpler in some cases, but they cannot be used in others, for
34+
example when introducing polymorphic recursion due to GADTs. Generally
35+
their readability is worse than full-declaration annotations in
36+
complex cases.)
37+
38+
39+
## Proposal
40+
41+
We propose to allow using `val` declarations immediately before definitions.
42+
43+
```ocaml
44+
val map : ('a -> 'b) -> 'a list -> 'b list
45+
let rec map f li = ...
46+
```
47+
48+
### Recursive bindings
49+
50+
In a nest of mutually-recursive bindings, each binding may or may not
51+
have a declaration, but the declarations must all come together before
52+
the `let rec` block.
53+
54+
```ocaml
55+
val even : int -> bool
56+
val odd : int -> bool
57+
let rec even n = ...
58+
and odd n = ...
59+
```
60+
61+
(It is not allowed to mix declarations and definitions, because there
62+
is no obvious syntax for this, although `and val` could be
63+
considered. See "Alternative syntax: declarations with `let` blocks"
64+
below for a form that allows this.)
65+
66+
### Local bindings
67+
68+
The `let <structure item> in <expr>` form of
69+
[#14040](https://github.com/ocaml/ocaml/pull/14040) is extended to
70+
cover local declarations:
71+
72+
```ocaml
73+
let rev li =
74+
let val loop : 'a list -> 'a list -> 'a list in
75+
let rec loop li acc = ... in
76+
loop li []
77+
```
78+
79+
## Discussion and extensions
80+
81+
### Locally abstract types in `val` declarations
82+
83+
We propose to extend the form `type a . ...` to work with value
84+
annotations. For example:
85+
86+
```ocaml
87+
let val mem : type a . a -> a list -> bool
88+
and mem elt li =
89+
let rec loop : a list -> bool = function
90+
| [] -> false
91+
| x :: xs -> (x = elt) || loop xs
92+
in loop li
93+
```
94+
95+
Notice that `type a` binds the variable `a` in both the declaration and the definition.
96+
97+
(This extension could be left out of a first implementation of this proposal.)
98+
99+
100+
### Alternative syntax: declarations within `let` blocks
101+
102+
An alternative syntax would be possible where `val` is part of the `let` block, as follows:
103+
104+
```ocaml
105+
let rec
106+
val map : ('a -> 'b) -> 'a list -> 'b list
107+
and map f li = ...
108+
```
109+
110+
This syntax is weirder (it feels closer to SML), but it scales
111+
slightly better to mutually-recursive or local definitions:
112+
113+
```ocaml
114+
let rec val f : <type>
115+
and val g : <type>
116+
and f <def>
117+
and g <def>
118+
and val h : <type>
119+
and h <def>
120+
and i <def>
121+
```
122+
123+
```ocaml
124+
let rev li =
125+
let rec
126+
val loop : 'a list -> 'a list -> 'a list
127+
and loop li acc = ...
128+
in loop li []
129+
```
130+
131+
### Combination with `_` inference from signature
132+
133+
oxcaml has a work-in-progress feature where `_` can be used to elide types and module signatures in structures (in particular `.ml` files), when they are declared in the corresponding signature (in particular the `.mli` file), see https://github.com/oxcaml/oxcaml/pull/2783 . This feature is independent, but it was part of the motivation to revive the current proposal, as it can naturally be combined:
134+
135+
```ocaml
136+
val map : _
137+
let rec map f li = ...
138+
```

0 commit comments

Comments
 (0)