Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Check for the well-formedness of let rec earlier, before or at type checking #6738

Closed
vicuna opened this issue Dec 29, 2014 · 9 comments
Closed
Milestone

Comments

@vicuna
Copy link

vicuna commented Dec 29, 2014

Original bug ID: 6738
Reporter: oleg
Assigned to: @yallop
Status: resolved (set by @yallop on 2017-09-25T14:19:04Z)
Resolution: fixed
Priority: low
Severity: minor
Version: 4.02.1
Target version: 4.06.0 +dev/beta1/beta2/rc1
Category: typing
Tags: patch
Related to: #4989 #6939 #7215 #7231 #7429
Monitored by: @gasche @glondu

Bug description

There are two restrictions on let rec: patterns must be simple
variable patterns (either just 'var' or '_ as var') and the variable
bound by let rec must appear under lambda, lazy or constructor.
These conditions are checked very late (in bytecomp/transcore.ml),
after type checking. But these are syntactic conditions; in
particular, the first condition can be checked during the parsing.
Minimal suggestion: check the first condition at parsing and
the second at type checking. So, a code that type checks should
produce no further compilation errors. Extended suggestion: since
let rec patterns are so restricted (and since the processing of patterns
becomes more involved with the addition of GADTs), separate
Pexp_let/Texp_let into Pexp_let and Pexp_letrec (ditto for Texp).
Type checking will become more orthogonal since in type checking Pexp_letrec
we don't need to care about GADTs, the exhaustiveness check and
the type propagation from expression to patterns.

@vicuna
Copy link
Author

vicuna commented Dec 29, 2014

Comment author: @yallop

I have a patch in the works for this.

@vicuna
Copy link
Author

vicuna commented Jan 6, 2015

Comment author: @alainfrisch

Minimal suggestion: check the first condition at parsing and
the second at type checking.

I'm strongly against checking the first condition during parsing: it could be circumvented with -pp/-ppx. There is a general tendency towards asserting assumed invariants on Parsetree during type-checking to avoid such problems (e.g. checking that tuples don't have 0 or 1 elements). In this specific case, doing so would require to duplicate the checking logic. I don't see any disadvantage of doing both checks during type checking.

(The story would be different with the extended suggestion, since one could then enforce the invariant in the structure of the Parsetree.)

@vicuna
Copy link
Author

vicuna commented Jan 6, 2015

Comment author: @gasche

In my mind the recursive-value restriction is semantic, not syntactic, and in particular it might be extended with non-syntactic criteria in the future; for example, it would be fine to pass the not-yet-defined recursive values to a function call whose polymorphic type guarantees, by parametricity, that the values are not inspected.

@vicuna
Copy link
Author

vicuna commented Jan 6, 2015

Comment author: @yallop

I like the idea of a semantic restriction. Of course, we'd have to get rid of polymorphic equality first...

@vicuna
Copy link
Author

vicuna commented Jan 13, 2015

Comment author: oleg

I too like the idea of a semantic restriction on let rec bodies. There were a couple of times were I had to struggle with the let rec restriction and had to tie up the knot myself, using the explicit reference cell. Still I wonder if my case was rare to justify any complication of the compiler.

My motivation for this feature request is simple: request that the let rec check,
however it is performed, be performed at type checking time rather than after type-checking. If the code passed type-checking, it should be regarded as well-formed.

@vicuna
Copy link
Author

vicuna commented Jan 13, 2015

Comment author: @alainfrisch

FWIW, LexiFi has a local extension for lazy let (and lazy let rec). See the "Lazy let-bindings" on http://www.lexifi.com/blog/ocaml-extensions-lexifi-semi-implicit-laziness . This gives a simpler way to too the tie up the knot without reference cells, when you are convinced that the recursion is well-founded. This is especially useful e.g. for GUI programming, where it is typical to have mutual recursion between all the "widgets" and "callbacks" on the single panel (but widgets are built in a bottom-up way, and callbacks are only applied after all widgets are built, so the recursion is actually well-formed). But I don't think it's possible to let the compiler ensure that this won't produce runtime error without adding significant machinery to the type system (one'd need to keep track on the fact that callbacks are not called too early, and this should be reflected in the type of functions that build widgets).

All in all, I'm not sure that a more semantic restriction is realistic/worthwhile: any sound system is likely to exclude most interesting cases anyway.

@vicuna
Copy link
Author

vicuna commented Jan 13, 2015

Comment author: @gasche

Sorry for being unclear: I was not asking for "semantic" extensions of the criterion to be made today, but rather just pointing out that this was a restriction that should be made and understood at the static-checking time (in the type-checker) rather than a syntactic restriction on the form of programs.

@vicuna
Copy link
Author

vicuna commented Jan 2, 2017

Comment author: @yallop

The patch is here, along with a fair amount of discussion:

#556

@vicuna
Copy link
Author

vicuna commented Sep 25, 2017

Comment author: @yallop

The patch is now merged; in the forthcoming 4.06 release the well-formedness of 'let rec' bindings is checked during type-checking, not in Translcore.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

1 participant