Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] type classes without class parameters


view this post on Zulip Email Gateway (Aug 19 2022 at 11:22):

From: Christian Sternagel <c.sternagel@gmail.com>
Dear all,

is it possible to use type classes without any class parameters (i.e.,
fixed constants)?

For example, something like

class infinite =
assumes infinite: "infinite (UNIV::'a set)"

but then the resulting type of the class predicate is

term class.infinite
:: "'a itself ⇒ bool

I'm not sure whether this would make sense at all. My initial thought
was to replace assumptions like

assumes "infinite (UNIV :: 'a)"

by "'a :: infinite" in appropriate places.

cheers

chris

view this post on Zulip Email Gateway (Aug 19 2022 at 11:22):

From: Brian Huffman <huffman.brian.c@gmail.com>
On Jul 25, 2013 9:30 AM, "Christian Sternagel" <c.sternagel@gmail.com>
wrote:

Dear all,

is it possible to use type classes without any class parameters (i.e.,
fixed constants)?

For example, something like

class infinite =
assumes infinite: "infinite (UNIV::'a set)"

Yes, that is certainly possible. See for example class "finite" from the
standard libraries.

The problem with a type class for infinite types is that you can't quite
define the instances you want. For example, 'a*'b is infinite if either 'a
OR 'b is infinite, but you can't express this with an instance declaration.


Last updated: Mar 29 2024 at 04:18 UTC