Stream: Coq users

Topic: ✔ Recursive class.


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Ignat Insarov (Oct 01 2021 at 08:36):

How can I solve this?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip Ignat Insarov (Oct 01 2021 at 08:49):

But how do I pattern match a function type?

view this post on Zulip Gaëtan Gilbert (Oct 01 2021 at 08:50):

T is supposed to be an inductive

view this post on Zulip 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.

view this post on Zulip Ignat Insarov (Oct 01 2021 at 08:50):

Error: Invalid notation for pattern.

view this post on Zulip Théo Winterhalter (Oct 01 2021 at 08:51):

What he calls eval is the other way around.

view this post on Zulip Théo Winterhalter (Oct 01 2021 at 08:51):

eval : T -> Type

view this post on Zulip 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
| ...

view this post on Zulip Ignat Insarov (Oct 01 2021 at 08:52):

Ah, so T is reified_type?

view this post on Zulip Ignat Insarov (Oct 01 2021 at 08:52):

I see.

view this post on Zulip Ignat Insarov (Oct 01 2021 at 08:59):

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

view this post on Zulip 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!

view this post on Zulip Notification Bot (Oct 01 2021 at 10:36):

Ignat Insarov has marked this topic as resolved.


Last updated: Jan 27 2023 at 02:04 UTC