Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Conflict of type arities: What are the constra...


view this post on Zulip Email Gateway (Feb 16 2021 at 12:52):

From: Peter Lammich <lammich@in.tum.de>
Hi List,

I have naively tried to define a type-class for types that have more
than one element. However, when trying to make the obvious
instantiations, I get stuck with "Conflict of type arities" error
messages. I could not find any documentation on what the restrictions
are that I'm violating here, and how they are motivated. Any pointers?

instance prod :: (not_singleton,type) not_singleton ..
instance prod :: (type,not_singleton) not_singleton

Conflict of type arities:
prod :: (type, not_singleton) not_singleton and
prod :: (not_singleton, type) not_singleton

Peter

view this post on Zulip Email Gateway (Feb 16 2021 at 13:05):

From: Tobias Nipkow <nipkow@in.tum.de>
The type system requires that your type constructor signatures satisfy a
property called coregularity. If you have two type constructor signatures
kappa :: (S1,...) C
kappa :: (T1,...) D
and D is a subclass of C then Ti must be a subsort of Si. Otherwise terms do not
have the principal types. With your two declarations you would lose the pricipal
types property.

Tobias
smime.p7s

view this post on Zulip Email Gateway (Feb 16 2021 at 14:56):

From: Jakub Kądziołka <kuba@kadziolka.net>
On Tue Feb 16, 2021 at 1:52 PM CET, Peter Lammich wrote:

Hi List,

I have naively tried to define a type-class for types that have more
than one element. However, when trying to make the obvious
instantiations, I get stuck with "Conflict of type arities" error
messages. I could not find any documentation on what the restrictions
are that I'm violating here, and how they are motivated. Any pointers?

The restriction in question is that each ground type has at most one
instance of a type class.

instance prod :: (not_singleton,type) not_singleton ..
instance prod :: (type,not_singleton) not_singleton

In your example, a product of two non-singleton types would apply to
both instances.

The motivation for this restriction is that if your typeclass defines a
constant, then the overlapping instances would constitute potentially
contradictory definitions.

Regards,
Jakub Kądziołka

view this post on Zulip Email Gateway (Feb 17 2021 at 00:48):

From: Jeremy Dawson <Jeremy.Dawson@anu.edu.au>
the way I have understood this - correct me if I am wrong - is that to
prove that ('a, 'b) tycon is in some type class, the system needs to
know unambiguously what type classes 'a amd 'b have to be in - there is
no backtracking / trying multiple possibilities - presumably for
efficiency reasons

Jeremy


Last updated: Dec 05 2021 at 22:18 UTC