From fbf1219e4295bea34a9c43d3973bc02fc1f49149 Mon Sep 17 00:00:00 2001 From: octachron Date: Fri, 18 Mar 2016 23:12:58 +0100 Subject: [PATCH 1/5] Manual: polymorphic abstract types: more context --- manual/manual/refman/exten.etex | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/manual/manual/refman/exten.etex b/manual/manual/refman/exten.etex index 28e9c0deb..09ac4710b 100644 --- a/manual/manual/refman/exten.etex +++ b/manual/manual/refman/exten.etex @@ -577,7 +577,9 @@ Here is another example: S.elements (List.fold_right S.add l S.empty) \end{verbatim} -It is also extremely useful for first-class modules and GADTs. +It is also extremely useful for first-class modules (see +section~\ref{s-first-class-modules}) and generalized algebraic datatypes +(GADTs: see section~\ref{s:gadts}). \paragraph{Polymorphic syntax} (Introduced in OCaml 4.00) @@ -607,6 +609,8 @@ is automatically expanded into let rec f : 't1 't2. 't1 * 't2 list -> 't1 = fun (type t1) (type t2) -> (... : t1 * t2 list -> t1) \end{verbatim} +This syntax can be very useful when defining polymorphically recursive +functions involving GADTs. The same feature is provided for method definitions. The @'method!'@ form combines this extension with the @@ -1107,7 +1111,7 @@ intentional and should not trigger the warning. \section{Generalized algebraic datatypes} \ikwd{type\@\texttt{type}} -\ikwd{match\@\texttt{match}} +\ikwd{match\@\texttt{match}} \label{s:gadts} (Introduced in OCaml 4.00) From 73da8d89e774f4662f09f4936c637f05412a6a90 Mon Sep 17 00:00:00 2001 From: octachron Date: Sat, 19 Mar 2016 16:25:27 +0100 Subject: [PATCH 2/5] Manual: avoid "polymorphically" --- manual/manual/refman/exten.etex | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/manual/manual/refman/exten.etex b/manual/manual/refman/exten.etex index 09ac4710b..e37204f52 100644 --- a/manual/manual/refman/exten.etex +++ b/manual/manual/refman/exten.etex @@ -609,8 +609,8 @@ is automatically expanded into let rec f : 't1 't2. 't1 * 't2 list -> 't1 = fun (type t1) (type t2) -> (... : t1 * t2 list -> t1) \end{verbatim} -This syntax can be very useful when defining polymorphically recursive -functions involving GADTs. +This syntax can be very useful when defining recursive functions involving GADTs +(see \ref{s:gadts}). The same feature is provided for method definitions. The @'method!'@ form combines this extension with the From f8481a675659547cdcd72b9102eb9e013f844a89 Mon Sep 17 00:00:00 2001 From: octachron Date: Sat, 19 Mar 2016 16:26:57 +0100 Subject: [PATCH 3/5] Manual: detail polymorphic annotation for gadts --- manual/manual/refman/exten.etex | 29 +++++++++++++++++++++++++++-- 1 file changed, 27 insertions(+), 2 deletions(-) diff --git a/manual/manual/refman/exten.etex b/manual/manual/refman/exten.etex index e37204f52..d6def5137 100644 --- a/manual/manual/refman/exten.etex +++ b/manual/manual/refman/exten.etex @@ -609,8 +609,8 @@ is automatically expanded into let rec f : 't1 't2. 't1 * 't2 list -> 't1 = fun (type t1) (type t2) -> (... : t1 * t2 list -> t1) \end{verbatim} -This syntax can be very useful when defining recursive functions involving GADTs -(see \ref{s:gadts}). +This syntax can be very useful when defining recursive functions involving +GADTs, see the section~\ref{s:gadts} for a more detailed explanation. The same feature is provided for method definitions. The @'method!'@ form combines this extension with the @@ -1168,6 +1168,31 @@ Here is a concrete example: let two = eval (App (App (Add, Int 1), Int 1)) val two : int = 2 \end{verbatim} +It is important to remark that the function "eval" is using the +polymorphic syntax for locally abstract types. When defining a recursive +function that manipulates a GADT, explicit polymorphic recursion should +generally be used. For instance, the following definition fails with a +type error: +\begin{verbatim} + let rec eval (type a): a term -> a = function + | Int n -> n + | Add -> (fun x y -> x+y) + | App(f,x) -> (eval f) (eval x) +(* ^ + Error: This expression has type ($App_'b -> a) term but an expression was + expected of type 'a + The type constructor $App_'b would escape its scope +*) +\end{verbatim} +In absence of an explicit polymorphic annotation, a monomorphic type +is inferred for the recursive function. If a recursive call occurs +inside the function definition at a type that involves an +existential GADT type variable, this variable flows to the type of +the recursive function, and thus escapes its scope. In the above example, +this happens in the branch "App(f,x)" when "eval" is called with "f" as +an argument. Since the type of "eval" is "'a term -> 'a" whereas the +type of f is "($App_ 'b-> a)", the call "eval f" makes the existential +type "$App_'b" flows to the type variable "'a" and escape its scope. Type inference for GADTs is notoriously hard. This is due to the fact some types may become ambiguous when escaping From 5058a794439401787029d564d06836a84e9ebb7a Mon Sep 17 00:00:00 2001 From: octachron Date: Mon, 21 Mar 2016 13:45:40 +0100 Subject: [PATCH 4/5] Manual: gadt monomorphic error explanation This commit rewords the explanation of the erroneously monomorphic example in the GADT section and add a forward reference to the naming convention followed by the compiler for existential type appearing in error messages. --- manual/manual/refman/exten.etex | 20 ++++++++++++-------- 1 file changed, 12 insertions(+), 8 deletions(-) diff --git a/manual/manual/refman/exten.etex b/manual/manual/refman/exten.etex index d6def5137..e6975e406 100644 --- a/manual/manual/refman/exten.etex +++ b/manual/manual/refman/exten.etex @@ -1186,13 +1186,16 @@ type error: \end{verbatim} In absence of an explicit polymorphic annotation, a monomorphic type is inferred for the recursive function. If a recursive call occurs -inside the function definition at a type that involves an -existential GADT type variable, this variable flows to the type of -the recursive function, and thus escapes its scope. In the above example, -this happens in the branch "App(f,x)" when "eval" is called with "f" as -an argument. Since the type of "eval" is "'a term -> 'a" whereas the -type of f is "($App_ 'b-> a)", the call "eval f" makes the existential -type "$App_'b" flows to the type variable "'a" and escape its scope. +inside the function definition at a type that involves an existential +GADT type variable, this variable flows to the type of the recursive +function, and thus escapes its scope. In the above example, this happens +in the branch "App(f,x)" when "eval" is called with "f" as an argument. +In this branch, the type of "f" is "($App_ 'b-> a)". The prefix "$" in +"$App_ 'b" denotes an existential type named by the compiler +(see~\ref{p:existential-names}). Since the type of "eval" is +"'a term -> 'a", the call "eval f" makes the existential type "$App_'b" +flows to the type variable "'a" and escape its scope. This triggers the +above error. Type inference for GADTs is notoriously hard. This is due to the fact some types may become ambiguous when escaping @@ -1349,7 +1352,8 @@ to implement dynamic types. | None -> None | Some Eq -> Some x \end{verbatim} -\paragraph{Existential type names in error messages} +\paragraph{Existential type names in error messages}% +\label{p:existential-names} (Updated in OCaml 4.03.0) From da0faee1d359b3f3b154dc640b6d41e037967c9b Mon Sep 17 00:00:00 2001 From: octachron Date: Mon, 21 Mar 2016 20:26:38 +0100 Subject: [PATCH 5/5] Manual: paragraph headers in section 7.16 (GADTs) --- manual/manual/refman/exten.etex | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/manual/manual/refman/exten.etex b/manual/manual/refman/exten.etex index e6975e406..d10ae9f82 100644 --- a/manual/manual/refman/exten.etex +++ b/manual/manual/refman/exten.etex @@ -1152,6 +1152,8 @@ If a constructor has some existential variables, fresh locally abstract types are generated, and they must not escape the scope of this branch. +\paragraph{Recursive functions} + Here is a concrete example: \begin{verbatim} type _ term = @@ -1197,6 +1199,8 @@ In this branch, the type of "f" is "($App_ 'b-> a)". The prefix "$" in flows to the type variable "'a" and escape its scope. This triggers the above error. +\paragraph{Type inference} + Type inference for GADTs is notoriously hard. This is due to the fact some types may become ambiguous when escaping from a branch.