CODEWITHSUNDEEP
ocamlabstract-data-type
Charlie Parker
Charlie Parker

Reputation: 5231

What does it mean to define a type with no constructors in OCaml?

I saw this OCaml code in the Coq codebase:

type ('a, 'b, 'c) tag

which seems we create the type tag that takes three type arguments 'a, 'b, 'c but has no constructors…? So how do we even construct values for this type?

Upvotes: 1

Views: 256

Answers (1)

kopecs
kopecs

Reputation: 1731

Because this is in reference to a specification in an interface, this simply means that constructors are not exposed as part of the interface.

However, this does not mean there is no way to obtain a value of this type. In this case, it appears the primary (possibly only; I am unfamiliar with Coq's API) way to obtain a value of this type would be to use get_arg_tag from the containing module.

Upvotes: 2

Related Questions