Questions tagged [type-class]

A type class is a type system construct that supports ad hoc polymorphism. (from Wikipedia)

Filter by
Sorted by
Tagged with
1 vote
1 answer

Lean 4 exercise: Why can't I write this function definition inside an instance declaration?

In Lean 4.3.0, I'm solving an exercise from section 4.5 "Standard Classes" of the excellent book "Functional Programming in Lean". Given the structure ...
Adam Dingle's user avatar
1 vote
1 answer

Type class constaint is ignored in type synonym definition

My class constraint is ignored in a type synonym definition: for type_synonym 'value myTypeOperator = "'value::group_add" I get ...
Gergely's user avatar
  • 299
3 votes
0 answers

Coq Typeclass on Functions Gets Confused by Equality

I was trying to use typeclasses to generalize the different notions of homomorphisms, but I’ve run into an annoying issue. Consider this code which demonstrates the issue: ...
sudgy's user avatar
  • 193
6 votes
2 answers

Defining essentially unique objects with typeclasses

I noticed that in Lean, the localization of rings (which is unique up to isomorphism) is defined as a predicate is_localization. I am not an expert in Lean, and I'm ...
Trebor's user avatar
  • 3,718
3 votes
2 answers

Multiplicity of implicit type arguments in interfaces

I have the following state monad in Idris 2: record State (s : Type) (a : Type) where constructor MkState run : s -> (s, a) and I'm trying to define ...
ionchy's user avatar
  • 1,026
5 votes
1 answer

How to rename a type class operator in a subclass in Isabelle/HOL?

I am trying to define a hierarchy of type classes with binary operations, in which the base class defines a binary operation binop and then each class ...
tinlyx's user avatar
  • 1,906
16 votes
1 answer

Extends vs including a typeclass argument

In the Lean mathlib, I see some places where a typeclass argument is included in a class definition, such as locally_finite_order. In other places, I see the "<...
Bolton Bailey's user avatar