What is an Isabelle/HOL subtype? What Isar commands produce subtypes?

Question

I'd like to know about Isabelle/HOL subtypes. I explain a little about why it's important to me in my partial answer to my last SO question:

Trying to Treat Type Classes and Sub-types Like Sets and Subsets

Basically, I only have one type, so it might be useful to me if I could exploit the power of HOL types through subtypes.

I've done searches in the Isabelle documentation, on the Web, and on the Isabelle mailing lists. The word "subtype" is used, though not much, and it seems like it's not a super important part of the Isabelle vocabulary.

Partly, I'd just like to know how to use the word "subtype" correctly. I don't want to be calling something a subtype in Isabelle that's not a subtype.

According to the Wiki, subtyping is language specific:

https://en.wikipedia.org/wiki/Subtyping

Important last part; the commands please

Can someone give me a list of the Isar commands that create Isar subtypes? I'm investigating typedef, as explained in the question linked to above. I'm inclined to call that subtyping, but isar-ref.pdf doesn't use "subtype" when explaining the command.

If there are other ways to create Isabelle/HOL subtypes, I'd like to know.

Orrery

Answer 1

Isabelle/HOL does not have subtypes in the sense of substitutability. This means that if you need a value of type a, then you have to provide a value of type a - you cannot get along with a different type b. In particular, Isabelle does not have the notion of subtype where the values of the subtype satisfy some additional property.

There are some ways to emulate certain aspects of subtypes, and this is where the notion subtype is used:

1. Substitution of type parameters allows you to sometimes create the illusion of subtyping. The record package uses this to extend records such that one can use an extended record q in place of the non-extended record r. Internally, the additional fields of q are stuffed into an additional type parameter of a generalisation of r's record type. Technically, there's no subtype polymorphism going on; consequently, the order of extending records matters.

2. typedef introduces a new type t whose type universe is a non-empty subset of the values of some existing HOL type a. Sometimes, this is referred to as t being a subtype of a, but you do not get substitutability. You always have to explicitly mention the embedding morphism Rep_t when you want to use a value of t as one of a. It does not matter whether you define your type with typedef or by some other means, any injective function can serve as such a coercion.

3. Coercive subtyping as described in the Isabelle Reference Manual (section 12.4) makes Isabelle infer and insert such coercions automatically. This only works both the type and the subtype are type constructors without arguments. Use declare [[coercion_enabled]] to enable coercive subtyping and register your coercion function with declare [[coercion Rep_t]]. Thus, you do not have to insert the embedding functions yourself.

Summerville

Andreas, another example of where I get a foggy idea of what I need and want, and the developers have thought about and implemented the idea in a mature form a long time ago. Sec.12.4 uses the phrase "coercive subtyping". "Subtype" could be defined specifically for how it's used in Isabelle/HOL... When a word is used in docs, but never defined, and has a non-standard meaning, I can spin my wheels... But strike those 2 last sentences. I see now that "coercive typing" says it all, it's even addressed in the Wiki; my awareness has been raised. @Lars, thanks for clarifying "write" as "insert". – Orrery