Discussion:
[isabelle] No type arity itself
(too old to reply)
Mark Wassell
2016-07-23 14:02:53 UTC
Permalink
Raw Message
Hello,

With the following:

notepad
begin
fix r::real
fix f :: "'a::euclidean_space ⇒ nat ⇒ real" and g::"'a::euclidean_space
⇒ real"

let ?P = "λb. LEAST N. ∀n≥N. dist (f b n) (g b) < r/ card Basis"
let ?Q = "Max ( ?P ` Basis)"
end

I get the error "No type arity itself :: euclidean_space" at the "let ?Q"
statement.

Can anyone tell me what 'itself' is and how to resolve this problem?

Cheers

Mark
Lars Hupel
2016-07-23 15:31:09 UTC
Permalink
Raw Message
Hi Mark,
Post by Mark Wassell
let ?P = "λb. LEAST N. ∀n≥N. dist (f b n) (g b) < r/ card Basis"
the error is in this line. Roughly speaking, the type of "Basis" is too
general: it can be an arbitrary fresh 'b::euclidean_space, not the
'a::euclidean_space you in the previous line. The reason is that you
immediately apply the "card" function to it, which is of type "'a set =>
nat". So from the outside there is no indication which type is meant.

The system "helpfully" detects these situations and introduces an
explicit type parameter disguised as a value parameter.

You can observe this parameter when you print ?P:

"λtype b. LEAST N. ∀n≥N. dist (f b n) (g b) < r / real (card Basis)"
:: "'b itself ⇒ 'a ⇒ nat"

Luckily, the solution is simple: Just give a type annotation for "Basis":

let ?P = "λb. LEAST N. ∀n≥N. dist (f b n) (g b) < r/ card (Basis::'a set)"

Cheers
Lars
Mark Wassell
2016-07-23 17:58:56 UTC
Permalink
Raw Message
Lars,

Thank you for your comprehensive answer. One small question: How do I
print ?P ?

Mark
Post by Lars Hupel
Hi Mark,
Post by Mark Wassell
let ?P = "λb. LEAST N. ∀n≥N. dist (f b n) (g b) < r/ card Basis"
the error is in this line. Roughly speaking, the type of "Basis" is too
general: it can be an arbitrary fresh 'b::euclidean_space, not the
'a::euclidean_space you in the previous line. The reason is that you
immediately apply the "card" function to it, which is of type "'a set =>
nat". So from the outside there is no indication which type is meant.
The system "helpfully" detects these situations and introduces an
explicit type parameter disguised as a value parameter.
"λtype b. LEAST N. ∀n≥N. dist (f b n) (g b) < r / real (card Basis)"
:: "'b itself ⇒ 'a ⇒ nat"
let ?P = "λb. LEAST N. ∀n≥N. dist (f b n) (g b) < r/ card (Basis::'a set)"
Cheers
Lars
Manuel Eberl
2016-07-23 18:10:16 UTC
Permalink
Raw Message
term "?P"
Post by Mark Wassell
Lars,
Thank you for your comprehensive answer. One small question: How do I
print ?P ?
Mark
Post by Lars Hupel
Hi Mark,
Post by Mark Wassell
let ?P = "λb. LEAST N. ∀n≥N. dist (f b n) (g b) < r/ card Basis"
the error is in this line. Roughly speaking, the type of "Basis" is too
general: it can be an arbitrary fresh 'b::euclidean_space, not the
'a::euclidean_space you in the previous line. The reason is that you
immediately apply the "card" function to it, which is of type "'a set =>
nat". So from the outside there is no indication which type is meant.
The system "helpfully" detects these situations and introduces an
explicit type parameter disguised as a value parameter.
"λtype b. LEAST N. ∀n≥N. dist (f b n) (g b) < r / real (card Basis)"
:: "'b itself ⇒ 'a ⇒ nat"
let ?P = "λb. LEAST N. ∀n≥N. dist (f b n) (g b) < r/ card (Basis::'a set)"
Cheers
Lars
Loading...