Stream: Beginner Questions

Topic: Class constraints ignored in type synonym definition

view this post on Zulip Gergely Buday (Aug 02 2023 at 10:28):

My class constraint is ignored in a type synonym definition: for

type_synonym 'value myTypeOperator = "'value::group_add"

I get 

Ignoring sort constraints in type variables(s): "'value"
in type abbreviation "myTypeOperator

The examples I have found in the codebase were using such constraints on the Right Hand Side:

Isabelle2022/src/HOL/Isar_Examples/Hoare_Ex.thy:type_synonym 'a time = "\<lparr>time :: nat, \<dots> :: 'a\<rparr>"
Isabelle2022/src/HOL/TLA/Intensional.thy:type_synonym ('w,'a) expr = "'w \<Rightarrow> 'a"   (* intention: 'w::world, 'a::type *)
afp-2023-03-16/thys/Binomial-Heaps/BinomialHeap.thy:type_synonym ('e, 'a) BinomialQueue_inv = "('e, 'a::linorder) BinomialTree list"
afp-2023-03-16/thys/Binomial-Heaps/SkewBinomialHeap.thy:type_synonym ('e, 'a) SkewBinomialQueue = "('e, 'a::linorder) SkewBinomialTree list"
afp-2023-03-16/thys/Locally-Nameless-Sigma/preliminary/FMap.thy:type_synonym ('a, 'b) fmap = "('a :: finite) \<rightharpoonup> 'b" (infixl "-~>" 50)
afp-2023-03-16/thys/Strong_Security/Types.thy:type_synonym ('id, 'd) DomainAssignment = "'id \<Rightarrow> 'd::order"
afp-2023-03-16/thys/Differential_Dynamic_Logic/Denotational_Semantics.thy:type_synonym 'a Rvec = "real^('a::finite)"

so I wonder what the problem is here.

view this post on Zulip Gergely Buday (Aug 03 2023 at 08:45):

I am not sure if this is the cause of ignoring type class prescriptions, but Section 5.12.2 of the Isabelle/Isar Reference Manual says that

Unlike the semantic type definitions in Isabelle/HOL, type synonyms are merely syntactic abbreviations without any logical significance.

I don't know if datatype is a semantic definition but it works:

datatype ('v::group_add) myTypeOperator = MyTyOp 'v

datatype ('v) myTypeOperator2 = MyTyOp2 "'v::group_add"

to add type class prescription on both sides of the defining equation.

view this post on Zulip Mathias Fleury (Aug 03 2023 at 08:47):

type synonyms means type_synonym…

view this post on Zulip Mathias Fleury (Aug 03 2023 at 08:47):

not datatype

view this post on Zulip Gergely Buday (Aug 03 2023 at 09:01):

If type_synonym does not accept type class constraints, I use another type definition command, for my purposes it does not matter which I use.

view this post on Zulip Wolfgang Jeltsch (Aug 03 2023 at 11:05):

For wrapper types I would use typedef in the form typedef … = "UNIV :: … set". The proof obligation this creates should be dischargable with ...

view this post on Zulip Wolfgang Jeltsch (Aug 03 2023 at 13:03):

And when working with types defined by typedef, I exclusively use lift_definition and the transfer proof methods, as opposed to using and reasoning with the Abs and Rep functions typedef creates.

Last updated: Apr 28 2024 at 16:17 UTC