CODEWITHSUNDEEP
typeclassisabelle
Isabelle Newbie
Isabelle Newbie

Reputation: 9378

How to declare "free" instance of type class?

I'm trying to model some program analysis in Isabelle/HOL. The analysis computes values in a bounded lattice, but (for now, and for generality) I don't want to commit to any concrete lattice definition; all I care about is whether some result is bottom or not. I'm looking for a way to declare an abstract type which is an instance of Isabelle/HOL's bounded_lattice type class without committing to a concrete instance.

That is, analogously to how I could write

typedecl some_data
type_synonym my_analysis_result = "var => some_data"

where some_data is completely free, I would like to be able to write something like

typedecl "some_lattice::bounded_lattice"
type_synonym my_analysis_result = "var => some_lattice"

where some_lattice would be the "free" bounded lattice of which I require nothing except that it fulfill the lattice laws. This particular syntax is not accepted by Isabelle/HOL, and neither is something like

type_synonym my_analysis_result = "var => 'a::bounded_lattice"

I can work around this problem by defining a concrete datatype and making it an instance of bounded_lattice, but I don't see why there shouldn't be a more general way. Is there some easy (or complex) syntax to achieve what I'm doing? Do I have to (somehow, I'm not sure whether it would work) stick my entire development inside a context bounded_lattice block? Or is there some reason why it's logically OK to have fully free types via typedecl but not free types restricted by type class?

Upvotes: 1

Views: 126

Answers (1)

Andreas Lochbihler
Andreas Lochbihler

Reputation: 5058

Making an unspecified type an instance of a type class may introduce inconsistencies if the type class has contradictory assumptions. To make this axiomatic nature explicity, you have to axiomatize the instantiation. Here's an example:

typedecl some_lattice
axiomatization where some_lattice_bounded:
  "OFCLASS(some_lattice, bounded_lattice_class)"
instance some_lattice :: bounded_lattice by(rule some_lattice_bounded)

NB: A few years ago, you could have used the command arities, but this has been discontinued to emphasize the axiomatic nature of unspecified type class instantiations.

Alternatively, you could just use a type variable for the lattice. This is more flexible because you can later on instantiate the type variable if you need a concrete bounded lattice. However, you have to carry the type variable around all the time. For example,

type_synonym 'a my_analysis_result = "var => 'a"

Type synonyms with sort constraints are not supported by Isabelle (as the do not make much sense anyway). If you add the sort constraint, you will get a warning that it is going to be ignored. Whenever you need the bounded_lattice instance, type inference will add the sort constraint (or you have to mention it explicitly for the type variable).

Upvotes: 2

Related Questions