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.
output
fun (T : Type) (x : T) => x
: forall T : Type, T -> T
or
Definition id (T:Type) (x:T) := x.
Check id.
output:
id
: forall T : Type, T -> T
and I can call it with
Compute id nat 1.
output
= 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
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