Which is less generic than

Learning
1

Hello! I’m trying to get the types work for a task interface where a task is a function. But a task can depend on the output of other tasks so I want to pass in a fetch function. But tasks can return different types of values, so I’m trying to pass in a fetch function that is polymorphic but running into a type error. Below is the code I’m trying to implement, any ideas?

module K : sig
  type 'a t

  val int : string -> int t
  val to_string : 'a t -> string
end = struct
  type 'a t = string

  let int s = s
  let to_string t = t
end

type 'v task = { run : 'r. ('r K.t -> 'r) -> 'v }

let task = { run = (fun fetch -> fetch (K.int "foo")) }

Error:

69 | let task = { run = (fun fetch -> fetch (K.int "foo")) }
                        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: This field value has type (int K.t -> int) -> int
       which is less general than 'r. ('r K.t -> 'r) -> 'a
2

Your type has the quantifier scoping over the return type, ∀r.((r K.t → r) → v), which means that the type of run is polymorphic.

But you want only the type of run’s argument to be polymorphic, (∀r.(r K.t → r)) → v, which you can achieve with a record for the argument, as follows:

type fetcher = { fetch : 'r. 'r K.t -> 'r }
type 'v task = { run : fetcher -> 'v }
let task = { run = fun {fetch} -> fetch (K.int "foo")}

or, more simply:

type fetcher = { fetch : 'r. 'r K.t -> 'r }
let task {fetch} = fetch (K.int "foo")
5 Likes
3

AHHH of course, so obvious. Thank you so much for the helpful and fast response!

4

I have a follow up question: Given the answer above, is it possible to implement the following function?


  module Tasks = struct
    type t = { get : 'v. M.State.t -> 'v M.k -> 'v Task.t option M.C.t }
  end

The idea is to have some store of tasks which can all be heterogeneous in type and get one, if it exists. I am pretty sure I know how I can implement this with GADTs, but is it possible to have an implementation that is as naive as a function? Like the following:

let tasks =
  {
    get =
      (function
      | a -> Some { run = (fun _ -> 10) }
      | b -> Some { run = (fun _ -> "hi") }
      | _ -> None);
  }