Stream: Coq users

Topic: ✔ Record type scope

James Wood (Feb 28 2022 at 09:44):

The following code fails because it interprets + as nat-addition rather than a sum type former. I could solve that by surrounding the expression by ( ... )%type, but is there a way I can annotate the Record declaration to do that automatically?

Record foo {A : Type} : Type := { bar : A -> Type; }.
Arguments foo A : clear implicits.

Definition add_foo {A} (X : foo A) (Y : foo A) : foo A :=
  {| bar := fun a => X.(bar) a + Y.(bar) a; |}.

Paolo Giarrusso (Feb 28 2022 at 09:48):

AFAIK not directly, because scope inference can't deal with type constructors (including functions): the scope for Type is type_scope, but the scope for A -> B is always function_scope no matter what the scope for B is. But abbreviations can save you:

Paolo Giarrusso (Feb 28 2022 at 09:49):

Record foo {A : Type} : Type := _mkFoo { bar : A -> Type; }.
Notation mkFoo bar := (_mkFoo bar%type).

Paolo Giarrusso (Feb 28 2022 at 09:53):

Or you could write a fun variant for type_scope, something like:

Notation "'funT' x .. y => t" := (fun x => .. (fun y => t%type) ..)
  (at level 200, x binder, y binder, right associativity,
  only parsing) : function_scope.

Beware that reserves funT as a keyword! The Unicode variant is less annoying here (it pairs with the stdlib's λ notation).

Notation "'λT' x .. y , t" := (fun x => .. (fun y => t%type) ..)
  (at level 200, x binder, y binder, right associativity,
  only parsing) : function_scope.

Paolo Giarrusso (Feb 28 2022 at 09:54):

I haven't done funT but I've definitely used λI (for Iris's %I)

James Wood (Feb 28 2022 at 09:57):

Ah yeah, this might do. By the way, what does function_scope provide?

Paolo Giarrusso (Feb 28 2022 at 10:00):

Uh, nothing apparently? Even coq's theories/Unicode/Utf8_core.v doesn't use it... I thought I'd followed it in the above.

Notation "'λ' x .. y , t" := (fun x => .. (fun y => t) ..)
  (at level 200, x binder, y binder, right associativity,
  format "'[  ' '[  ' 'λ'  x  ..  y ']' ,  '/' t ']'").

Paolo Giarrusso (Feb 28 2022 at 10:02):

At least Coq itself doesn't use either %.*function or function_scope in the stdlib (beyond declaring it).

Paolo Giarrusso (Feb 28 2022 at 10:07):

However, Bind Scope function_scope with Funclass. ensures it's open every time an expression is known to be a function "statically" (that is, before typechecking). Coq seems too clever here...

Paolo Giarrusso (Feb 28 2022 at 10:07):

TLDR: probably just drop : function_scope above and you're good.

Notification Bot (Feb 28 2022 at 10:49):

James Wood has marked this topic as resolved.

Gaëtan Gilbert (Feb 28 2022 at 11:10):

Can't you do Arguments Build_foo _ _%function.?

Paolo Giarrusso (Feb 28 2022 at 14:55):

@Gaëtan Gilbert that's automatic, but @James Wood would need Arguments Build_foo _ _%type. if anything, and I wouldn't expect it to work here

Paolo Giarrusso (Feb 28 2022 at 14:56):

In particular, Arguments Build_foo _ _%function. isn't equivalent to replacing `Build_foo bar baz with Build_foo bar baz%function (at least for general scopes, dunno if function is special).

Paolo Giarrusso (Feb 28 2022 at 14:58):

When you call foo (bar args), and foo has some scope argument, that only affects how bar is interpreted — it's then up to bar to decide how to interpret args.

Paolo Giarrusso (Feb 28 2022 at 14:59):

Instead, in foo (bar args)%some_scope, some_scope affects all of bar args.

Paolo Giarrusso (Feb 28 2022 at 15:00):

but in the original case, you're using foo (fun ... => body), and fun doesn't set a scope for body.

Last updated: Oct 03 2023 at 20:01 UTC