CakeML / CakeML/cakeml

Add support for when-clauses in the front end.

Open
#663 0 comments 0 reactions 0 assignees View on GitHub
low priority
Dominant language
Standard ML
Stars
1.2k
Forks
104
Avg merge
2d 21h
Merged PRs (30d)
16

Description

When clauses are very useful for writing concise ML code.

Yet, it is very hard to give them a semantics. On the one hand, it is useful to allow the when clause to perform side effects (e.g. a union-find query that may compress a path). On the other hand, mutating the data being matched is generally unsafe in the presence of pattern matching optimization (cause of a famous OCaml segfault).

A simple solution is to view when clauses as a mere syntactic sugar. Along the lines of:
```
match v with
| p1 when e1 -> body1
| _other_clauses_
```
would compile down to
```
let k() = match v with _other_clauses_ in
match v with
| p1 -> if e1 then body1 else k()
| _ -> k()
```
This prevents optimizations of the pattern matching branch selection, but at least would be clear in terms of semantics. Compilation using gotos would save the need to allocate the closure k.

Contributor guide

No contributing guide indexed for this repository

Assessment

This issue has not been assessed yet.

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.