Can you pass types as arguments in OCaml like one does in Coq (or are type variables usually decided by type inference)?

I am trying to make comparisons with Coq just to learn more about functional programming and proof assistants (and their relationships and difference).

The simplest example is the polymorphic identity function. In Coq it is easy to pass types as actual arguments and show them explicitly in function e.g.

  Check fun {T: Type} (x:T) => x.


fun (T : Type) (x : T) => x
     : forall T : Type, T -> T


  Definition id (T:Type) (x:T) := x.
  Check id.


     : forall T : Type, T -> T

and I can call it with

  Compute id nat 1.


     = 1
     : nat

Notice that I passed nat as an argument. Can this be done in Ocaml or does type inference the only way to determine the values of type variables like 'a? (my guess is that one cannot pass them since I’ve never seen them and I read somewhere that the type system of OCaml is decidable so my guess is that there is no need…)

It is possible (but a bit heavy) to pass “types as arguments” by using first-class modules:

# module type T = sig type t end;;
module type T = sig type t end
# let id (type a) (module M : T with type t = a) (x : a) = x;;
val id : (module T with type t = 'a) -> 'a -> 'a = <fun>

You can call it with

# id (module (struct type t = int end)) 1;;
- : int = 1

Note that this kind of code is made both more convenient and more powerful by the ongoing work in Modular explicits by mrmr1993 · Pull Request #9187 · ocaml/ocaml · GitHub


I have never used Coq so I am not absolutely certain what question the OP is asking, but GADTs can also carry along with them arbitrary types:

type _ alternatives =
  | First: int alternatives
  | Second: float alternatives

let do_it (type t) (alts: t alternatives) (t:t) =
  match alts with | First -> Printf.printf "First: %d\n" t
                  | Second -> Printf.printf "Second: %f\n" t

let () = do_it First 50