let rec f : type t u . t -> u = fun (x : t) : u -> f x
Dear all, why the t in the expression (x : t) is in scope? I thought t was only available in
the type annotations, thanks! – Hongbo
2 Likes
Hi,
according to the documentation on locally abstract types, their scope is the whole sub-expression.
It can then be used wherever a type is expected but where a type variable (what you would have otherwise) is not correct or does not have the same meaning :
- type annotations (as in your example) or in lets or patterns
- type expression local modules
- local exception definitions
- (maybe other places).
The manual shows examples of such cases.
1 Like
A point to keep in mind is that the syntax
let rec f: type t u. t -> u = fun (x:t) : u -> f x
is desugared to:
let rec f: 't 'u. 't -> 'u = fun (type t u) -> fun (x:t) : u -> f x
In other words, the locally abstract types are not introduced inside the type annotation and their scope is the whole body of the let definition.
4 Likes
Thanks @octachron , that explains the issue.
I tried to play it a bit further:
let rec f = fun (type t u) (x : t) : u -> f (x)
Hope it would give me a type val f : 't -> 'u but ends up a typing error:
This expression has type t but an expression was expected of type 'a The type constructor t would escape its scope
It is not obvious to me that t would escape. I know the solution or work around but would be nice to understand what’s the scope of t and why it escaped here?
I was hoping it would behavior as below (with type t, u erased after checking):
type t
type u
let rec f = fun (x : t) : u -> f x
Thanks
I am not sure which workaround you have in mind? The usual workaround makes it pretty explicit that
the issue is that the type t and u are introduced after f:
let f (type t u) =
let rec f (x:t): u = f x in
f
In term of scope, your initial code is equivalent to:
let cell = ref None
let store x = cell := Some x
let () =
let module M = struct type t = A end in
store M.A
which more obviously problematic.
Note that the syntax type t u . t -> u is useful for polymorphic recursion, and that an unannotated let rec f = ... cannot be used polymorphically inside its own definition. If you want polymorphic recursion you need either let rec f : type t u . t -> u = ... or let rec f : 't 'u. 't -> 'u = .... (The type t u form is useful when you want to mention the polymorphic types inside the program, and necessary for some uses of GADTs or local modules.)
@bobzhang I don’t understand what your question is and what you are trying to do/achieve. (Can you explain the context for your questions?) The first post was about an admittedly non-intuitive scoping aspect of an advanced OCaml feature: this is a good question and it deserves an explanation. But then what is your followup question?
hi @gasche , thanks for the follow up, my second question is that
let f (type t u) =
let rec f (x:t): u = f x in
f
I want to express local abstract type exclusively in this style, but it seems there is no
intuitive syntax for this, ideally let rec f = fun (type t u) (x : t) : u -> f (x) would work this way, but it does not, I guess the type checker treat the fun (type t u) : u -> f (x) as a whole without taking into let rec into consideration, is that the case? thanks – Hongbo
No, currently we don’t easily support this, due to the interaction betweeen locally abstract types and polymorphic recursion. This should work for non-recursive functions, I think.
We may be able to infer a bit more about polymorphic recursion to support your example. I will think more about it and possibly open an upstream feature request.
I want to express local abstract type exclusively in this style
Would you mind explaining why? Is it just personal stylistic preference, or is there another reason?
After thinking more about this, I don’t know of a good way to extend the current rule. The problem is that trying to infer a polymorphic type scheme works in some very limited cases but quickly fails. Consider for example
let rec iter n f x =
if n = 0 then x
else iter (n - 1) f (f x)
I can propose a heuristic/alogrithm that would handle gracefully this case
let rec iter n (type a) (f : a -> a) (x : a) : a = ...
but it would fail if any of the three annotations (on f, x and the return type) was missing
let rec iter n (type a) (f : a -> a) (x : a) = ... (* fail *)
let rec iter n (type a) (f : a -> a) x : a = ... (* fail *)
let rec iter n (type a) f (x : a) : a = ... (* fail *)
It seems very fragile to put this kind of inference in place, that breaks on the slighest change.
Currently, users have to be taught that to combine (type a) with recursive function, they have to use a polymorphic recursion annotation:
let rec iter : type a . _ -> (a -> a) -> a -> a = ...
there is a simple rule: all the parts of the final type that mention a have to be annotated – the others can be left inferred by using _. I find this rule intuitive on the type annotation (notice in particular that we had to think about the return type of the function, not just the type of the arguments), whereas it seems arbitrary and unintuitive in the “inferred” versions above where users did not write the annotation.
Personally the syntax that I would prefer is to allow val declarations before let to carry the annotations:
val iter : 'a. int -> ('a -> 'a) -> 'a -> 'a
let rec iter n f x = ...
('a. would behave as type a. also for GADTs.)
I think that this approach is nicer than the current syntax, and more robust than trying to infer the annotation from the unannotated declaration.
1 Like
val outside of mli files would be so nice! My current style for polyrec is let rec with the types on one line, then fun with the values, unindented, on the following line.
I believe F* has some form of this floating signatures feature.
there is a simple rule: all the parts of the final type that mention
ahave to be annotated – the others can be left inferred by using_.
Is this documented ?
Personally the syntax that I would prefer is to allow
valdeclarations beforeletto carry the annotations:
I like this too. I wonder for the current implementation, if the toplevel is fully annotated, is this information used for checking directly, or we still do the type inferrence and check if the two types are consistent? I would prefer the former to use the type annotation to guide the type checking.