Who needs polymorphics types? (when we have modules)

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

  • it is possible to code without using polymorphic types
  • and yet retain the full expressive power of OCaml
  • and the only downside would be verbosity and loss of inference?

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
1 Like

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.

3 Likes

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 :slight_smile: 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.

1 Like

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.

4 Likes

…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 :slight_smile:

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

  1. 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

  2. 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 :slight_smile: I’m wondering if there is much practical use, but the sheer fact it’s possible in OCaml is mind-opening to me.

You may find the following related work interesting: 1ML - core and modules united

2 Likes

I think that was part of their inspiration for this line of inquiry. :slight_smile:

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?

3 Likes

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

1 Like