From 925256e30380d55f963d5835337e17ae073bbf29 Mon Sep 17 00:00:00 2001 From: Richard Eisenberg Date: Fri, 9 May 2025 08:51:47 -0400 Subject: [PATCH] Definitive kind annotations documentation --- jane/doc/extensions/_05-kinds/syntax.md | 133 +++++++++--------------- 1 file changed, 50 insertions(+), 83 deletions(-) diff --git a/jane/doc/extensions/_05-kinds/syntax.md b/jane/doc/extensions/_05-kinds/syntax.md index 338aa75f37e..00b34d7d658 100644 --- a/jane/doc/extensions/_05-kinds/syntax.md +++ b/jane/doc/extensions/_05-kinds/syntax.md @@ -198,10 +198,11 @@ type. **Summary:** Type parameters without annotations are assumed to have a layout other than `any` and assumed to be `non_null`; beyond that, inference chooses -the best possible kind. You can use a kind annotation to make a type parameter -of layout `any` or with `maybe_null`, but inference is still performed. +the best possible kind. If a type parameter is written with a kind annotation +(at its definition site or any occurrence), that kind sets the kind of the type +parameter; no further inference is performed. -**Details:** We use inference to determine the kind of a type parameter. +**Details:** We generally use inference to determine the kind of a type parameter. The best kind for a type parameter is the highest in the subkinding lattice: this allows for a type @@ -243,12 +244,37 @@ inclusion) would not be safe: it would allow us to smuggle, say, a `float64` type where only `value`s are expected. Accordingly, all type parameters are assumed to have a layout other than `any` -and also bounded by `non_null` -- unless you write a kind annotation saying -otherwise (like `type ('a : any) array`). However, even if you write a kind -annotation, we still perform inference. For example, if you write `type ('a : -any) t = K of 'a t_port`, then we'll infer `'a : value mod portable`. The -annotation is not ignored, but instead causes the initial assumed kind of `'a` -to be `any`, allowing that kind to be lowered by usages of `'a`. +and are also bounded by `non_null` -- unless you write a kind annotation saying +otherwise (like `type ('a : any) array`). + +If you write a kind annotation, that kind is definitive. For example, we may +write + +```ocaml +type ('a : any) my_array = 'a array +(* or, equivalently *) +type 'a my_array = ('a : any) array +``` + +and the type parameter to `my_array` will be allowed to range over all kinds. +In the case where there is a kind annotation, we do not perform further inference; +this will sometimes lead to rejecting programs that we could otherwise infer. +For example: + +```ocaml +type ('a : immediate) requires_immediate +type 'b t1 = 'b requires_immediate +type ('c : value) t2 = 'c requires_immediate +type 'd t3 = ('d : value) requires_immediate +``` + +Type `requires_immediate` is there just to set up the example; it is accepted. +Type `t1` is also accepted: there is no kind annotation, and so we infer +`'b : immediate`. However, `t2` and `t3` are both rejected: the kind annotation +`: value` sets the definitive kind for `'c` and `'d` respectively, and so +we do not then infer these kinds to be `immediate`, as required. (A kind +annotation on one variable does not affect our ability to do inference on other +variables.) If type inference ends and we still do not know what layout should be used for the parameter (this can happen only without an annotation), we infer the @@ -320,11 +346,21 @@ to change the kind. A unifiable type variable has its kind inferred based on how it is used, inferring the topmost kind consistent with its usage, with some exceptions: -* In a `val` or `external` declaration, we infer a layout other than `any`, and -we infer only kinds with `mod non_null`. To avoid these restrictions, use a -rigid type variable (with an explicit binding) instead. This exception is to -allow, for example, `val id : 'a -> 'a` to infer `'a : value`, necessary for -backward compatibility. +* In `val` and `external` declarations: + + * We infer a layout other than `any`, and we infer only kinds with `mod + non_null`. This exception is to allow, for example, `val id : 'a -> 'a` to + infer `'a : value`, necessary for backward compatibility. + + * If a variable appears in a kind annotation, it is as if the variable were + bound rigidly, before a `.`. This means that cases like `val f : ('a : + value) -> (string as 'a)` will be rejected, because of the kind + annotation. On the other hand, this extra rule allows us to write `val + id_or_null : ('a : value_or_null) -> 'a` and keep `'a` with kind + `value_or_null`: without this rule, the "always infer `mod non_null`" rule + just above would apply, and this declaration for `id_or_null` would be + interpreted identically to `val id_or_null : ('a : value). 'a -> 'a`, which + is likely not what the user wants. * In a `class` or `class type` declaration, all type variables have kind `value`. @@ -334,75 +370,6 @@ the definition, in usage sites of the bound variable. This is similar to the way the value restriction works via weak polymorphism. The bounds are _not_ determined afterwards. -## Examples around rigid vs unification variables - -For an abstract type declaration -like `type t : value mod portable`, the kind annotation will be used as the -exact kind of the type `t`. - -However, for a type declaration that describes what the type is (that is, has at -least one `=`), the kind annotation is just a check. For example, consider this -type declaration: - -```ocaml -type t : value = (int -> int) option -``` - -This declaration is allowed because `(int -> int) option` does have the kind -`value` (due to subkinding). But the type system treats `t` and `(int -> int) -option` as completely equal types, and therefore still knows the more precise -kind `value mod contended immutable non_float non_null` for `t` despite the -annotation. - -On the other hand, the following declaration is rejected because the kind of -`(int -> int) option` is not less than or equal to `value mod portable`: - -```ocaml -type t : value mod portable = (int -> int) option -``` - -There is a similar subtlety around unifiable type variables in `val` -declarations. Consider - -```ocaml -val id : 'a -> 'a -``` - -The type checker assumes a default of `'a : value` here. If you want to change -that, you should write - -```ocaml -val id : ('a : any). 'a -> 'a -``` - -Here, we have annotated the binding site of `'a` to say that it should have kind -`any`. (The type `('a : any). 'a -> 'a` is a perfectly good type, and a -function of that type can be called on values of any type of any kind. However, -you will be unable to define a function of that type, because the compiler will -not know what register will hold the argument.) In contrast, writing - -```ocaml -val id : ('a : any) -> 'a -``` - -does not do what you might think: it constrains a *usage site* of `'a`, stating -that `'a` must have a subkind of `any` -- but of course `value` *is* a subkind -of `any`, so the default behavior of choosing `value` is unaffected. That is, -the type `('a : any) -> 'a` is the same as just writing `'a -> 'a`. - -Contrast further with - -```ocaml -val id : ('a : float64) -> 'a -``` - -Here, we'll choose `'a` to have kind `float64`. This annotation works because -`float64` is not a superkind of `value`; the default kind does not apply. - -The bottom line here: if you want to set the kind of a type variable, do it at a -binding site like `val f : ('a : <>). ...` or `let f : ('a : -<>). ...`. - ## Syntax reference In this reference, we use backticks to denote a literal keyword,