Keeping polymorphism of universally quantified fields

polymorphism
#1

I have the following code snippet:

type 'a f = 'a -> 'a

type foo = { f: 'a. 'a f }

let seqF : 'a. 'a f -> 'a f -> 'a f =
  fun f1 f2 ->
  fun a ->
    let a = f1 a in
    f2 a

let seq foo1 foo2 =
  { f = seqF foo1.f foo2.f }

and get this error at compile time:

Error: This field value has type 'b f which is less general than 'a. 'a f

Is there a way for me to keep the same level of polymorphism after having sequenced the functions.

0 Likes
#2 
let seq foo1 foo2 =
     { f = (fun x -> seqF foo1.f foo2.f x) }

I think it’s explained here:

http://caml.inria.fr/pub/docs/manual-ocaml/polymorphism.html

0 Likes
#3

I have a follow up question:

type 'a f = ('a -> 'a) option
type foo = { f: 'a. 'a f }

let seqF : 'a. 'a f -> 'a f -> 'a f =
  fun f1 f2 ->
    match f1, f2 with
    | Some f1, Some f2 ->
      Some (fun (a:'a) ->
          let a = f1 a in
          f2 a)
    | None, Some f2 -> Some (fun (a:'a) -> f2 a)
    | Some f1, None -> Some (fun (a:'a) -> f1 a)
    | _ -> None

let seq foo1 foo2 =
  { f = (fun a b -> seqF a b) foo1.f foo2.f }

I modified the type 'a f to be a function option.
I don’t understand how to tell the compiler to keep the polymorphism of the function after wrapping it inside an option.

The link was explaining that by using the fun notation we clearly indicate to the compiler that the value is a function definition. The type is not a function anymore so it looks like I can’t use eta-expansion anymore.

0 Likes
#5

No, you need all your calls under one quantifier, so foo1 foo2 within a (fun ... -> ...).

0 Likes
#6

You can write it as follows:

let seq f1 f2 =
  match f1.f, f2.f with
  | Some f1, Some f2 -> {f = Some (fun a -> f2 (f1 a)) }
  | None   , Some f2 -> {f = Some f2 }
  | Some f1, None    -> {f = Some f1 }
  | _                -> {f = None }
0 Likes