Stream: Coq users

Topic: ✔ Recursive class.

Ignat Insarov (Oct 01 2021 at 08:33):

I want to write a recursive polymorphic function that does one thing for an argument of type ℙ, another thing for an argument of any type other than a function, and the third thing for function arguments. How can I do this?

Ignat Insarov (Oct 01 2021 at 08:35):

I thought of two ways:

1. Make a type class with overlapping instances. _(Haskell would let me do this.)_
2. Make a polymorphic function that takes a type and case splits on it.

Nothing works so far.

Ignat Insarov (Oct 01 2021 at 08:35):

The type class approach does not work because Coq does not understand that I want it to try the most specific instance first. Since a function type is also a type, Coq always chooses the most general instance.

Ignat Insarov (Oct 01 2021 at 08:36):

The polymorphic function approach does not work because Coq does not let me match on a type:

Recursive definition on "Type"
which should be a recursive inductive type.

Ignat Insarov (Oct 01 2021 at 08:36):

How can I solve this?

Gaëtan Gilbert (Oct 01 2021 at 08:39):

Ignat Insarov said:

The type class approach does not work because Coq does not understand that I want it to try the most specific instance first. Since a function type is also a type, Coq always chooses the most general instance.

adjust the instance priority

Guillaume Melquiond (Oct 01 2021 at 08:39):

Reify your type. Instead of having a function foo: Type -> U, have a function foo: forall {t:T}, eval t -> U with eval: T -> Type. Then, you can match on t.

Ignat Insarov (Oct 01 2021 at 08:48):

I see, so fixed points require inductive arguments, but _«flat»_ definitions do not, so I can define a flat eval. Nice!

Ignat Insarov (Oct 01 2021 at 08:49):

But how do I pattern match a function type?

Gaëtan Gilbert (Oct 01 2021 at 08:50):

T is supposed to be an inductive

Ignat Insarov (Oct 01 2021 at 08:50):

This does not work:

Variant reified_type := reified_any_type | reified_property | reified_function.

Definition reify_type: Type → reified_type := λ type, match type with ℙ => reified_property | x → y => reified_function end.

Here reify_type is what Guillaume calls eval.

Ignat Insarov (Oct 01 2021 at 08:50):

Error: Invalid notation for pattern.

Théo Winterhalter (Oct 01 2021 at 08:51):

What he calls eval is the other way around.

Théo Winterhalter (Oct 01 2021 at 08:51):

eval : T -> Type

Gaëtan Gilbert (Oct 01 2021 at 08:52):

instead of having something like

Inductive is_type : Type -> Type :=
| fun_is_type : forall A B, is_type (A -> B)
...
Definition my_thing T {t : is_type T} := match t with ...

you would do

Inductive type :=
| fun_type : forall A B : Type, type
...
Definition eval t := match t with
| fun_type A B => A -> B
| ...

Ignat Insarov (Oct 01 2021 at 08:52):

Ah, so T is reified_type?

Ignat Insarov (Oct 01 2021 at 08:52):

I see.

Ignat Insarov (Oct 01 2021 at 08:59):

So, it is more like dematerialize_type, or whatever the antonym of _«reify»_ is.

Ignat Insarov (Oct 01 2021 at 10:18):

Reification works in that it allows me to case split on the type once. However, I still cannot recurse on it the way I wanted to since the function arrow is not an inductive constructor. But the class based approach also works, as Gaëtan suggested. Thanks to everyone!

Notification Bot (Oct 01 2021 at 10:36):

Ignat Insarov has marked this topic as resolved.

Last updated: Sep 30 2023 at 17:01 UTC