Type hierarchy definition in Isabelle

Question

I would like to build a kind of type hierarchy in Isabelle:

B is of type A  ( B::A )

C and D are of type of B   (C,D ::B) 

E and F are of type of C     (E,F ::C)

What is the best way to encode this in Isabelle? Is there any direct way to define this hierarchy, or I need a workaround. Where should I look?

PS: Suppose A..F are all abstract and some functions are defined over each type)

Thanks

Answer 1

(1st Note: In my opinion, as you've been using it, the word "abstract" doesn't have clear meaning. The Isabelle keywords used to define types can be used to define, as I see it, either abstract or concrete types, or types that can be considered both, such as 'a list.)

(2nd Note: Here, I take into consideration your comparisons, in other questions, to object-oriented programming. As to programming languages and languages of logic, it should be noted, I am a mere observer.)

Terms have types, and types have types (or sorts, so they say)

For myself, it all becomes a big blur, and in my mind I stop clearly differentiating between terms and types, so answers such as Rene Thiemann's help to bring that back to mind.

Still, not knowing much, I can simply consider your phrase "type hierarchy" to be synonymous with "type class hierarchy", and further to be synonymous with "sort hierarchy". That allows me to happily provide an answer to your question, though acceptance by others could be precarious.

Of course, in the Isabelle vocabulary, types and sorts aren't synonymous, but in Isabelle/HOL, they are inseparable because every HOL term has a sort. (A dangerous claim, since type prop is used in HOL, and maybe I still don't understand what the empty sort is.):

• Section 3.3.4 Type classes, sorts and arities, page 54
  • isabelle.in.tum.de/website-Isabelle2014/dist/Isabelle2014/doc/isar-ref.pdf#page.54
• The difference between the empty sort and 'a::type
  • stackoverflow.com/questions/25811989/whats-the-difference-between-the-empty-sort-a-and-a-sort-of-type-a

Inheritance, Isabelle's got it

It's through locales that Isabelle provides inheritance (among other ways?), where a type class is (or includes), among other things, a locale:

• Section 3 Type classes as locales, page 7, classes.pdf
  • http://isabelle.in.tum.de/website-Isabelle2014/dist/Isabelle2014/doc/classes.pdf#page.7
• Section 3 Import, page 5, locales.pdf
  • Quote: "With locales, this kind of inheritance is achieved through import of locales".
  • http://isabelle.in.tum.de/website-Isabelle2014/dist/Isabelle2014/doc/locales.pdf#page.5

I create 5 type classes which meet your requirements, at least simplistically. Each one has its own identity function. The + symbol is the magical inheritance symbol.

declare [[show_sorts, show_consts]]
(*The 5 type classes.*)
  class cA =
    fixes idA :: "'a => 'a"
    assumes idA_is_id: "idA x = x"
  class cB = cA +
    fixes idB :: "'a => 'a"
    assumes idB_is_id: "idB x = x"
  class cC = cB +
    fixes idC :: "'a => 'a"
    assumes idC_is_id: "idC x = x"
  class cD = cB +
    fixes idD :: "'a => 'a"
    assumes idD_is_id: "idD x = x"
  class cE = cC +
    fixes idE :: "'a => 'a"
    assumes idE_is_id: "idE x = x"
  class cF = cC +
    fixes idF :: "'a => 'a"
    assumes idF_is_id: "idF x = x"

It works:

(*Any of type class cB, cC, cD, and cF can be used where cA can be used.*)
  term "idA (x::'a::cA)"
  term "idA (x::'a::cB)"
  term "idA (x::'a::cC)"
  term "idA (x::'a::cD)"
  term "idA (x::'a::cE)"
  term "idA (x::'a::cF)"

More examples of the inheritance:

(*Use of idC shows that cE inherited all of what's in cC.*)
  term "idC :: ('a::cC => 'a::cC)"
  term "idC :: ('a::cE => 'a::cE)"
  term "idC (x::'a::cE)"
(*But here, there's a type sort clash, because cC didn't inherit from cE. *)
  term "idE :: ('a::cC) => ('a::cC)"

Now, add some concreteness by instantiating nat as type class cF:

(*It took me over an hour to see I was using 'idA_cA' instead of 'idA_nat'.
  99% of the battle can be learning the syntax.*)
instantiation nat :: "{cF}"
begin
  definition idA_nat :: "nat => nat" where "idA_nat == id"
  definition idB_nat :: "nat => nat" where "idB_nat == id"
  definition idC_nat :: "nat => nat" where "idC_nat == id"
  definition idF_nat :: "nat => nat" where "idF_nat == id"
instance (*proof. Use 'proof' and see 4 subgoals: the need for 4 id functions.*)
  by(default, auto simp add: idA_nat_def idB_nat_def idC_nat_def idF_nat_def)
end

(*When I instantiated nat as cF, I had to instantiate nat as cA, cB, and cC,
  because I had not previously done so. Normally, you would be adding useful 
 'fixes' and 'assumes' with each type class, and proving useful theorems about
 them.*)
  value "idA (0::nat)"
  value "idB (0::nat)"
  value "idC (0::nat)"
  value "idF (0::nat)"
  
(*You have to show that a type satisfies all of the 'fixes' and 'assumes'
  of a type class. But additional proved theorems, you get those for free.
  That's the great benefit of type classes. You may have 20 types that
  you instantiate as a type class, but you only have to prove 'extraneous' 
  theorems once, that being for the type class, based on the 'fixes' and
  'assumes' (and other things defined with other keywords).*)

I still try, periodically, to learn how to use the Isabelle vocabulary correctly. So, I was looking at the keyword subclass:

• subclass, page 97 isar-ref.pdf
  • isabelle.in.tum.de/website-Isabelle2014/dist/Isabelle2014/doc/isar-ref.pdf#page.97

I might as well prove that cF is a subclass of cA, to make a point:

context cF
begin
  subclass cA ..
end

Is cA a subclass of cF or vice-versa? Well, I wouldn't have already committed if I hadn't of replaced c and d in the definition for subclass in isar-ref.pdf, to find out.

It's not object-oriented classes, but then C++ doesn't compare to ML for functional programming

The nature of being exposed to languages, whether logic or programming, is you find out that none of them give you everything, and so you end up wanting everything that all of them give you separately.

You may be able to define objects in C++ easily, but try to define algebraic data types in C++.

You kind of can:

• Wiki Algebraic Data Type
  • en.wikipedia.org/wiki/Algebraic_data_type
• Open and Efficient Type Switch for C++
  • parasol.tamu.edu/~yuriys/pm/

But it's not ridiculously easy like with Isabelle/HOL, which is similar to Haskell, and the pattern matching abilities of the workarounds I've tried is not even close.

But, hey, I'm all for the eventual convergence of all these things we want.

Answer 2

At least in Isabelle/HOL this is not directly possible, since there is a strict separation between terms and types where :: takes a term on the left-hand side and a typ on the right-hand side. So, when writing B :: A then B is a term and A is a type. Then, it is impossible to write C :: B.

I'm not sure, but perhaps your setup can directly be modeled within Isabelle/ZF.

Concerning workarounds, you can exchange types by sets and use membership : instead of ::. Then you can write

context
  fixes A B C D E F
  assumes 
  "B : A" 
  "C : B" "D : B" 
  "E : C" "F : C"
begin
 ...
end

but then you get no support from the type-checker, and A has type 'a set set set.

Hope this helps.