## Stream: Beginner Questions

### Topic: proof that countable is linorder

#### Sophie Tourret (Oct 10 2022 at 14:36):

Hello,

I am trying to show (with Isabelle2021-1) that a countable type is a linorder type (which should follow from the fact that nat is a linorder). Since both are typeclasses, I am trying to show this using the subclass relation.

However, when I type

``````subclass (in countable) linorder
``````

I get the error:

``````Conflict of type arities for classes preorder < ord:
sum :: (countable, countable) preorder and
sum :: (finite, finite) ord
``````

There is only one instance of `sum` in countable and none in linorder. I don't understand where this error message comes from. Can someone help?

MWE (in Scratch.thy):

``````theory Scratch
imports "HOL-Library.Library"
begin

subclass (in countable) linorder

end
``````

#### Mathias Fleury (Oct 11 2022 at 15:35):

Given that countable does not entail the existence of an order (syntactically, there is no <), I am not sure what you expect to happen here exactly

#### Mathias Fleury (Oct 11 2022 at 15:37):

``````term "(x :: 'a :: {countable}) ≤ x"
(*
Type unification failed: Variable 'a::countable not of sort ord
*)
``````

#### Mathias Fleury (Oct 11 2022 at 15:45):

In slightly more words: image int are also countable, but you cannot use the same order as the one defined by default over integer. And isabelle's typeclasses to not allow two instantiations of the same operator

#### Mathias Fleury (Oct 11 2022 at 15:52):

With the following you get at least the theorems:

``````context
fixes a :: "'a :: {countable}"
begin

interpretation X: linorder where
less_eq = "λ(a::'a) b. to_nat a ≤ to_nat b" and
less = "λa b. to_nat a < to_nat b"
by unfold_locales
auto
``````

#### Manuel Eberl (Oct 12 2022 at 15:48):

Perhaps I should add that Isabelle typeclasses work like Haskell type classes: you can only have one instance per combination of type and type class, and instances are forever and unchanging. You cannot ‘delete’ or ‘locally forget’ a type class instance. If you import two theories that each have a `linorder` type class for some given type, you wil get an error.

The Isabelle `linorder` type class does not just mean that ‘there is some linear order on this type’, but rather ‘there is one canonical linear order on this type and whenever I write ≤ this is what I mean by it’.

This is the reason why e.g. there is no `order` instance for lists and products by default because there are a number of reasonable orders on this, e.g. the lexicographic order and the pointwise order.

Another unrelated limitation is that if you have a type class `a` and a type class `b` which assumes the existence of some operation `f` (as is the case here with `countable` and `linorder`), you cannot say something like ‘Every type of class `a` also has an instance of type `b` where we instantiate `f` as follows.’

That last limitation could, I think, be lifted in principle. But things being as they are, it is not possible to do this. The usual workaround is to introduce an additional typeclass `countable_linorder` that is a superclass of both `countable` and `ord` (the syntactic type class that only assumes the existence of `≤` with no laws) and that assumes that `(≤)` is simply defined in the way that follows from `countable`. Then you can show that `countable_linorder` is a subclass of `linorder`.

You will then, however, have to explicitly demand `countable_linorder` in many places where you would normally only require `countable`, and you will have to instantiate `countable_linorder` for every concrete type where you want to make use of this `linorder` class that comes out of countability.

Last updated: Dec 07 2023 at 20:16 UTC