Re: [isabelle] Extra type variables, type classes and locales



Quoting Christoph Feller <c_feller at informatik.uni-kl.de>:

Hallo,

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"
begin

definition ftest :: "nat => 'a list" where "ftest n == [from_nat n]"

inductive test::"nat => nat => bool"
where
"((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,
Christoph

Hi Christoph,

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:

thm Test_def

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.

definition
  test2 :: "nat => bool"
where
  "test2 n = (((ftest n) :: 'a list) = [dummy])"

- Brian








This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.