Hi,
would I be right to conclude that polymorphic types in OCaml would not have been needed if modules were better integrated in the language?
E.g. taking OCaml as it is now
Can you give an example of what you mean by āif modules were better integrated in the languageā?
Polymorphism is all about generalising code so it has more utility. I donāt think OCaml would be very expressive without it at all. Even operators such as (|>) rely on polymorphism to work, i.e. it has the function signature of
val (|>) : 'a -> ('a -> 'b) -> 'b
You cannot write the following function with monomorphic functor currently:
type 'a t =
| Elt of 'a
| List of 'a list t
let rec list: 'a. 'a t -> 'a list = function
| Elt x -> [x]
| List l -> List.concat (list l)
since the corresponding recursive functor is unsafe:
module Listify(T: sig type t end) = struct
type t = T.t list
end
module rec L: functor (T: sig type t end) -> sig
type t =
| Elt of T.t
| List of L(Listify(T)).t
val list: t -> T.t list
end = functor (T: sig type t end) -> struct
type t =
| Elt of T.t
| List of L(Listify(T)).t
let rec list = function
| Elt x -> [x]
| List l ->
let module Sub = L(Listify(T)) in
List.concat (Sub.list l)
end
But even without this limitation, modules are far more complex than polymorphic types. Expressing the simple feature (polymorphic types) using the complex one (modules and functors) for the sake of losing type inference (and we also need explicit type applications with functors) does not seem like a good idea.
Hi, but you can write something like this right?
module type SINGULART = sig type t end
module PIPEF(TA : SINGULART, TB : SINGULART) = struct
let pipef (a : TA.t) (ff : TA.t -> TB.t) : TB.t = ff a
end
PIPEF(struct type t = int end, struct type t = float end).pipef a ff
I guess I meant if the above was less painful to write
Thanks a lot for your response @lepoetemaudit, I will ponder upon it. Loosing inference obviously is not a goal 
The goal is figuring out what a more minimal language similar in spirit to OCaml might look like. Cutting features is the goal.
I am trying to make sense of 1ML - very slowlyā¦
Ah okay, now I see what you mean. Thatās interesting - perhaps ultra lightweight functors could be a viable way of doing things, and everything is monomorphic at use. I wonder if it wouldnāt feel a bit like macros or templates in other statically typed languages.
If everything is monomorphic that would be like C++ or Rust and probably blow up compile times and executable sizes.
Thanks a lot, I didnāt realize functors yield monomorphic code. Itās not obvious form language spec is it? Isnāt it true an OCaml implementation could exist which would compile functors polymorphically?
And if functors were compiled polymorphically then this issue
would probably cease to exist, since polymorphically compiled functors could acquire full power of polymorphic functions?
But preserving type interference for the simpler core language is one of the aim of the separation between the module and core type systems.
This is a consequence of your constraint of āmodules without polymorphic typesā, nothing more. One could avoid this issue by specializing functors applications on module with only type components. However, this would require introducing a separate kind of modules if one want to keep higher-order functors.
Slightly orthogonal note, but itās not really āunsafeā, merely not handled by the recursive module compilation. Roughly speaking, itās fairly trivial (and correct) to mark functors as always safe, but the drawback is that more recursive definitions will end up throwing Undefined_recursive_module exceptions. This is not very intuitive (the more safe modules you have, the more likely you are to get these exceptions, with or without functors), and will likely impact existing code, so I donāt think weāll do it in OCaml, but in a language where functors are more prevalent I would expect this to be supported.
For reference: the following paper describes the translation of SML to an internal language (comprising a core language and a module language), where SML let-polymorphism is translated to functors.
Chris Stone and Robert Harper.
A Type-Theoretic Interpretation of Standard ML.
Milner Festschrifft. 2000.
Citation. PS. PDF.
Personally, I think this approach is not much of a simplification. As @octachron wrote, it also makes polymorphic recursion much harder to add.
More recent work on the metatheory of ML-like languages shoots for unified internal languages where both the core language and the module language can be represented.
ā¦wouldnāt compiling a module to a vtable, C++ style,
allow to compile functors polymorphically in all cases?
.mli would prescribe which āvirtual methodsā to include into a vtable
vtable could also contain size information for abstract types
@xavierleroy Iām honoured to see you here
No? You would have the same issue that in C++ with a separate vtable for each instance of a template class. Typically, C++ cannot handle polymorphic recursion at all. Trying to compile, the C++ version of the list function above is quite āfunā.
Fair enoughā¦ being more precise
it seems possible to compile non-recursive functors polymorphically even if their arguments are not limited to modules with only type components; value components of such argument modules could go into vtables; so it seems introducing a separate kind of modules could be avoided
polymorphic recursion is an interesting challengeā¦ it depends on low-level details of run-timeā¦ but if āeveryting is a pointerā does it not look somewhat possible to share vtable-s between many (all?) instances of the same ātemplate classā? The fact that polymorphic recursion can be compiled at all seems to suggest there should be a way to compile such functors polymorphically too.
P.S. btw Iām hugely thankful for the polymorphic recursion example; I certainly heard about polymorphic recursion before but never before did I appreciate what kind of a thing these recursive types are Iām wondering if there is much practical use, but the sheer fact itās possible in OCaml is mind-opening to me.
I think that was part of their inspiration for this line of inquiry.
Oops, I missed that.
1ML is very relevant, but iiuc, in the opposite direction? Rather than suggesting we might do away with polymorphism, the implication seems to be that the polymorphism of System F (omega) is enough, and subsumes parametric and first-class modules?
Big thanks to everybody! Thank you @octachron, @smolkaj, @shonfeder, @xavierleroy
Iām just super-slow at comprehending 1ML papersā¦
I still havenāt made sense of how polymorphic recursion is treated in 1ML - if it is at all supported