Why can't I write a function that doesn't take a type argument besides Set, Prop, or Type?

Question

I'm trying to make a "formal" model of a C++ domain specific language. One thing the language has is a notion of a "reducer" where you take an array and add up all the elements. I don't want to write all of the C++ type system, I want to focus only on the DSL, so I am trying to make a sort of placeholder for a C++ type. Here is my first attempt.

(* I don't want to write a type checker for C++ so I just say it's some "thing" *)
Definition CppType := string.

Inductive Reducer : Type :=
| Sum
| Prod
| CustomReducer (t : CppType) (init : t) (join : t -> t -> t)
.

But I get an error that says “The term “t” has type “CppType” which should be Set, Prop or Type.”

The idea here is it’s just that the join can be any C++ type, because that's a simpler model than specifying exactly what the type needs to look like (which is rather complex). I could instead write this:

Inductive Reducer : Type :=
| Sum
| Prod
| CustomReducer (T : Type) (init : T) (join : T -> T -> T)
.

but that seems far too powerful of a notion, since that can be any Coq type, but I want to specify instead it's just a C++ type, to indicate that we're not concerned with that in this specification.

Answer 1

The problem you encounter is that you want CppType to express a C++ type… but Coq only knows its own types. More precisely, whatever comes to the right of : must be a Coq type, ie something of type Prop, Set or Type (as you noticed). So what you need is some way to make the C++ types and the Coq types interact.

One possible way is to axiomatize the C++ type structure, doing something like the following

Axiom CppType : Type.
Axiom El : CppType -> Type.

This makes it explicit that you are not describing the C++ type system, only taking it as a primitive. El stands for "elements", and is the customary name for such functions which take some inhabitant t of a datatype supposed to represent a type, and compute a real Type from it, corresponding to the type of elements of t. You can then amend your reducer to be of type

| CustomReducer (t : CppType) (init : El t) (join : El t -> El t -> El t)

This is somewhat similar to you second attempt, but now you are correctly quantifying over only C++ types. Moreover, if you later on want to describe more precisely what a CppType can be, you can amend El accordingly, to compute a Coq type from a C++ type, for instance you would probably want to define El CppInt to be nat.

This first solution is quite nice and simple, however, it means that you rely on Coq's type system, which might work differently than C++'s. I understand that you do not want to describe all of that in Coq as it is orthogonal to your purpose. But you could also axiomatize it, say do something like the following:

Axiom CppType : Type.
Axiom CppFun : CppType -> CppType -> CppType.
Axiom CppProg : Type.
Axiom CppTyping : CppProg -> CppType -> Prop.

Inductive Reducer : Type :=
| Sum : Reducer
| Prod : Reducer
| CustomReducer (t : CppType) (init : CppProg) (join : CppProg) :
    CppTyping init t -> CppTyping join (CppFun t (CppFun t t)) -> Reducer
.

This is more precise than the first solution, as it does not assume than you can translate C++'s type system to Coq in a faithful way. However, it is probably quite heavier… At the very least, you will probably want to have a notation for CppTyping that looks like p : t.

Answer 2

Your issue lies in that having a Coq term like t : "hello world" doesn't make sense. If you do want to absolutely no type checking for your CppTypes, you can definite a sort of composition, like this:

Definition CppType := string.
Definition TypedCppObj (t : CppType) := CppData (*phantom type for book keeping purposes only *)

Inductive Reducer : Type :=
| Sum
| Prod
| CustomReducer (t : CppType) (init : TypedCppObj t) (join : TypedCppObj (t ++ "->" ++ t ++ "->" ++ t )
.

But at that point, it's not that much more difficult to do at least a little bit of the type checking. Something like this may be reasonable to do:

Definition CppBaseType := string.
Inductive  CppType : Type :=
| CppObj (t : CppBaseType)
| CppBinFun (t1 : CppBaseType) (t2 : CppBaseType) (tr : CppBaseType)
.
Inductive Reducer : Type :=
| Sum
| Prod
| CustomReducer
  (t : CppBaseType) (init : CppType) (join : CppType) (v : Var)
  (initOK : init = CppData t)
  (joinOK : join = CppBinFun t t t)
.