Email Gateway (Aug 22 2022 at 17:18): Email Gateway (Aug 22 2022 at 17:18):From: Lars Hupel <hupel@in.tum.de>
Dear BNF developers,
I'm looking for some information about the way the BNF package treats
sort constraints. This is going to be a footnote in a paper, maybe a bit
more.
Consider this typedef:
typedef (overloaded) 'a::plus id = "UNIV :: 'a set" by auto
(Please ignore for a moment that the sort constraint is entirely
unnecessary here.)
Observation #1:
"copy_bnf 'a id" fails with tactic errors and a THM exception. Should
this produce a better error message?
Observation #2:
"copy_bnf (dead 'a :: plus) id" gives a better error message, namely "No
live variables".
At this point I'm assuming that "copy_bnf" can't deal with sort constraints.
So let's try with raw "bnf".
Observation #3:
Some setup:
lift_definition map_id :: "('a::plus ⇒ 'b::plus) ⇒ 'a id ⇒ 'b id" is "λf
x. f x" .
lift_definition set_id :: "'a::plus id ⇒ 'a set" is "λx. {x}" .
bnf "'a::plus id"
bnf "'a id"
Both produce identical proof obligations. First subgoal after applying
"rule ext":
"x" does not have any sort constraints. So it is not provable (?).
Observation #4:
I can define
datatype ('a::plus) id = Id 'a
just fine, but "map_id" does not have any sort constraints (whereas "Id"
and "case_id" have them).
Could somebody shed some light onto how this works? I looked at some of
the papers but didn't find anything.
Cheers
Lars
Email Gateway (Aug 22 2022 at 17:18):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Hi Lars,
Could somebody shed some light onto how this works? I looked at some of
the papers but didn't find anything.
I can answer Observation 4, which involves some of my code.
BNF type variables may not have sort constraints. "map_id" is part of the BNF structure, so it accordingly doesn't have sort constraints. More high-level theorems and constants are declared with the sort constraints. To overgeneralize a bit, Dmitriy's low-level BNF code doesn't like sort constraints, whereas my higher-level "(co)datatype" code copes with them to the extent possible. In the code, you'll see this by grepping for "unsorted_As" in "bnf_fp_def_sugar.ML".
I presume there's no deep reason for not supporting syntactic type class constraints in BNFs. It would complicate the composition operators for sure, and in a bunch of places we'd have to discharge 0 goals arising from syntactic type class instantiations. If you're up for putting in the effort, we won't stop you.
Incidentally, what is the motivation for your example? Is your application related to item 5 in the "Known Bugs and Limitations" of the "datatypes" document?
Cheers,
Jasmin
Email Gateway (Aug 22 2022 at 17:19):From: Lars Hupel <hupel@in.tum.de>
Hi Jasmin,
BNF type variables may not have sort constraints. "map_id" is part of
the BNF structure, so it accordingly doesn't have sort constraints.
More high-level theorems and constants are declared with the sort
constraints. To overgeneralize a bit, Dmitriy's low-level BNF code
doesn't like sort constraints, whereas my higher-level "(co)datatype"
code copes with them to the extent possible. In the code, you'll see
this by grepping for "unsorted_As" in "bnf_fp_def_sugar.ML".
that sounds basically like what I guessed from my observations. Thanks
for the clarification!
Incidentally, what is the motivation for your example? Is your
application related to item 5 in the "Known Bugs and Limitations" of
the "datatypes" document?
I don't intend to use this in any way. I'm merely trying to "tie up
loose ends":
My dictionary construction will just ignore sort constraints from data
constructors, and I was trying to figure out to what extent they might
be introduced in datatypes, e.g. by having a constrained BNF through
which recursion occurs.
The "meta-theorem" I am aiming for is that by dropping the sort
constraints you'll still end up with exactly the same datatype; i.e., I
want to argue that not supporting constraints in constructors is not a
problem because I can always ask the user to remove the constraints.
NB, because you mentioned "limitation 5": The fact that the overloaded 0
is a constructor for "nat" is the bane of my existence. It messes with
so many things and it is surprising that it works at all :-)
Cheers
Lars
Email Gateway (Aug 22 2022 at 17:19):From: Dmitriy Traytel <traytel@inf.ethz.ch>
Hi Lars,
let me refine Jasmin's anwer.
Live BNF type variables may not have sort constraints.
This is inherent: live variables indicate where we may recurse through. Imagine a BNF "'a :: foo F" with 'a live. Then we should be able to define:
datatype X = N | C "X F"
which in turn would require X to be an instance foo. Suddenly the datatype command would need to instantiate arbitrary type classes simultaneously with defining the type, which sounds quite ambitious even for syntactic type classes (e.g., one might get the "wrong" instance).
In contrast, dead BNF type variables may carry sort constraints. Consider e.g.,
datatype (dead 'a::plus, 'b) X = N 'b | C 'a "('a, 'b) X"
term map_X
where the first type argument of X in map_X has the sort constraint.
Sometimes one can even use the sort constraints on dead type variables to prove that some type is a BNF. My favorite example that uses this trick are arity-correct first-order terms:
declare [[typedef_overloaded]]
class arity =
fixes arity :: "'a ⇒ nat"
instantiation unit :: arity begin
definition arity_unit :: "unit ⇒ nat" where "arity_unit x = 0"
instance proof qed
typedef (overloaded) ('c :: arity, 'ty) comb (infixr "$" 65) =
"{(s :: 'c, Ts :: 'ty list). arity s = length Ts}"
morphisms Rep_comb comb
by (auto intro!: exI[of _ "replicate _ undefined"])
lift_bnf (no_warn_wits) (dead 'c :: arity, 'ty) comb by auto
setup_lifting type_definition_comb
lift_definition "fun" :: "'c :: arity $ 'ty ⇒ 'c" is fst .
lift_definition "args" :: "'c :: arity $ 'ty ⇒ 'ty list" is snd .
datatype ('x, 'c :: arity) "term" = Var 'x | App "'c $ ('x, 'c) term"
Dmitriy
PS: For sure, copy_bnf should emit a proper failure instead of the tactic failure in "observation 1". I will have a look eventually.
Last updated: Apr 19 2024 at 20:15 UTC