1
$\begingroup$

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.

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 guess this is the cause it does not pay attention to type class constraints.

What is a semantic type definition in Isabelle/HOL then? Should I use datatype for this?

$\endgroup$

1 Answer 1

1
$\begingroup$

Yes, datatype is adequate for this:

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

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

Type class prescription works on both sides of the defining equation.

$\endgroup$
1
  • $\begingroup$ Caveat: I do not see if this has an effect on later definitions. I had to use the type class prescription again when defining a function on this type. $\endgroup$
    – Gergely
    Aug 4, 2023 at 15:06

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.