Add pure functors to the module system

[samsa1]

In this PR we introduce a new type of functors : pure functors.

module PureFunctor : (M : S) => sig ... end
module PureFunctor2 : (M : S) => sig ... end
module PureFunctor3 : functor [@pure] (M : S) -> sig ... end

Such functors work like normal applicative functors and are coercible. The main objective is to be retro-compatible while
having the possibility to give stronger guarantees when writing a functor.

What is a pure functor

The objective of this definition is to make CSE valid on all such functors as explained in the motivation section.

A pure functor is an application functor with aditionnal restrictions:

• We don't want to generate any mutable state or have any side effect : this leads to a more restrictive version of is_nonexpansive that tests purity of expression
• We want to have value sharing : extending an extensible type is not permitted.
• All functor application inside must also be pure

What is allowed in a pure functor:

• type, module type, class type definitions
• rebinding an exception or other extension of an extensible type
• pure functor applications
• all expression and (rec-)bindings of expression accepted by an more restrictive version of is_nonexpansive (already used for value restriction) that does not allow raise _, assert _ and goes through sequences.

Motivation

While working on #13649 I realized that not having a notion of pure functors in OCaml was highly restricting.

As such it is possible to do many impure operation inside a applicative functor such as:

• Defining exceptions,
• Creating mutable states

Because of this we don't have the sharing of values between applicative functors and #13649 disallows all functor applications.

Having pure functors also allows new optimizations on module expression such as CSE which would be mandatory for something like modular implicits (Implicit functors should be pure).

However for backward compatibility reason we cannot force applicative functors to be pure (or at least not with a prior notice). As such I propose to introduce a new type of functors : pure applicative functors.

Behaviour

• Subtyping : a pure applicative functor can be considered as an impure applicative functor :

module F_valid (M : sig module F : S => T end) : sig module F : S -> T end = M

• Purity of module expression is inferred if not specifically annotated as pure.

module F_pure (M : S) = sig end
module F_impure (M : S) = sig exception E end

To be discussed

The first proposition would be to annotated pure functors using => (or the [@pure] attribute if people want to be
valid through multiple versions of OCaml) but it is open to discussion.

The syntax is what I think the most complex part of this PR. Which syntax do we want ?

The main constraints being : we don't have n-ary functors, thus purity is associated for each argument and not as a whole.

All pure except the last argument (implemented in this iteration) :

Only the last argument and impure applicative arguments arrow's are mandatory with -> for impurity, => for purity.
All other arrows are optional.
() => ... is valid and can be impure because () overwrite the purity annotation of the arrow.

This permit writing things like : module F : (M : S) (N : T) -> ... or module F : (M : S) () -> ... where we can easily expect the first argument be pure.

If both argument of a functor are impure then one must write (M : S) -> (N : T) -> ... (but such a pattern seems really rare).

All arguments have the same purity :

If one uses a syntax with multiple arguments for a single arrow than all arguments will have the purity of the corresponding arrow :
Thus (M : S) -> (N : T) -> ... is equivalent to (M : S) (N : T) -> ... and (M : S) => (N : T) => ... to (M : S) (N : T) => ...

Another proposition ?

[nojb]

Thanks @samsa1 for the description. However unless I missed something there is no specification of what a pure functor actually is :)

I guess we are talking about functors whose body consists only of type definitions, function bindings and other pure constructs, not including possibly side-effecting operations (such as ordinary variable bindings let v = e). Is that right?

[samsa1]

Indeed I've forgot to add a specification. I added a paragraph to explain the intuition and actual restriction on what a pure functor is : mostly a syntactic restriction that rejects all possibly side-effecting operations

[lpw25]

There is a little-known compiler option -no-app-funct that disables applicative behaviour for functors. How about adding -no-impure-app-funct that only allows applicative behaviour for pure functors?

[chambart]

This probably shouldn't be a boolean.
I think that this should either be a 'purity' type or this case should be turned into an inline record

[chambart]

This should also be a purity type.

[lpw25]

One thing that I think is not necessarily obvious, and is probably relevant to discussions of this feature, is that you can demand that only pure functors be treated as applicative without changing expressivity. That is because applicative behaviour only matters for types in the module, and given an impure applicative functor:

module F (X : S) = struct
  let foo = ...
  type bar = ...
  let baz = ...
end

you can always replace it with a pair of a functors: one obviously pure and the other generative:

module F_types (X : S) = struct
  type bar = ...
end
module F (X : S) () = struct
  include F_types(X)
  let foo = ...
  let baz = ...
end

This ability to split an impure applicative functor is what makes them sound in the first place. That is why any feature which would prevent the split -- e.g. unpacking first-class modules -- is banned from the body of applicative functors.

This means that -- from the perspective of expressivity -- you don't actually need to worry about how precise your tracking of purity is. If your purity checking has false negatives, then users can just do the transformation to get equivalent applicative behaviour anyway.

[gasche]

() => ... is valid and can be impure because () overwrite the purity annotation of the arrow.

This does not make sense to me and I would refer for this combination to be rejected.

[samsa1]

() => ... is valid and can be impure because () overwrite the purity annotation of the arrow.

This does not make sense to me and I would refer for this combination to be rejected.

I agree that it does make much sense so it is never printed. The main reason I decided to make it legit was to have a simpler parser. However I'll look to see if it is possible to have a nice looking solution rejecting that case.

edit : it seems like a 38 lines patch so it seems a good thing to go into that direction

[gasche]

Maybe you could accept it in the parser and reject it in the type-checker ? This also makes it easier (for now) to produce a precise error message.

[samsa1]

Last week I had discussion about this feature with the flambda2 team (in particular @lthls, @chambart and @Ekdohibs). One of the points being how it could interact with the back-end and in particular while also considering modular implicits.

One point that was raised was that if we wanted to be able to do CSE on modules expressions as presented in Implicit functors should be pure we also wanted to ensure termination (it is necessary if we want to be able to lift module expressions out of functions). However this corresponds to a stricter notion of purity than the one present in this PR that does not consider divergence as a side-effect.
A first proposal of a termination check could be to disallow applying inside a functor any functor that has been received as argument (this should prevent any divergence such as the one in Girard's paradox by @lpw25). It feels that such a restriction would not penalize examples we might want to write with modular implicits and could be refined later on to something more subtle.

Side note : we should check that this PR behaves correctly with recursive functors as they might raise exceptions at application which is a side effect.
Side note 2 : if we accepted functors as argument having a way to have purity polymorphism could be nice (ie : a functor is pure if and only if its argument is a pure functor).

[lthls]

However this corresponds to a stricter notion of purity than the one present in this PR that does not consider divergence as a side-effect.

I took a bit of time to look at the implementation of is_nonexpansive in this PR, and I couldn't find a way to create an expression treated as pure which diverges. In particular, function/functor applications are never considered pure as far as I can tell.

Side note : we should check that this PR behaves correctly with recursive functors as they might raise exceptions at application which is a side effect.

I think that recursive functors behave the same way as non-recursive functors. In a recursive definition functors are not considered safe so they end up compiled the same way as non-recursive functors, except that they may refer to not-yet-initialised modules. But calling a function from another module (parameter or not) should never be considered pure anyway, so I don't think we need to worry about possible exceptions due to uninitialised modules.

[samsa1]

I took a bit of time to look at the implementation of is_nonexpansive in this PR, and I couldn't find a way to create an expression treated as pure which diverges. In particular, function/functor applications are never considered pure as far as I can tell.

Yes, but applying a pure functor to an argument is currently considered pure. This might lead to a divergence coming from the module language and not the core language

[samsa1]

I've been discussing pure functors (with termination) with @Drup today. He had new proposals to add to the mix :

1. define non-termination of module-expressions as UB. This is quite aggressive as a change but shifts all the complications of termination from the compiler to the user.

2. prevent applications of pure functors to themselfs functors rather than the definition. The idea is that we want to prevent the applications of F to F by checking all call-sites to F. For example we would reject examples such as F(A)(F(B)) or F(X)(F). But we still want to accept examples such as List(List(Int)).

However this seems impossible to do in practice after more thinking due to some examples that becomes difficult to detect such as :

module M (G : (S -> S) -> (S -> S)) = G(F)
module M2 = M(F)

[OlivierNicole]

1. define non-termination of module-expressions as UB.

For the record, this sets off alarm bells in my head. One of the nice things in OCaml is that it has well-defined semantics on most programs (maybe all, if you exclude primitives?), which makes it easier to reason about and debug, as put forward in the PLDI 2014 paper “Bounding Data Races in Space and Time”.