The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Yann,

 

I would suggest you follow Adam’s advice.

 

Quickly: I don’t think you can create a function which maps types to nat in Gallina (Coq’s term language). I am not a mathematician, so I can’t give you the exact reason, but I think this Wikipedia is in the right direction: https://en.wikipedia.org/wiki/Parametricity.

 

You can use match only to distinguish between different constructors of inductive types. You can match on types, but (afaik) this makes most sense if these types depend on an inductive type like the length of a dependently typed vector. If the term you match on doesn’t have anything inductive in its type, you can have only one pattern. It might still make sense to match a type without inductive parameters to give names to generic type parameters for use in the result term. But matching with a type which doesn’t have any parameters at all is a nop.

 

When I want to achieve the kind of functionality you describe, I create an inductive type, which has separate constructors for separate types like nat or bool. Then it is trivial to write such a function.

 

Please also note, that it would be possible to write such a function in Ltac, Coq’s proof automation language.

 

Regarding types and values:

Definition type1 (t:Type) :=

match t with

| bool => 0 (* doesn’t make much sense, see below *)

end.

 

Definition type2 {t:Type} (val:t) :=

match t with

| bool => 0

end.

 

type1 accepts a type, while type 2 accepts a value (the t in curly braces is an implicit parameter whose value is derived from the type of val).

Please note that both functions return 0 for whatever type or value you give them. if you look at the print, you see that the match goes away, because bool doesn’t have any inductive parameters.

Compute type1 nat.

Compute type2 1.

Print type1.

Print type2.

 

Best regards,

 

Michael

 

From: coq-club-request AT inria.fr [mailto:coq-club-request AT inria.fr] On Behalf Of Mwyann
Sent: Tuesday, June 21, 2016 2:51 PM
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Dependant Match Example

 

Dear Michael,

 

Thanks a lot for your fast and complete answer. Indeed, I think I’m still confused with types and values. What I’m really looking after is to match the type of a value, for example we would like to make this work as you would imagine:

 

Inductive some_type := A | B | C.

 

Definition type (t:Type): nat :=

match t with

| bool => 0

| nat => 1 (* error: redundant *)

| some_type => 2

| _ => 99 (* any other type *)

end.

 

Compute type 1. (* would return “1” as “nat” *)

 

I don’t know what mechanism we can use to determine the type of a term (apart from the internal Coq’s type checking).

 

Do you know if any lectures on the subject exists somewhere? (especially courses that contains examples, which help learning efficiently).

Best regards,

 

Yann

 

2016-06-21 10:48 GMT+02:00 Soegtrop, Michael <michael.soegtrop AT intel.com>:

Dear Yann,

 

 [...]

Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928