Conflating Types and their String Names · Coq users

So this may not be possible but I am hopeful.
I would like to take in a string (given in a module but that seems unimportant) and have Coq recognize the type which has the name given by that string. The specific code at hand is:

Inductive wrapper :=
  | build_wrapper : forall ty : Type, (ty = m.idc) -> wrapper.

Here the equality ty = m.idc is what's at question, and idc is the string coming from a module m, but this equality cannot work because on one side is a Type and on the other, a String. Ideally I need something that takes in m.idc and translates it into the type which has the name m.idc. I have been playing with MetaCoq for a bit to see if anything works there, but you have to get inside the Template Monad to do anything and then you're stuck in there. I've also found Ltac2.Ident.ident_of_string but that is a simple conversion between two different String types.

Paolo Giarrusso (Jul 21 2023 at 16:17):

this might be doable in a "metafunction" (Ltac/elpi/...) — that only runs before or during typechecking, but not in a Coq function of type "string" -> Type.

But if you can list the types of interest there's a chance — you can _match_ on the string, or you can encode a metafunction using a typeclass:

From Coq Require Import String.
Class StringToType (s : string) (X : Type) := {}.
#[global] Hint Mode StringToType + - : typeclass_instances.
Definition stringToType (s : string) {X} {H : StringToType s X} := X.

(* then instances you need. Feel free to generate them. *)
#[global] Instance: StringToType "unit" unit := {}.
#[global] Instance: StringToType "nat" nat := {}.

Eval compute in stringToType "nat".
Eval compute in stringToType "unit".

(*
     = nat
     : Type
     = ()%type
     : Type
 *)

Paolo Giarrusso (Jul 21 2023 at 16:20):

actually, if you can do what you want in Ltac (say, via Ltac2), you could write a generic instance of StringToType.

_However_, that's still not a real function that computes a type at runtime, it just looks very close and will work in many scenarios (with some experience using typeclasses): it's still running during typechecking.

Angelo Taranto (Jul 21 2023 at 18:56):

Interesting...I expect my module to be used by an end-user, who defines m.idc themselves (as well as the rest of the module variables). I can have defining an instance of this type-class be part of the experience, but I was hoping to have it be automated so that a single wrapper definition can handle any Type. If the only way to do that would be writing an Ltac, I will learn how to do so.

Paolo Giarrusso (Jul 21 2023 at 19:16):

why can't the user just pass the Type, instead of its string name? The former would also work for types like list a or Γ ⊢ a : A or <insert almost any Coq type that isn't a single identifier>

Paolo Giarrusso (Jul 21 2023 at 19:17):

(handling arbitrary expressions in strings requires a Coq parser, but the only correct one is Coq itself)

Angelo Taranto (Jul 21 2023 at 19:24):

The Type itself is constructed by a MetaCoq function which adds a constructor (or several) to a known type. The module is basically all the inputs to that MetaCoq function wrapped up. The user interacts with the module and provides those inputs, the MetaCoq function is run after that on the module's variables, and one of the inputs to that module is the new name of the generated Type. So before that MetaCoq function is run, all I have access to is the user's new choice of name as a String.

Paolo Giarrusso (Jul 21 2023 at 22:33):

it's still possible there's a different solution, but the problem remains underspecified — which is okay, you asked a specific question.

I guess you want to refer to the type in the module _before_ running MetaCoq? If the users can write their code "below" the MetaCoq call, they can just refer to the type by name, and everything gets much easier honestly.

Alternatively:
TemplateCoq _could_ output an instance of the class, but here's the problem: that instance doesn't let you do much; StringToType is isomorphic to unit. You can't prove StringToType s T1 -> StringToType s T2 -> T1 = T2.

In simple cases, the module could contain a function forall (T : Type) -> a tuple of all the components that might want to use T`, and MetaCoq could "run" that function. For your concrete example:

Inductive wrapper (T : Type) :=
  | build_wrapper : forall ty : Type, (ty = T) -> wrapper.

and then pass wrapper to the module. An upside here is that ty1 = T and ty2 = T do imply ty1 = ty2.

Another potential problem is that you still know nothing about T, but MetaCoq could also pass any number of functions to your code, as long as you can represent their type. If you know MetaCoq builds a function nat -> T; if you know it builds nat -> nat {n times} -> nat -> T, you need to use dependent types more to represent this argument (but you can write this type by recursion on n).

Stream: Coq users

Topic: Conflating Types and their String Names