Natural transformation for free selective applicative

Learning
,
1

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
  end
  
  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
      end
    end
    
    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) -> 
          Select
            ( map x ~f:Either.(map ~f) 
            , F.map 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 ~g:Fn.id)

        | 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
            ( select (map x ~f) (map y ~f:g )
            , F.map 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) -> S2.select (run_select t x) (t.apply y)
      end 
    end
    
  
  end    
end

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?

Thanks,

Michael

1 Like
2

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