 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

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.