Allow a let definition to introduce locally abstract types

[fpottier]

While working on Menhir's new back-end, which produces OCaml code that uses GADTs, it has come to my attention that there seems to be currently no good way of inlining a function that performs a case analysis on a GADT, while preserving well-typedness.

Suppose I have these type and function definitions:

type 'a foo =
  | F1 : int foo
  | F2 : bool foo

let f : type a . a foo -> a =
  fun foo ->
    match foo with F1 -> 0 | F2 -> true

let g () : int =
  f F1

Suppose I want to inline f into g. The following naive attempt is considered ill-typed:

let g () : int =
  let foo = F1 in
  match foo with F1 -> 0 | F2 -> true (* ill-typed *)

Florian Angeletti notes that I can write this, which is well-typed and is likely to be efficiently compiled (once types are erased,
it is an explicit beta-redex):

let g () : int =
  F1 |> begin fun (type a) (foo : a foo) -> (
  (match foo with F1 -> 0 | F2 -> true)
  : a) end

This is an interesting remark, but I would prefer a syntax that involves a let construct. Does the following proposed syntax make sense? The let construct introduces the local abstract type a in its right-hand side.

let g () : int =
  let (type a) (foo : a foo) = F1 in
  ((match foo with F1 -> 0 | F2 -> true) : a)

[trefis]

I don't know how to reconcile let g () : int with (... (... -> 0 | ... -> true) : a).
Can you explain?

[gasche]

The syntax that François suggests is consistent with the syntax for naming existential variables in GADT patterns introduced recently in #9584: | Dyn (type a) (w, x: a ty * a) -> .... The difference is that here you expect (edit: wrong, see below) the type-checker to learn the equation a = int when checking F1 : a foo, and use it in the right-hand-side, whereas the existential-in-patterns syntax expects (if I'm not mistaken) the type names to only be used for existentials that do not introduce any equation, so they appear as purely rigid in the right-hand-side.

I think that the feature request makes sense.

[fpottier]

In my mind, the type a is locally abstract in the right-hand side of the let construct, which is type-checked just like the function f in the original code. The type a becomes a normal type variable 'a in the left-hand side of the let construct, so 'a foo is unified with the type of F1, which is int foo, and the type-checker unifies 'a with int, as in the original code, when the function f is called.

[lthls]

I'm not competent to discuss the part about typing, but if you want to inline f you can use the [@local] attribute:

let g () : int =
  let[@local] f : type a . a foo -> a =
    fun foo ->
      match foo with F1 -> 0 | F2 -> true
  in
  f F1

This should ensure that the function is inlined by the compiler, but at a stage where types have been erased.

[fpottier]

In the setting of Menhir, we want to perform inlining ourselves (and not delegate it to the OCaml compiler) because it unlocks other optimizations that only Menhir can perform.

Besides, it seems desirable for a programming language to guarantee that a function can always be manually inlined.

[fpottier]

By the way, is [@local] documented? I have never seen it before.

[lthls]

By the way, is [@local] documented? I have never seen it before.

It's tersely documented in the section about built-in attributes (8.12.1 for the 4.11.1 manual)

[lpw25]

I think the feature and choice of syntax make sense. In principle it should be quite easy to implement using code that is very similar to the existing code for dealing with (type a). One aspect that is not immediately obvious to me is what to do for recursive let bindings.

[trefis]

Thanks, the explanation makes sense.

[gasche]

Besides, it seems desirable for a programming language to guarantee that a function can always be manually inlined.

Syntactic type-preservation is old school :-)

[fpottier]

One aspect that is not immediately obvious to me is what to do for recursive let bindings.

Indeed, the feature as proposed makes sense for non-recursive let bindings only. Good point.

[garrigue]

While I think that this feature makes sense, there are a few questions.
The simplest approach to implement this would be to make it syntactic sugar for the applicative version.
However, this limits it to single lets (is there a need to also handle let (type a) ... and ... in ... ?), and does not allow let-polymorphism.
Also, I'm not sure this is sufficient for what @fpottier has in mind, as this means that the construct would disappear either during parsing, or during typing, and that we rely on later phases to produce efficient code.
The other solution is to handle it natively in the let construct, but this seems to require much more work. There may even be concerns about principality (if we generalize the let, shouldn't generalized type variables be allowed to be instantiated with types containing a ?).
Another question is whether this is really the semantics we want for this syntax. It is clearly coherent with the fun (type a) form, but the scoping (visible in the pattern and the body of the let, but not in the definition) is not completely trivial.

[DemiMarie]

In the setting of Menhir, we want to perform inlining ourselves (and not delegate it to the OCaml compiler) because it unlocks other optimizations that only Menhir can perform.

What are these optimizations? Could you create a specialized version?

[fpottier]

There is work in progress on a new back-end for Menhir, with a new intermediate language where it is easier to perform optimizations such as delaying PUSH operations, canceling PUSH and POP operations, and so on.

At the moment, we are taking advantage of OCaml's let[@local] construct to tell the OCaml compiler that a function exists only for type-checking purposes.

[DemiMarie]

There is work in progress on a new back-end for Menhir, with a new intermediate language where it is easier to perform optimizations such as delaying PUSH operations, canceling PUSH and POP operations, and so on.

At the moment, we are taking advantage of OCaml's let[@local] construct to tell the OCaml compiler that a function exists only for type-checking purposes.

Can you work around this issue by using Obj.magic? Obviously, that’s a disgusting hack, but in generated code it should be safe enough.

[fpottier]

Sure, that's what Menhir has been doing for 15 years, but the point of the new project is to get rid of it (and to enable more aggressive optimizations at the same time).

[github-actions]

This issue has been open one year with no activity. Consequently, it is being marked with the "stale" label. What this means is that the issue will be automatically closed in 30 days unless more comments are added or the "stale" label is removed. Comments that provide new information on the issue are especially welcome: is it still reproducible? did it appear in other contexts? how critical is it? etc.

[DemiMarie]

Is let[@local] sufficient for Menhir’s optimizations @fpottier?

[fpottier]

Actually, we don't even use let[@local] any more. We are happy with vanilla OCaml (with GADTs).
I still think it would be nice to allow let bindings to introduce locally abstract types, but Menhir does not need this feature.

[DemiMarie]

Nice! What change did you make to avoid the problem?

[fpottier]

The main trick is to restrict inlining: 1- we never inline a function that matches on a GADT, and 2- we never inline a function into a function that matches on a GADT.

[DemiMarie]

Did that come at a performance cost?

[DemiMarie]

(compared to this feature or using Obj.magic)

[fpottier]

No, I don't think so.

[github-actions]

This issue has been open one year with no activity. Consequently, it is being marked with the "stale" label. What this means is that the issue will be automatically closed in 30 days unless more comments are added or the "stale" label is removed. Comments that provide new information on the issue are especially welcome: is it still reproducible? did it appear in other contexts? how critical is it? etc.