Commit 74a34e81 authored by POTTIER Francois's avatar POTTIER Francois

Finished the new subsection on map_from_fold.

parent c5fdba45
2017/02/09:
Documentation: a new subsection on OCaml objects,
entitled "Where the expressiveness of OCaml's type system falls short".
This section explains why "map" cannot be a subclass of "fold",
even though it should be.
2017/02/07:
VisitorsRuntime: make every method monomorphic in 'env.
In theory, this should be more flexible, as it allows overriding these methods
with code that actually uses the environment. In practice, I don't have a
compelling example where that would be necessary or useful.
In theory, this should be more flexible, as it allows overriding these methods
with code that actually uses the environment. In practice, I don't have a
compelling example where that would be necessary or useful.
2017/01/31:
Documentation: added an example of constructing a lexicographic ordering.
......
......@@ -1402,7 +1402,37 @@ shown in \fref{fig:map_from_fold:type}. This type is \emph{not} polymorphic
in~\oc|'b|, thus strictly less general than the type of the method
\tyconvisitor{option} in the class \map (\fref{fig:map_from_fold}).
What would it take to repair this problem? Apparently, the type of the method
\tyconvisitor{option} in the class \fold is not general enough. Whereas the
type variables \oc|'r| and \oc|'s| currently have kind \oc|*|, it seems that
they should have kind \oc|* -> *|. The type of the class \fold should be as
follows:
%
\begin{mdframed}[backgroundcolor=green!10]
\begin{lstlisting}
class ['self] fold : object ('self)
method private visit_option: 'a 'b .
('env -> 'a -> 'r['b]) -> 'env -> 'a option -> 's['b]
method private virtual build_None: 'b . 'env -> 's['b]
method private virtual build_Some: 'b . 'env -> 'r['b] -> 's['b]
end
\end{lstlisting}
\end{mdframed}
This is not valid OCaml: we write \oc|'r[b]| for the type-level application of
\oc|'r| to \oc|'b|. The type of each method is universally quantified in
\oc|'b|, as desired. The type of \tyconvisitor{option} seems to have the
desired generality. By instantiating both~\oc|'r| and~\oc|'s| with the
type-level function \oc|fun 'b -> 'z|, we obtain the type of
\tyconvisitor{option} in the class \reduce. By instantiating \oc|'r| and
\oc|'s| with the type-level functions
%
\oc|fun 'b -> 'b| and \oc|fun 'b -> 'b option|, respectively, we obtain the
type of \tyconvisitor{option} in the class \map.
This suggests that higher kinds, type-level functions, and type-level
$\beta$-reduction might be valuable features, not just in functional
programming languages, but also in an object-oriented programming setting.
% ------------------------------------------------------------------------------
% ------------------------------------------------------------------------------
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment