How can I fake existential types in Isabelle/HOL?

Question

Consider the following Isabelle/HOL definition of a simple process language:

typedecl channel

datatype process = Put channel char process | Get "char ⇒ process" | Stop

This languages supports sending and receiving of characters via channels.

Now I’d like to have typed channels. The channel type should have the type of values it can transport as a parameter:

typedecl 'a channel

The Put and Get data constructors should have the following (polymorphic) types:

Put :: "['a channel, 'a, process] ⇒ process"
Get :: "['a channel, 'a ⇒ process] ⇒ process"

However, this requires support for existential quantification in data types, which Isabelle/HOL doesn’t have.

I tried to fake existential quantification and came up with the following attempt:

typedecl put
axiomatization put :: "['a channel, 'a] ⇒ put" where
  put_inject: "put a x = put b y ⟷ a = b ∧ x = y"

bnf_axiomatization 'r get
axiomatization get :: "['a channel, 'a ⇒ 'r] ⇒ 'r get" where
  get_inject: "get a f = get b g ⟷ a = b ∧ f = g"

datatype process = Put put process | Get "process get" | Stop

Unfortunately, this results in the following error message:

Type definition with open dependencies, use "typedef (overloaded)" or enable configuration option "typedef_overloaded" in the context.
  Type:  process
  Deps:
  map_get(process.process_IITN_process
          ⇒ (process_pre_process_bdT + process_pre_process_bdT process_pre_process) set ⇒ bool,
           (process_pre_process_bdT + process_pre_process_bdT process_pre_process) set ⇒ bool),
  bd_get,
  set_get(process.process_IITN_process
          ⇒ (process_pre_process_bdT + process_pre_process_bdT process_pre_process) set ⇒ bool)
The error(s) above occurred in typedef "process"

Is my attempt reasonable, and, if yes, how can I solve this problem? Is there a better solution?

I discovered meanwhile that the existence of that injective function get makes the get type a non-bounded functor which contradicts the statement that it is a bounded natural functor (BNF). Thus this code should introduce logical inconsistency. However, that should be fixable by bounding the cardinality of 'a, for example by requiring that 'a is an instance of countable. — Wolfgang Jeltsch

Andreas Lochbihler Andreas Lochbihler · Accepted Answer · 2018-08-03T17:50:54

Indeed, the axiom for get is inconsistent with the bnf_axiomatization. However, if you restrict yourself to countable types 'a, then such a type exists. As soon as you fix such a cardinality bound, you do not even have to restort to axiomatization. Existential types can then be emulated within HOL using encoding and decoding functions into/from a universal domain.

For example, for countable types, the natural numbers can be used as the universal domain. This has been used, e.g., in Imperative_HOL to model a heap that can store typed values, see the paper from 2008. Huffman has done something similar for HOLCF, Isabelle's domain theory library.

With such an encoding in place, you'd construct the datatype of processes using untyped channels and then create a type-safe view on the datatype using the encoding and decoding functions as necessary.

How can I fake existential types in Isabelle/HOL?

1 Answers