CODEWITHSUNDEEP
isabelle
Denis
Denis

Reputation: 1271

How to use type's argument as a value in a function?

I'm trying to define a simple type system with a custom set type:

notation bot ("⊥")

typedef 'a myset = "UNIV :: 'a fset option set" ..

copy_bnf 'a myset

setup_lifting type_definition_myset

lift_definition myset :: "'a fset ⇒ 'a myset" is Some .

instantiation myset :: (type) bot
begin
lift_definition bot_myset :: "'a myset" is None .
instance ..
end

free_constructors case_myset for
  myset
| "⊥ :: 'a myset"
  apply (simp_all add: bot_myset_def myset_def)
  apply (metis Rep_myset_inverse option.collapse)
  apply (metis Abs_myset_inverse iso_tuple_UNIV_I option.inject)
  apply (metis Abs_myset_inverse iso_tuple_UNIV_I option.distinct(1))
  done

lift_definition map_myset :: "('a ⇒ 'b) ⇒ 'a myset ⇒ 'b myset" 
  is "map_option ∘ fimage" .

Type system has integer, real and set types:

datatype type =
  IType
| RType
| SType type

Also there are 3 kinds of values:

datatype val =
  IVal int
| RVal real
| SVal "val myset"

I need to define a function type_of which determines a type of a value:

fun elem_type :: "val myset ⇒ type" and
    type_of :: "val ⇒ type" where
  "elem_type xs = ???"
| "type_of (IVal x) = IType"
| "type_of (RVal x) = RType"
| "type_of (SVal x) = SType (elem_type x)"

value "type_of (SVal (myset {|IVal 1, IVal 2|}))"
value "type_of (SVal (myset {|RVal 1, RVal 2|}))"
value "type_of (SVal (myset {|SVal (myset {|IVal 1|})|}))"

Could you suggest how to get element type of myset?

Upvotes: 0

Views: 100

Answers (1)

Manuel Eberl
Manuel Eberl

Reputation: 8278

I would say there is a fundamental problem with your modelling: your type_of function seems to suggest that every value has exactly one type.

In his comment, Lars has already pointed out that there are some values (e.g. a set containing both integers and real values) that you would probably consider to be invalid and that therefore have no type at all. That you could handle by returning ‘undefined’ or something like that, perhaps, and introduce some kind of additional ‘well-formedness’ predicate for values, but I'm not sure that's a good idea.

Another problem is that there are some values that are polymorphic, i.e. that have more than one type, in a sense: For instance, what should your type_of function return for the empty set, i.e. SVal (myset {|})? There are infinitely many reasonable types that this thing could have.

The usual approach to handle this is to introduce a typing relation instead of a typing function so that each value can have several types – or none at all. Usually, you do this with the inductive command, defining an inductive predicate like has_type v t which states that the value v has the type t (or ‘can be given the type t’ in case of polymorphism).

Also, on an unrelated note, I am not sure why you define a new type and use copy_bnf, free_constructors etc. I don't know what you're planning to do but my guess would be that whatever it is does probably not get easier with that typedef; it will probably just cause some annoyances.

Upvotes: 2

Related Questions