Implicit functors should be pure

[lpw25]

Implicit functors should be pure and they should be aliasable.

[bluddy]

Why is this the case? Is it because their application is hard to predict?

[let-def]

And because we might want to share instances for performance reason.

E.g. if you use Show_list(Show_int) a lot, it's better to hoist the instance as early as possible.
Same for coercions.

If they are pure, sharing and reordering is always correct.

[lpw25]

Those are both good reasons, but my main motivation is to safely support patterns like inheritance. See section 3.3 of the modular implicits paper for some examples and explanation.

[gadmm]

In Section 3.3, you write:

In order to maintain coherence we must require that all implicit functors be pure. [...] We ensure
this using the standard OCaml value restriction. This is a very conservative approximation of purity, but we do not expect it to be too restrictive in practice.

I would like to offer a use-case for implicit functors which are pure but do not satisfy the value restriction. Essentially, I would like to rewrite types along equality types, doing some computation which ideally would be optimised away (but the front-end cannot know that). By simplifying this idea we get to the following canonical example:

type (_,_) eq = Refl : ('a,'a) eq

module type EQ = sig
  type a
  type b
  val eq : (a,b) eq
end

module Refl (T : sig type t end) : EQ with type a = T.t
                                       and type b = T.t
  = struct
  type a = T.t
  type b = T.t
  let eq = Refl
end

(* simple example *)
implicit module List_eq {T:EQ} : EQ with type a = T.a list
                                     and type b = T.b list
  = struct
  type a = T.a list
  type b = T.b list
  let eq : (a,b) eq =
    let lift (type a) (type b) (Refl : (a,b) eq) : (a list, b list) eq = Refl in
    lift T.eq
end

(* more general *)
module Lift_eq (M : sig type 'a t end) = struct
  let cast (type a) (type b) (Refl : (a,b) eq)
        (module A : EQ with type a = a M.t
                        and type b = a M.t)
    = (module A : EQ with type a = a M.t
                      and type b = b M.t)

  implicit module Make {T:EQ} : EQ with type a = T.a M.t
                                    and type b = T.b M.t
    = struct
    module R = Refl (struct type t = T.a M.t end)

    include (val cast T.eq (module R))
  end
end

Currently, this compiles but side-effecting functors are allowed as well. It would be nice to keep this use-case. I am using something along these lines (especially the second form) for a prototype resource-management library which uses modular implicits and abstract type equalities non-trivially. Alternatively, a workaround is welcome.

[gadmm]

To spin it more dramatically: if the criterion is the value restriction, are there other implicit functors EQ^n -> EQ than constants and projections?

[lpw25]

I believe that you could instead write something like:

(* simple example *)
implicit module List_eq {T:EQ} : EQ with type a = T.a list
                                     and type b = T.b list
  = struct
  type a = T.a list
  type b = T.b list
  let eq : (a,b) eq = let Refl = T.eq in Refl
end

although this may not work in the prototype because it is still based on a quite old version of OCaml.

[gadmm]

Yes, I was doing that in my original code without implicits, and I had to change it for the reason you said. This still does not satisfy the value restriction, or did I miss something?

[lpw25]

This still does not satisfy the value restriction, or did I miss something?

It should do. There are no function calls, uses of mutable fields, etc. so it should be fine.

[gadmm]

Ok, thanks. The form that interests me is the second one with a functor application and include(val cast...). The casts look like they can be replaced with semantic values (so far), but I am more concerned about the functor application. In my use-case I cannot get rid of it.

[lpw25]

Since functors with implicit parameters would have been made pure we can allow applications of such functors to count as values. So if you can make the parameters of the functor that you hope to apply be implicit (you can still pass the arguments explicitly you don't need to use the search) then it should all work.

Ideally, I'd like to make all applicative functors pure, or at least provide a syntax for pure non-implicit functors, since its weird to have the implicitness of the parameter decide whether the functor is pure, in which case you could just use one of those for your functor.

[gadmm]

I see, thanks, there is a chance that this could be a workaround. My use of type equalities appears to be very simple indeed.

There's indeed a broader issue of effects in functors which I imagine you have to address in your effect type system. It reminds me of similar issues with linearity, I hope we will have occasions to further chat about this.