Email Gateway (Aug 19 2022 at 15:27): Email Gateway (Aug 19 2022 at 15:27):From: Peter Lammich <lammich@in.tum.de>
Hi all.
If I issue the following definition:
primrec f where "f g v (a,b) = (g v a, b)"
I get:
Type unification failed: Variable 'a::{} not of sort type
Type error in application: incompatible operand type
Operator: old.rec_prod :: ('b ⇒ 'd ⇒ ??'a) ⇒ 'b × 'd ⇒ ??'a
Operand: λa b g v. (g v a, b) ::
'b ⇒ 'd ⇒ ('a ⇒ 'b ⇒ 'c) ⇒ 'a ⇒ 'c × 'd
Although I would have expected the definition to go through. What is
going wrong here?
Email Gateway (Aug 19 2022 at 15:28):From: Lawrence Paulson <lp15@cam.ac.uk>
The error message could be more informative, but I can’t imagine why you would use primrec here. There is neither a datatype nor recursion.
Larry Paulson
Email Gateway (Aug 19 2022 at 15:28):From: Brian Huffman <huffman.brian.c@gmail.com>
The product type is certainly a datatype. I've often used primrec to
define functions over non-recursive datatypes.
Email Gateway (Aug 19 2022 at 15:28):From: Lars Noschinski <noschinl@in.tum.de>
This has nothing to do with primrec. If you inspect
term "f g v (a,b) = (g v a, b)"
or the even simpler
term "h x"
you will see that the first argument to g has the empty sort, as has x.
This is a shortcoming of our type-inference:
If the type of a variable is fully unconstrained (like the first
argument of g), the type inference fails to insert the default sort
("type", in the case of HOL) for the corresponding type variable.
The workaround is to add sufficient type annotations.
-- Lars
Last updated: Apr 23 2024 at 20:15 UTC