Natural transformation for free selective applicative

I’ve been looking at the Haskell prototype and OCaml implementation of selective applicative functors and started writing Selective.Rigid.Free in OCaml.

In the Haskell code there is a function runSelect which defines a natural transformation from Select f to g given a natural transformation from f to g. The Haskell definition is as follows:

-- | Given a natural transformation from @f@ to @g@, this gives a canonical
-- natural transformation from @Select f@ to @g@.
runSelect :: Selective g => (forall x. f x -> g x) -> Select f a -> g a
runSelect _ (Pure a)     = pure a
runSelect t (Select x y) = select (runSelect t x) (t y)

I think I’ve managed to implement this in OCaml with the following:

module Selective = struct
  module type S = sig 
    include Applicative.S
    val select : ('a,'b) Either.t t -> f:('a -> 'b ) t -> 'b t
  module Free = struct 
    module type S = sig 
      include S 
      module F :  Functor.S
      module Transform : functor (S2 : S) -> sig
        type nt = { apply : 'a. 'a F.t -> 'a S2.t; }
        val run_select : nt -> 'a t -> 'a S2.t
    module Make_free(F: Functor.S) : S with module F := F = struct
      type 'a t = 
        | Pure : 'a -> 'a t 
        | Select : ('a,'b) Either.t t * ('a -> 'b) F.t -> 'b t

      let rec map : type a b.  a t -> f:(a -> b) -> b t = fun x ~f ->
        match x with 
        | Pure a -> Pure (f a)
        | Select(x,y) -> 
            ( map x ~f:Either.(map ~f) 
            , y ~f:Fn.(map ~f) 

      let rec select : type a b. (a,b) Either.t t -> f:(a -> b) t -> b t = fun x ~f ->
        match f with 
        | Pure y -> 
            map x ~f:Either.(either ~f:y

        | Select(y,z) ->
          let f x = Either.(map ~f:second x)
          and g y = fun a -> Either.bimap y ~f:(fun b -> b,a) ~g:((|>) a)
          and h z = Fn.uncurry z in 
            ( select (map x ~f) (map y ~f:g )
            , z ~f:h

      let return x = Pure x

      let apply : type a b. a t -> f:(a -> b) t -> b t = fun x ~f ->
        select (map f ~f:Either.first) (map x ~f:((|>)))
      module Transform(S2 : S) = struct
        type nt = { apply : 'a. 'a F.t -> 'a S2.t }
        let rec run_select : type a. nt -> a t -> a S2.t = fun t -> function
            | Pure a -> S2.return a 
            | Select(x,y) -> (run_select t x) (t.apply y)

If I leave of the signature from Make_free this works fine. However, when I add ... : S with module F := F ... the type checker complains:

Error: Signature mismatch

At position module Transform(S2 : ) …
The module ‘F’ is required but not provided

I’ve tried without destructive substitution too but can’t figure it out. Can anyone see what I’m doing wrong?



1 Like

It is a shadowing problem.
Your free module type requires Transform to work on any selective input, but the one that you defined only work on free_selective .
You may want to use other names than S as names for module types.

1 Like