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.