Stream: math-comp users

Topic: finmap: Canonical choiceType for {fset K}

Ana de Almeida Borges (Nov 26 2020 at 23:17):

I expected that if K : choiceType then {fset K} could be interpreted as a choiceType. At least that's what I thought the following line of the finmap library was doing:

Canonical fset_choiceType := Eval hnf in ChoiceType {fset K} fset_choiceMixin.

However:

From mathcomp Require Import all_ssreflect finmap.

Variable K : choiceType.
Variable s : {fset K}.
Variable f : choiceType -> bool.

Fail Check (f s).
(* The command has indeed failed with message:
The term "s" has type "{fset K}" while it is expected to have type
 "choiceType". *)

More or less by chance I discovered that Check (f (fset_sub_choiceType s)). works, while Check (f (fset_choiceType s)). does not.

I'm confused. What is going on?

Emilio Jesús Gallego Arias (Nov 26 2020 at 23:20):

Not sure I follow, s is not a choiceType but an element of the type, so indeed Coq can't type that term

Emilio Jesús Gallego Arias (Nov 26 2020 at 23:21):

Check (f {fset K}). works.

Emilio Jesús Gallego Arias (Nov 26 2020 at 23:22):

We all get confused by types that are elements of others types often, at least I do :)

Ana de Almeida Borges (Nov 26 2020 at 23:24):

You are right, I messed up my example. Should have written Definition s := {fset K}, or used it directly. But over here Check (f {fset K}) fails with the same error:

The term "{fset K}" has type "Type" while it is expected to have type
 "choiceType".

Ana de Almeida Borges (Nov 26 2020 at 23:26):

I have finmap 1.5.0. Is this possibly a bug?

Cyril Cohen (Nov 27 2020 at 01:31):

Actually, with Variable s : {fset K}, both the coercion from s to Type and {fset K} itself are canonically choice types, which is not the same has having type choiceType. You can recover the canonical instance using [choiceType of _], and both f [choiceType of s] and f [choiceType of {fset K}] should work.

Ana de Almeida Borges (Nov 27 2020 at 10:39):

Great, that works! But it seems that I don't understand what it means for something to be canonically a choiceType. I thought it meant that if a choiceType was needed to correctly type an expression, then the choiceType instance would be chosen automatically. And in my previous experience with Coq similar things have happened with a number of canonical things. Or maybe it was a coincidence and the inference happened because of other reasons?

Paolo Giarrusso (Nov 27 2020 at 10:57):

the inference did happen because of canonical structures, but there are specific rules

Paolo Giarrusso (Nov 27 2020 at 10:57):

IIUC, for f : {X : choiceType} -> X -> bool, such inference would happen.

Paolo Giarrusso (Nov 27 2020 at 10:58):

but (once you show coercions) this type will be sth like f : {X : choiceType} -> projectType X -> bool (dunno the actual name)

Paolo Giarrusso (Nov 27 2020 at 10:59):

and what Canonical Structure inference does, at its root, is that they solve equations of form projectType ?X = {fset K} by filling in the right ?X.

Ana de Almeida Borges (Nov 27 2020 at 11:01):

Wait, what is projectType?

Paolo Giarrusso (Nov 27 2020 at 11:01):

But going from {fset K} to [choiceType of {fset K}] is not an equation of that form.

Paolo Giarrusso (Nov 27 2020 at 11:02):

sorry I don’t know the actual name, but I expect sth like projectType : {choiceType} -> Type

Ana de Almeida Borges (Nov 27 2020 at 11:02):

Oh right, sorry. So it's the coercion from choiceType to Type.

Paolo Giarrusso (Nov 27 2020 at 11:04):

(the name seems sort https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/choice.v#L279, but using Set Printing Coercion when printing types using it will be more helpful)

Paolo Giarrusso (Nov 27 2020 at 11:06):

I’m no math-comp expert, but I was pointed to https://hal.inria.fr/hal-00816703v1/document to understand CS basics a while ago, and it has a better version of what I was saying

Christian Doczkal (Nov 27 2020 at 11:31):

Yes, the convention is to define the coercion inside a Module (named after the structure) and then call it sort. So there is Finite.sort, Choice.sort etc.

Christian Doczkal (Nov 27 2020 at 11:37):

Also, it might be worthwhile to point out the reason why the type is written {fset T} rather than fset T: In order to construct the type of finite sets, one needs not only the type T but indeed its choiceType instance.
The notation {fset T} plays some trickery with phantom types to trigger canonical instance resolution for T, allowing one to write {fset nat} rather than fset nat_choiceType.

Enrico Tassi (Nov 27 2020 at 13:02):

FTR there is a, rather terse my bad, explanation of this at page 136 of https://zenodo.org/record/4282710#.X8D4MMIo-8Q

Christian Doczkal (Nov 27 2020 at 13:16):

@Enrico Tassi Terse and not exactly margin-respecting :smirk:

Enrico Tassi (Nov 27 2020 at 13:21):

My $\LaTeX$ is :pile_of_poo:

Last updated: Oct 13 2024 at 01:02 UTC