Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Manual: New chapter on polymorphic types and functions in the tutorial #594

Merged
merged 35 commits into from Oct 16, 2017

Conversation

@Octachron
Copy link
Contributor

Octachron commented May 22, 2016

This PR proposes to add a new chapter to the manual to describe in more detail the properties of polymorphic functions and type in OCaml. More precisely, the new chapter would describe:

  • the relaxed value restriction: starting from weakly polymorphic types to the relaxed value restriction itself
  • polymorphic recursion and the use of explicit polymorphic annotation
  • higher-rank polymorphic functions using explicitly polymorphic record fields or object methods.

The main objective of this PR is to gather in the manual the information that is already available on the web but not always easily discoverable.

As an important side-effect, this PR moves the description of explicitly polymorphic type annotation out of the extension section of the language reference manual.

Note: this is still a work in progress, comments and criticisms are more than welcome.

undecidable; therefore using this kind of higher-rank function requires to
handle manually these universally quantified type.

In OCaml, there is three main way to introduce this kind of explicit universally

This comment has been minimized.

Copy link
@objmagic

objmagic May 22, 2016

Contributor

there are three main ways


This distinction between weakly and generic polymorphic type variable protects
OCaml program from unsoundness and runtime errors. To understand from where
unsoundness might come, consider this simple function which swap a value "x"

This comment has been minimized.

Copy link
@objmagic

objmagic May 22, 2016

Contributor

swaps

\begin{caml_example}
let id_again = fun x -> (fun x -> x) (fun x -> x) x;;
\end{caml_example}
Whith this argument, "id_again" is seen as a function definition by the type

This comment has been minimized.

Copy link
@objmagic

objmagic May 22, 2016

Contributor

with

Allied with this relaxed value restriction, type parameter covariance
helps to avoid eta-expansion in many situation.

\subsection{Asbract data types}

This comment has been minimized.

Copy link
@objmagic

objmagic May 22, 2016

Contributor

abstract

This comment has been minimized.

Copy link
@Octachron

Octachron May 22, 2016

Author Contributor

Thanks for noticing these errors.

This chapter details each of these situations and, if it is possible,
how to recover genericity.

\section{Weak polymorphism and mutations}

This comment has been minimized.

Copy link
@gasche

gasche May 24, 2016

Member

mutation

This comment has been minimized.

Copy link
@Octachron

Octachron May 25, 2016

Author Contributor

Fixed.


More generally, weak types protect the program from undue mutation of
values with a polymorphic type. Moreover, weak type cannot appear as the type
of toplevel values: the type of values must be known at compilation time.

This comment has been minimized.

Copy link
@gasche

gasche May 24, 2016

Member

You could point out that this would be problematic if two distinct modules relied on this module's interface, unifying exported weak types to different things. You should spell out the error message in entirety (for example, by using an example that raises it), because it's confusing when you first see it and it would be a good anchor for people looking for the error message text.

This comment has been minimized.

Copy link
@Octachron

Octachron May 25, 2016

Author Contributor

Good points. I have also added a remark on the fact that this error cannot be repoduced in the toplevel interpreter to avoid potential confusion.

There is another partial solution to the problem of unnecessary weak type
in the type of value, which is implemented directly within the type
checker. Briefly, it is possible to prove that weak types that only appear
as type parameters in a covariant position can be safely generalized to

This comment has been minimized.

Copy link
@gasche

gasche May 24, 2016

Member

People sometimes use "positive position" instead of "covariant position", and it makes as much sense when subtyping is not considered. It would be helpful to refer to this other wording at some point.

This comment has been minimized.

Copy link
@Octachron

Octachron May 25, 2016

Author Contributor

I have added a short mention. It may be better to weave the name more cohesively in the text.

\begin{caml_example}
type 'a tree = Leaf of 'a | Branch of 'a tree * 'a tree;;
\end{caml_example}
is covariant in its parameter "'a" if it preserves the order of the

This comment has been minimized.

Copy link
@gasche

gasche May 24, 2016

Member

I feel that this description is too abstract. (preserves the order of the subtyping relationship?).

This comment has been minimized.

Copy link
@Octachron

Octachron May 25, 2016

Author Contributor

You are right, I fear that I let out too much of my inner mathematician here. Anyway, the whole section have been rewritten (see below).

Then, if the type constructor "'a t" is covariant in "'a",
the subtyping relationship "x :> xy" can be lifted to "x t :> xy t".

This notion of covariance can be used to prove that a weak type"'_a" that

This comment has been minimized.

Copy link
@gasche

gasche May 24, 2016

Member

Another explanation would be that as soon as a type variable appears in a position describing mutable state, such as 'a ref, it becomes invariant, and that thus covariant variables will never denote mutable locations and can be safely generalized.

I don't know whether we need to have both explanations. I feel that you are repeating a lot of what was rather clearly written in Jacques Garrigue's article, and that it may be enough to more concisely explain the behaviour and intuition, and refer to the article for people looking for an in-depth explanation.

(Also that could help in keeping the documentation less abstract/formal.)

This comment has been minimized.

Copy link
@Octachron

Octachron May 25, 2016

Author Contributor

I have tentatively rewritten the variance section to put more emphasis on concrete examples. Linking directly invariance with mutable state seems to give a better flow to the text.
I would also add a link to Jacques Guarrigue's article later.


module Implementation = struct
type 'a t = { get: int -> 'a; len:int }
let empty ()= let a = [||] in { get = (fun n -> a.(n) ); len = 0 }

This comment has been minimized.

Copy link
@gasche

gasche May 24, 2016

Member

That code is too complex; what about just using lists under the hood? (Or int -> 'a option if you want something exotic)

This comment has been minimized.

Copy link
@Octachron

Octachron May 25, 2016

Author Contributor

Sure.

helps to avoid eta-expansion in many situation.

\subsection{Abstract data types}
Moreover, when the associated type definitions are visible, the type checker

This comment has been minimized.

Copy link
@gasche

gasche May 24, 2016

Member

Let's avoid "associated type" which means something else. You could just say "When the type definitions are exposed".

This comment has been minimized.

Copy link
@Octachron

Octachron May 25, 2016

Author Contributor

Fixed.

@gasche

This comment has been minimized.

Copy link
Member

gasche commented May 24, 2016

I think that's a good idea. I reviewed the part before "Polymorphic recursion" so far. I think it is important to keep things simple, concrete and example-based as soon as we can, and avoid formalism -- because it can turn people away and make the document feel less accessible.

@Octachron

This comment has been minimized.

Copy link
Contributor Author

Octachron commented May 25, 2016

@gasche
Thanks for your time and review.

@bluddy

This comment has been minimized.

Copy link

bluddy commented May 25, 2016

Thank you so much for doing this!

Error: The type of this expression, '_a option ref,
contains type variables that cannot be generalized
\end{verbatim}
In this case, the error can be solved by either fixing the relevant

This comment has been minimized.

Copy link
@gasche

gasche Jun 2, 2016

Member

fixing suggests that something was "broken" before, you should rather use something like

To solve this error, it suffices to add an explicit type annotation to make the type precise at declaration time.

I would also add:

This is in any case a good practice for such global mutable variables; otherwise, it will "adopt" the first type of use, which can give confusing type errors if there is a mistake at the first use site -- later, correct uses would be flagged as errors.

This comment has been minimized.

Copy link
@Octachron

Octachron Jun 2, 2016

Author Contributor

Good points. I have adopted your new paragraph with some stylistic modification.

let option_ref: int option ref = ref None
\end{verbatim}
or by transforming "option_ref" in a function%
\begin{verbatim}

This comment has been minimized.

Copy link
@gasche

gasche Jun 2, 2016

Member

I'm not sure it makes sense to show the two solutions on the same example. It seems pretty clear when I read let foo = ref None that a mutable global variable is intended to be initialized later, and making it a function changes its semantics in a way that seems rather artificial to me. Later examples will propose eta-expansion as a solution to get more polymorphism, so maybe you could just this ", or...." part of the paragraph.

This comment has been minimized.

Copy link
@Octachron

Octachron Jun 2, 2016

Author Contributor

Yes, skipping the second point is probably a good idea since it does not really make sense with this specific example.

\begin{verbatim}
let option_ref () = ref None
\end{verbatim}
An important point is that, by nature, this error cannot appear in OCaml

This comment has been minimized.

Copy link
@gasche

gasche Jun 2, 2016

Member

I think we could skip that paragraph as well -- I'm surprised I notice how to shorten other people's texts when mine are always so verbose. The explanation you give is not very good¹, and in any case people are rarely surprised when stuff works, they want explanations when it does not.

¹: The reason why weak polymorphic values are forbidden at module interfaces is that the module may be linked twice with different unifications, making it unsound. On the other hand, a toplevel declaration cannot be used by two consumers simultaneously, there is a single "continuation" which is the rest of the toplevel section. The sentence below ("in the toplevel, ...") is not really an explanation.

This comment has been minimized.

Copy link
@Octachron

Octachron Jun 2, 2016

Author Contributor

You are right the explanation is bad.

Anyway, I was worried about people trying to reproduce the error message in a toplevel after reading the previous paragraph. But it is probably a too unfrequent occurence to warrant any explanation.

@damiendoligez

This comment has been minimized.

Copy link
Member

damiendoligez commented Jun 7, 2016

@objmagic @gasche Are you done reviewing?

@gasche

This comment has been minimized.

Copy link
Member

gasche commented Jun 7, 2016

I'm not done, unfortunately. I need to invest more time and there are in places some reformulation that I'm thinking of proposing (instead of just commenting). Are you asking because you would like to merge soon? What's the calendar for when this should be settled?

(This manual change is more ambitious than others and it also hits closer to home in terms of discussing non-trivial points of advanced type system / language design. I could see myself falling into an unbounded process of gradual refinement (especially if we get Didier involved, which would be a good idea). I think that we should instead aim for a mergeable version that is reasonable, and refine later if we want to -- le mieux est l'ennemi du bien -- but I haven't read the whole thing yet so I cannot say I'm there.)

@Octachron what's your own feeling/preference? Does it feel "ready" to you, do you have specific expectations in term of perfectionism level vs. merge time?

@Octachron

This comment has been minimized.

Copy link
Contributor Author

Octachron commented Jun 7, 2016

For this specific PR, my objective is more to reach a good first step that could be readily improved upon in the future, either directly or by collecting feedback. I readily admit that with the limited depth of my understanding on some of the subjects covered trying to get it right on the first version would be overly ambitious.

However, there are still rough parts, spelling errors and some unnecessary complexity
in the current version, that I would like to correct (by the end of the week if needed?). I also would not mind some external confirmation that there is no factual errors in the later part of the text.

@gasche, if you find the time to write these propositions, I would be interested to merge them.

p.s. :

@damiendoligez , @gasche: As an echo to the trunk manual discussion, this is another situation where I feel that it might be nice to have an experimental web version of the manual to gather feedback more easily.

@mshinwell mshinwell changed the title [WIP] Manual: New chapter on polymorphic types and functions in the tutorial Manual: New chapter on polymorphic types and functions in the tutorial Jun 10, 2016
@damiendoligez

This comment has been minimized.

Copy link
Member

damiendoligez commented Jun 15, 2016

@gasche There's no calendar, I was just pinging the PR to see if it was ready.

polymorphic type variables, sometimes shortened as weak type variables. A weak
type variable is a placeholder for a single type that is currently unknown.
Once the specific type "t" behind the placeholder type "'_a" known, all
occurrences of "'_a" will be replaced by "t".

This comment has been minimized.

Copy link
@gerdstolpmann

gerdstolpmann Jul 6, 2016

Give an example here, e.g.

let store = ref None
  store : `_a option ref
store := Some 1
  store : int option ref

This comment has been minimized.

Copy link
@Octachron

Octachron Jul 7, 2016

Author Contributor

Thanks for the suggestion, giving an example here improve nicely the flow of the section.

undue mutation of values with a polymorphic type.

%todo: fix indentation in pdfmanual
Moreover, weak type cannot appear as the type of toplevel values:

This comment has been minimized.

Copy link
@gerdstolpmann

gerdstolpmann Jul 6, 2016

values in toplevel modules

This comment has been minimized.

Copy link
@Octachron

Octachron Jul 7, 2016

Author Contributor

I would rather say that weak types cannot appear in signatures in order
to include cases like

module M = struct module N = struct let store = ref None end end
replaced by weak types in a modular way is a difficult question. A first
natural idea would be to state that any mutable object like reference, array
or a record mutable field should never have a polymorphic type. Unfortunately,
this rule is not sufficient, as illustrated by the following function that

This comment has been minimized.

Copy link
@gerdstolpmann

gerdstolpmann Jul 6, 2016

Stumbling as reader over this. Better: "this rule is not only impractical but also not even a sufficient solution to the problem, as illustrated ..."

This comment has been minimized.

Copy link
@Octachron

Octachron Jul 7, 2016

Author Contributor

Thanks for your remark, I did not notice that this hand-wavy description fits multiple
type system (some which are even sound as far as I can tell). So it is probably better
to delete my babbling and shows the problem directly. For instance,

Identifying the exact context in which polymorphic types should be
replaced by weak types in a modular way is a difficult question. Indeed
the type system system must take in account the fact that functions
can hide persistent mutable state, as illustrated ...
At the same time, it should be possible to use a local mutable state without
impacting the type of a function.

The value restriction combined with this generalization for covariant type
parameters is called the relaxed value restriction.

%question: is here the best place for describing variance?

This comment has been minimized.

Copy link
@gerdstolpmann

gerdstolpmann Jul 7, 2016

Avoid variance in the main text, e.g. "In simple words, the generalization can also be done when the type only refers to values returned by functions that never appear as arguments of other functions (i.e. the values are all in covariant positions)"

This comment has been minimized.

Copy link
@Octachron

Octachron Jul 7, 2016

Author Contributor

I am not sure that it is better to avoid the word variance here. I fear that any reasonable approximation would end up quite wordy:

"As a first approximation, the generalization can also be done when the type only refers to values returned by functions that never appear as arguments of other functions or parameter of a mutable type constructor."

Is it not simpler to use the name "variance" and then explains what is variance? Note that it may be well my academic background speaking here.


\section{Polymorphic recursion}\label{s:polymorphic-recursion}

The second major class of non-genericty is directly related to the problem

This comment has been minimized.

Copy link
@gerdstolpmann

gerdstolpmann Jul 7, 2016

typo: genericity

The second major class of non-genericty is directly related to the problem
of type inference for polymorphic function. In some circumstances, the type
inferred by OCaml might be not general enough to allow the definition of
some recursive functions on recursive type.

This comment has been minimized.

Copy link
@gerdstolpmann

gerdstolpmann Jul 7, 2016

Before going on with this "brittle" stuff, show the reader safe grounds. Explain what a regular ADT is before going on with non-regular types. It is important to see the difference.

This comment has been minimized.

Copy link
@Octachron

Octachron Jul 7, 2016

Author Contributor

Well, up to now, I was not fully aware of the distinction between regular and non-regular ADT. Thanks for the pointer! And you are right making the distinction will make the origin of the problem much clearer for the reader.

@Octachron Octachron force-pushed the Octachron:manual_nme_polymorphism branch from c367cc5 to a543123 Oct 14, 2017
@Octachron

This comment has been minimized.

Copy link
Contributor Author

Octachron commented Oct 14, 2017

I think that squashing the commits is probably better for this PR, since the majority of commits after the first one are small fixes with an useless commit message for an external reader.

@gasche
gasche approved these changes Oct 14, 2017
Copy link
Member

gasche left a comment

Approved (on the basis of Damien's more exhaustive review). @Octachron, would you do the work of squashing, merging and cherry-picking in 4.06?

@Octachron

This comment has been minimized.

Copy link
Contributor Author

Octachron commented Oct 14, 2017

@gasche : Certainly, I will.

@Octachron Octachron merged commit 2675b1f into ocaml:trunk Oct 16, 2017
2 checks passed
2 checks passed
continuous-integration/appveyor/pr AppVeyor build succeeded
Details
continuous-integration/travis-ci/pr The Travis CI build passed
Details
@Octachron

This comment has been minimized.

Copy link
Contributor Author

Octachron commented Oct 16, 2017

Merged and cherry-picked on 4.06(641dab3).

@gasche

This comment has been minimized.

Copy link
Member

gasche commented Oct 16, 2017

Thanks! And thank for your work on the manual in general.

Something I've been thinking about but haven't got around to doing it yet is to make a pre-release of the 4.06 manual in a temporary place, to include in 4.06-preparation-related announcements. If you also think this could be of use, would you be interested in taking care of it? (I have web space where it's easy to push temporary stuff; if you don't, I will handle the whole thing).

@Octachron

This comment has been minimized.

Copy link
Contributor Author

Octachron commented Oct 16, 2017

I think releasing a beta version of the manual is a good idea. If it just a matter of putting a 4.06 version of the manual online, I could do the same thing as http://www.polychoron.fr/ocaml-nonmanual/mpr7497/ and make it available at http://www.polychoron.fr/ocaml-beta-manual/4.06/ with a slightly adjusted disclaimer text (and keeping the "alternative" color scheme).

@gasche

This comment has been minimized.

Copy link
Member

gasche commented Oct 16, 2017

Yes, I think that would be very nice. You could advertise it in the email thread of the latest beta announcement, and possibly point to specific part of the manuals that changed (typically this new section).

@Drup

This comment has been minimized.

Copy link
Contributor

Drup commented Oct 20, 2017

@gasche Couldn't we just have a version of the manual for trunk automatically uploaded ? (http://caml.inria.fr/pub/docs/manual-ocaml-trunk/ , for example)

@gasche

This comment has been minimized.

Copy link
Member

gasche commented Oct 20, 2017

We certainly could, but someone has to do the work.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
You can’t perform that action at this time.