Email Gateway (Apr 28 2021 at 09:41): Email Gateway (Apr 28 2021 at 09:41):From: Stepan Holub <holub@karlin.mff.cuni.cz>
Dear all,
can anybody explain why the error
"Term to be evaluated contains free dictionaries"
appears in the following minimal example:
================
theory Scratch
imports Main
begin
context ord
begin
fun foo :: "'a list ⇒ bool"
where "foo xs = True"
end
value "foo Nil"
"Term to be evaluated contains free dictionaries"
end
=============
Thanks.
Stepan
Email Gateway (Apr 28 2021 at 09:48):From: Jakub Kądziołka <kuba@kadziolka.net>
A dictionary is the implicit structure used to pass around constants and
functions defined by a type class. For `ord', the dictionary would
contain (<) and (<=).
A dictionary is free if the corresponding type variable is free. So, the
error essentially says "The value of this term depends on what ordered
type you instantiate it to, and you haven't specified that". In your
simple example, the result would be the same either way, but Isabelle
doesn't have a way of handling this special case.
Regards,
Jakub Kądziołka
Email Gateway (Apr 28 2021 at 10:06):From: Stepan Holub <holub@karlin.mff.cuni.cz>
Thank you. This makes sense, except:
the term is evaluated successfully for
value "foo xs"
where the type of xs is inferred as 'a list.
The same inference is made for Nil.
The difference in the result is therefore still not clear to me.
Stepan
Email Gateway (Apr 28 2021 at 11:08):From: Manuel Eberl <eberlm@in.tum.de>
The dictionary error that you saw comes from the code generator, which
is the evaluation backend that the value command normally uses.
When you write "foo xs", there is a free variable in the term, so code
generation cannot work at all. Therefore, the "value" command falls back
to one of its other evaluators (probably "nbe", normalisation by
evaluation). There is also a simplifier-backed backend.
You can tell the value command precisely which evaluator to use:
value [code] "foo Nil" (* free dictionary error *)
value [nbe] "foo Nil" (* True *)
value [simp] "foo Nil" (* True *)
By the way, when you do something like
value "Nil"
you see the error
Wellsortedness error:
Type 'a not of sort term_of
Cannot derive subsort relation {} < term_of
This is also an error caused by polymorphism in the term to be
evaluated, but this time, the problem is not that there are dictionaries
from type classes flying around, but simply that Isabelle does not know
how to convert the result (which is an ML term) back into a HOL term
(this only works for concrete types that are instances of the "term_of"
class).
Manuel
smime.p7s
Last updated: Jul 15 2022 at 23:21 UTC