Re: [isabelle] Extra type variables, type classes and locales
Quoting Christoph Feller <c_feller at informatik.uni-kl.de>:
I have with a hidden extra type variable again and again I have no
clue what exactly went wrong. I've made a small example:
class testC = type +
fixes from_nat :: "nat => 'a"
and to_nat :: "'a => nat"
locale Test =
fixes dummy :: "'a::testC"
assumes dd: "ALL z::'a::testC. to_nat z ~= 0"
definition ftest :: "nat => 'a list" where "ftest n == [from_nat n]"
inductive test::"nat => nat => bool"
"((ftest a)::'a list) = ((ftest b)::'a list) ==> test a b"
I thought the locale not only fixed dummy but also 'a so that it isn't
necessarily an extra type variable in the inductive definition. Am I
wrong or is there another mistake in my example?
Thanks in advance,
I think you are right to expect this to work.
When you define a locale like "Test", the locale package defines a
predicate of the same name, which encodes all of the locale
assumptions. Usually the predicate takes all of the parameters from
"fixes" declarations as arguments. However, locales like your "Test"
example require some special treatment. For example:
Test TYPE(?'a::testC) == ALL z::?'a::testC. to_nat z ~= 0
As you can see, the locale predicate "Test" does not depend on the
locale parameter "dummy", but it still depends on the type variable 'a.
I would have expected the locale package to use the same trick to
encode functions like your "test". That is, an extra hidden
TYPE(?'a::testC) parameter should be added to make the type checker
happy. I would consider this to be a bug in the locale implementation.
By the way, the following definition *does* work inside the locale.
Just like your inductive definition of "test", it uses type variable
'a on the right-hand side, but no type variable appears in the type of
the constant. The only difference is that this one also uses the
locale constant "dummy" on the right-hand side.
test2 :: "nat => bool"
"test2 n = (((ftest n) :: 'a list) = [dummy])"
This archive was generated by a fusion of
Pipermail (Mailman edition) and