From 46a636563f1ade9c838ea98c27a895ff0a4a3466 Mon Sep 17 00:00:00 2001 From: Samuel VIVIEN Date: Wed, 5 Jun 2024 16:58:35 +0200 Subject: [PATCH 1/7] First draft --- rfcs/type_arguments_for_modules.md | 71 ++++++++++++++++++++++++++++++ 1 file changed, 71 insertions(+) create mode 100644 rfcs/type_arguments_for_modules.md diff --git a/rfcs/type_arguments_for_modules.md b/rfcs/type_arguments_for_modules.md new file mode 100644 index 0000000..9591142 --- /dev/null +++ b/rfcs/type_arguments_for_modules.md @@ -0,0 +1,71 @@ + +# Type arguments for modules + +This RFC proposes to extend a bit the module language by adding the possibility +of giving types arguments to modules. + +The goal of this feature is to simplify replace cases where the user might want +to have a module containing only a single type by directly writing the type. +In those cases we currently force the user to define a module containing that +type. + +## Proof of concept + +A first draft of this feature is implemented at +https://github.com/samsa1/ocaml/tree/module_type_arg . + +It features types as arguments in modules expression and type paths +as arguments in modules paths. + +## Proposed change + +The idea is to extend the syntax of the module language with a new argument to +functors : + +```ocaml +module M (type a) = ... + +module M2 = functor (type a) -> ... +module type S = functor (type a) -> ... +``` + +and a new construction for applications. + +```ocaml +module M3 = M(type [`A | `B]) + +let f (x : M(type int).t) = x +``` + + +## Important restraints + +This feature needs some restraints in order to be sound. + +### Applicativity of type functors + +A functor that takes a type as argument should behave as an applicative functor. + +In other words, the following code should type-check + +```ocaml +type t1 = M(type int).t +type t2 = M(type int).t + +let f (x : t1) = (x : t2) +``` + +### Paths in paths + +Only type paths should be authorized when doing an application inside +a type path. + +In other words, `M(type ).t` should be rejected. + +## Possible extensions + +This feature could be extended with other similar patterns to be a bit more expressive. + +- Implement the same feature with module types, +- Allow using parametric types in paths (for example `int list`). + From 3dc00bf8195603b9139046bc21621d59eff8bff1 Mon Sep 17 00:00:00 2001 From: Samuel VIVIEN Date: Wed, 5 Jun 2024 17:17:08 +0200 Subject: [PATCH 2/7] Added comment about preserving argument all the way to runtime --- rfcs/type_arguments_for_modules.md | 21 ++++++++++++++++++++- 1 file changed, 20 insertions(+), 1 deletion(-) diff --git a/rfcs/type_arguments_for_modules.md b/rfcs/type_arguments_for_modules.md index 9591142..96f816f 100644 --- a/rfcs/type_arguments_for_modules.md +++ b/rfcs/type_arguments_for_modules.md @@ -62,10 +62,29 @@ a type path. In other words, `M(type ).t` should be rejected. +### Type application must be compiled as an empty structure + +If we could avoid giving the type arguments at runtime for modules like with +functions we would have soundness issues. + +The following example show why it is important to preserve the information of +application all the way to binary code. + +```ocaml +module F (type a) = struct + let r : a option ref = ref None +end + +let r1 = let module M = F(type int) in M.r +let r2 = let module M = F(type float) in M.r +``` + +If `F(type _)` does not launch any computation then `r1` and `r2` will be the +same reference but with incompatible types. + ## Possible extensions This feature could be extended with other similar patterns to be a bit more expressive. - Implement the same feature with module types, - Allow using parametric types in paths (for example `int list`). - From 19c7e41d9bd69b99e3432a9c2f0108995bee9596 Mon Sep 17 00:00:00 2001 From: Samuel VIVIEN Date: Thu, 6 Jun 2024 11:40:57 +0200 Subject: [PATCH 3/7] Updated with first round of comments --- rfcs/type_arguments_for_modules.md | 145 ++++++++++++++++++++++++++--- 1 file changed, 134 insertions(+), 11 deletions(-) diff --git a/rfcs/type_arguments_for_modules.md b/rfcs/type_arguments_for_modules.md index 96f816f..751adc6 100644 --- a/rfcs/type_arguments_for_modules.md +++ b/rfcs/type_arguments_for_modules.md @@ -4,18 +4,106 @@ This RFC proposes to extend a bit the module language by adding the possibility of giving types arguments to modules. -The goal of this feature is to simplify replace cases where the user might want +The goal of this feature is to simplify cases where the user might want to have a module containing only a single type by directly writing the type. In those cases we currently force the user to define a module containing that type. -## Proof of concept +## Use cases -A first draft of this feature is implemented at -https://github.com/samsa1/ocaml/tree/module_type_arg . +The motivation for this feature came from people working on modular explicits +and modular implicits. However, this feature will also benefit OCaml even +without modular implicits. -It features types as arguments in modules expression and type paths -as arguments in modules paths. +### Modular explicits/implicits + +This feature becomes very important when taking into account modular explicits +and [modular implicits](https://arxiv.org/pdf/1512.01895). Because interactions +between the code language and the module language becomes much more frequent. + +In the case of modular implicits, a signature is given in order to search for a +compatible module. However, basic types are not compatible with parametrized +types. + +Thus, the module following module : + +```ocaml +module AddList = struct + type 'a t = 'a list + let add = List.concat +end +``` + +does not match the signature of addition. + +```ocaml +module type Add = sig + type t + val add : t -> t -> t +end +``` + +A way to fix this is to add a type argument to the `AddList` module. + +```ocaml +module AddList (A : Any) = struct + type t = A.t list + let add : t -> t -> t = List.concat +``` + +However, this becomes problematic with modular implicits because you need to +define a sufficient amount of modules to access any possible types. This lead +Patrick Reader and Daniel Vlasits to write a whole file of modules containing +only a type field : +https://github.com/modular-implicits/imp/blob/master/lib/any.mli. + + + +### Use cases in current OCaml + +Is some cases a parametric module requires as argument a type without any +structure attached to it. This is useful when we just want to store the type +but never look into it. Cases where this pattern occurs exists in the OCaml code +base. + + +#### State monad in algebraic effects tutorial + +For example when implementing a state monad such as the +one in the example available at : +https://github.com/ocaml-multicore/ocaml-effects-tutorial/blob/998376931b7fdaed5d54cb96b39b301b993ba995/sources/state2.ml#L13-L40. + +```ocaml +module type STATE = sig + type t + val put : t -> unit + val get : unit -> t + val history : unit -> t list + val run : (unit -> unit) -> init:t -> unit +end + +module State (S : sig type t end) : STATE with type t = S.t = struct + + type t = S.t + + type _ Effect.t += Get : t Effect.t + + let get () = perform Get + + let put v = failwith "not implemented" + + let history () = failwith "not implemented" + + let run f ~init = failwith "not implemented" +end +``` + +#### In ocamlgraph + +Another example of usage that feature in the OCaml would be in +[ocamlgraph](https://github.com/backtracking/ocamlgraph). Where some parametric +modules such as `Imperative.Graph.AbstractLabeled` requires a module containing +a single type as argument (here the types for vertex labels). ## Proposed change @@ -37,8 +125,36 @@ module M3 = M(type [`A | `B]) let f (x : M(type int).t) = x ``` +## Proof of concept -## Important restraints +A first draft of this feature is implemented at +https://github.com/samsa1/ocaml/tree/module_type_arg . + +It features types as arguments in modules expression and type paths +as arguments in modules paths. + +## Semantic change + +This feature does not change the semantic, it is just adds conciseness. + +The reason behind this is that all module expression using type arguments could +be rewritten to a module expression using a module wrapping the type. + +For example : + +```ocaml +1: module F (type a) = BODY [a] +2: F (type p) +``` + +could be encoded as the following. + +```ocaml +1: module F (A : Type) = BODY [A.t] +2: F (struct type t = p end) +``` + +## Important restrictions This feature needs some restraints in order to be sound. @@ -55,12 +171,17 @@ type t2 = M(type int).t let f (x : t1) = (x : t2) ``` +This also mean that when defining a type-functor `functor (type a) -> ME1`, +the same restrictions on `ME1` apply than on `ME2` in `functor (M : S) -> ME2`. + ### Paths in paths -Only type paths should be authorized when doing an application inside -a type path. +Only [type constructors](https://ocaml.org/manual/5.2/names.html#typeconstr) +should be authorized inside a module path. The reason for this restriction is +that adding too much complexity inside paths would add a circular dependency +between path comparison and type unification. -In other words, `M(type ).t` should be rejected. +For example, `M(type ).t` should be rejected. ### Type application must be compiled as an empty structure @@ -82,9 +203,11 @@ let r2 = let module M = F(type float) in M.r If `F(type _)` does not launch any computation then `r1` and `r2` will be the same reference but with incompatible types. +Side note : for safety reason the functor above should have been generative. + ## Possible extensions This feature could be extended with other similar patterns to be a bit more expressive. - Implement the same feature with module types, -- Allow using parametric types in paths (for example `int list`). +- Allow using parametric types in paths (for example `M(type int list).t`). From 27e94773c6b191a372ade263195dade779132dc2 Mon Sep 17 00:00:00 2001 From: Samuel VIVIEN Date: Thu, 6 Jun 2024 15:06:29 +0200 Subject: [PATCH 4/7] Changed section and subsection ordering --- rfcs/type_arguments_for_modules.md | 95 +++++++++++++++--------------- 1 file changed, 46 insertions(+), 49 deletions(-) diff --git a/rfcs/type_arguments_for_modules.md b/rfcs/type_arguments_for_modules.md index 751adc6..48df375 100644 --- a/rfcs/type_arguments_for_modules.md +++ b/rfcs/type_arguments_for_modules.md @@ -9,55 +9,31 @@ to have a module containing only a single type by directly writing the type. In those cases we currently force the user to define a module containing that type. -## Use cases - -The motivation for this feature came from people working on modular explicits -and modular implicits. However, this feature will also benefit OCaml even -without modular implicits. - -### Modular explicits/implicits - -This feature becomes very important when taking into account modular explicits -and [modular implicits](https://arxiv.org/pdf/1512.01895). Because interactions -between the code language and the module language becomes much more frequent. - -In the case of modular implicits, a signature is given in order to search for a -compatible module. However, basic types are not compatible with parametrized -types. +## Proposed change -Thus, the module following module : +The idea is to extend the syntax of the module language with a new argument to +functors : ```ocaml -module AddList = struct - type 'a t = 'a list - let add = List.concat -end -``` - -does not match the signature of addition. +module M (type a) = ... -```ocaml -module type Add = sig - type t - val add : t -> t -> t -end +module M2 = functor (type a) -> ... +module type S = functor (type a) -> ... ``` -A way to fix this is to add a type argument to the `AddList` module. +and a new construction for applications. ```ocaml -module AddList (A : Any) = struct - type t = A.t list - let add : t -> t -> t = List.concat -``` +module M3 = M(type [`A | `B]) -However, this becomes problematic with modular implicits because you need to -define a sufficient amount of modules to access any possible types. This lead -Patrick Reader and Daniel Vlasits to write a whole file of modules containing -only a type field : -https://github.com/modular-implicits/imp/blob/master/lib/any.mli. +let f (x : M(type int).t) = x +``` +## Use cases +The motivation for this feature came from people working on modular explicits +and modular implicits. However, this feature will also benefit OCaml even +without modular implicits. ### Use cases in current OCaml @@ -66,7 +42,6 @@ structure attached to it. This is useful when we just want to store the type but never look into it. Cases where this pattern occurs exists in the OCaml code base. - #### State monad in algebraic effects tutorial For example when implementing a state monad such as the @@ -105,26 +80,48 @@ Another example of usage that feature in the OCaml would be in modules such as `Imperative.Graph.AbstractLabeled` requires a module containing a single type as argument (here the types for vertex labels). -## Proposed change +### Modular explicits/implicits -The idea is to extend the syntax of the module language with a new argument to -functors : +This feature becomes very important when taking into account modular explicits +and [modular implicits](https://arxiv.org/pdf/1512.01895). Because interactions +between the code language and the module language becomes much more frequent. -```ocaml -module M (type a) = ... +In the case of modular implicits, a signature is given in order to search for a +compatible module. However, basic types are not compatible with parametrized +types. -module M2 = functor (type a) -> ... -module type S = functor (type a) -> ... +Thus, the module following module : + +```ocaml +module AddList = struct + type 'a t = 'a list + let add = List.concat +end ``` -and a new construction for applications. +does not match the signature of addition. ```ocaml -module M3 = M(type [`A | `B]) +module type Add = sig + type t + val add : t -> t -> t +end +``` -let f (x : M(type int).t) = x +A way to fix this is to add a type argument to the `AddList` module. + +```ocaml +module AddList (A : Any) = struct + type t = A.t list + let add : t -> t -> t = List.concat ``` +However, this becomes problematic with modular implicits because you need to +define a sufficient amount of modules to access any possible types. This lead +Patrick Reader and Daniel Vlasits to write a whole file of modules containing +only a type field : +https://github.com/modular-implicits/imp/blob/master/lib/any.mli. + ## Proof of concept A first draft of this feature is implemented at From 8d83d03a0da53f764b1404dc638d3f42f761e701 Mon Sep 17 00:00:00 2001 From: samsa1 Date: Wed, 27 Nov 2024 16:27:55 +0100 Subject: [PATCH 5/7] Changed semantic to non-blocking lambda --- rfcs/type_arguments_for_modules.md | 108 ++++++++++++++++------------- 1 file changed, 60 insertions(+), 48 deletions(-) diff --git a/rfcs/type_arguments_for_modules.md b/rfcs/type_arguments_for_modules.md index 48df375..260dc08 100644 --- a/rfcs/type_arguments_for_modules.md +++ b/rfcs/type_arguments_for_modules.md @@ -42,34 +42,51 @@ structure attached to it. This is useful when we just want to store the type but never look into it. Cases where this pattern occurs exists in the OCaml code base. -#### State monad in algebraic effects tutorial +#### State monad For example when implementing a state monad such as the one in the example available at : -https://github.com/ocaml-multicore/ocaml-effects-tutorial/blob/998376931b7fdaed5d54cb96b39b301b993ba995/sources/state2.ml#L13-L40. +https://github.com/RedPRL/redtt/blob/ae76658873a647eb43d8cf84365a9d68e9a3273c/src/basis/StateMonad.ml. ```ocaml -module type STATE = sig - type t - val put : t -> unit - val get : unit -> t - val history : unit -> t list - val run : (unit -> unit) -> init:t -> unit +module type S = +sig + type state + + include Monad.S + + val get : state m + val set : state -> unit m + + val run : state -> 'a m -> 'a * state end -module State (S : sig type t end) : STATE with type t = S.t = struct +module M (X : sig type t end) : S with type state := X.t = +struct + type state = X.t + + type 'a m = state -> 'a * state - type t = S.t + let ret a st = a, st - type _ Effect.t += Get : t Effect.t + let bind m k st = + let a, st' = m st in + k a st' - let get () = perform Get + let try_ m kerr st = + try + m st + with exn -> + kerr exn st - let put v = failwith "not implemented" + let get st = + st, st - let history () = failwith "not implemented" + let set st _ = + (), st - let run f ~init = failwith "not implemented" + let run st m = + m st end ``` @@ -132,25 +149,41 @@ as arguments in modules paths. ## Semantic change -This feature does not change the semantic, it is just adds conciseness. +This feature has a slightly different semantic from usual functors. The idea is +to match the non-blocking `(type a)` from the core language. -The reason behind this is that all module expression using type arguments could -be rewritten to a module expression using a module wrapping the type. +Thus when defining `module M = functor (type a) -> S[a]`, `S` is directly +computed and `M(type t)` will not launch any computation and allocation. -For example : +However in order to preserve the type soundness of the OCaml language a +restriction needs to be applied : we use value restriction on `S`. Thus if `S` is +a structure : +- it cannot contain an expansive expressions (such as `ref None`), +- it cannot define an extensive type or extend an existing one, +- it cannot define an exception, +- it cannot define an object. + +The first restriction could be reduced to weak value restriction instead of weak +value restriction if required without impacting soundness. + +In order to lift those restriction the user can still write his functors using +a module containing only a single field that defines a type. -```ocaml -1: module F (type a) = BODY [a] -2: F (type p) -``` -could be encoded as the following. +Those restrictions comes from the fact that as `F(type _)` does not do any +computation in the example bellow, `r1` and `r2` are the same reference but have +incompatible types. ```ocaml -1: module F (A : Type) = BODY [A.t] -2: F (struct type t = p end) +module F (type a) = struct + let r : a option ref = ref None +end + +let r1 = let module M = F(type int) in M.r +let r2 = let module M = F(type float) in M.r ``` + ## Important restrictions This feature needs some restraints in order to be sound. @@ -180,31 +213,10 @@ between path comparison and type unification. For example, `M(type ).t` should be rejected. -### Type application must be compiled as an empty structure - -If we could avoid giving the type arguments at runtime for modules like with -functions we would have soundness issues. - -The following example show why it is important to preserve the information of -application all the way to binary code. - -```ocaml -module F (type a) = struct - let r : a option ref = ref None -end - -let r1 = let module M = F(type int) in M.r -let r2 = let module M = F(type float) in M.r -``` - -If `F(type _)` does not launch any computation then `r1` and `r2` will be the -same reference but with incompatible types. - -Side note : for safety reason the functor above should have been generative. - ## Possible extensions This feature could be extended with other similar patterns to be a bit more expressive. - Implement the same feature with module types, +- Replace value restriction in type-parametrized modules to weak value restriction. - Allow using parametric types in paths (for example `M(type int list).t`). From 702196405a5f63b520b7764b322b2613767cd231 Mon Sep 17 00:00:00 2001 From: samsa1 Date: Thu, 28 Nov 2024 13:31:43 +0100 Subject: [PATCH 6/7] Updated some cases after discussions with Florian --- rfcs/type_arguments_for_modules.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/rfcs/type_arguments_for_modules.md b/rfcs/type_arguments_for_modules.md index 260dc08..05b4864 100644 --- a/rfcs/type_arguments_for_modules.md +++ b/rfcs/type_arguments_for_modules.md @@ -159,8 +159,8 @@ However in order to preserve the type soundness of the OCaml language a restriction needs to be applied : we use value restriction on `S`. Thus if `S` is a structure : - it cannot contain an expansive expressions (such as `ref None`), -- it cannot define an extensive type or extend an existing one, -- it cannot define an exception, +- it cannot extend an existing extensible type (but not defining one), +- it cannot define a new exception (but not rebinding an exception), - it cannot define an object. The first restriction could be reduced to weak value restriction instead of weak From 236be864dcae3def84c5151bc1c01db51ef53b5f Mon Sep 17 00:00:00 2001 From: samsa1 Date: Fri, 29 Nov 2024 10:17:26 +0100 Subject: [PATCH 7/7] Added comment that impure functor application is not allowed --- rfcs/type_arguments_for_modules.md | 1 + 1 file changed, 1 insertion(+) diff --git a/rfcs/type_arguments_for_modules.md b/rfcs/type_arguments_for_modules.md index 05b4864..e7a0666 100644 --- a/rfcs/type_arguments_for_modules.md +++ b/rfcs/type_arguments_for_modules.md @@ -161,6 +161,7 @@ a structure : - it cannot contain an expansive expressions (such as `ref None`), - it cannot extend an existing extensible type (but not defining one), - it cannot define a new exception (but not rebinding an exception), +- it cannot contain a functor application to a module (could be reduced by allowing applications of pure functors), - it cannot define an object. The first restriction could be reduced to weak value restriction instead of weak