Implementing instances for inductive types

Stream: new members

[Shubham Kumar 🦀 (he/him)]

How does one implement Eq instance for an inductive type

inductive Token : Type :=
  | Id : Token -- | Terminal Symbol
  | Ident : String -> Token -- | Token contains a String Identifier
  | Number : Int -> Token -- | Token contains an Int value
  | If_Symbol : Token
  | Then_Symbol : Token
deriving Eq

deriving Eq doesn't work

default handlers have not been implemented yet, class: 'Eq' types: [Token]

[Yaël Dillies]

docs#Eq is defined for every type already

[Shubham Kumar 🦀 (he/him)]

so deriving Eq should not show that error message, is it an incorrect way to use it?

[Yaël Dillies]

Eq is not a typeclass, so it doesn't make any sense to use deriving Eq

[Shubham Kumar 🦀 (he/him)]

oh ok, so I can just use = and it would implicitly search for the instance?

[Yaël Dillies]

There is no instance because there is no typeclass!

[Yaël Dillies]

Have you clicked here? :point_right: docs#Eq :point_left:

[Yaël Dillies]

You will see what Eq is, and how it is not the same as Haskell's Eq (which is more like docs#BEq instead)

[Eric Wieser]

The answer here is possibly that you meant deriving BEq or deriving DecidableEq

[Shubham Kumar 🦀 (he/him)]

ok, soEq is an inductive type which consumes 2 Types and returns a Prop while BEq is typeclass which defines the beq function that consumes 2 Types (but of the same universe because it is a typeclass in that universe? I don't know why Type u is specified) and returns a Bool Type which is an inductive Type

[Yaël Dillies]

No, it doesn't consume two types. Instead it consumes one type α and two elements of that type

[Shubham Kumar 🦀 (he/him)]

Thanks! I didn't have (still don't) any understanding of Eq then

[Yaël Dillies]

When I write 0 = 1, this is notation for @Eq Nat 0 1. So α := Nat

[Shubham Kumar 🦀 (he/him)]

oh not that part, I don't know what is the difference between Eq and BEq I was assuming both are typeclasses, which it isn't and I don't have an image of how they are related

[Yaël Dillies]

The truth is that they are not

[Yaël Dillies]

Eq is mathematical equality. BEq is just a typeclass that gives you access to the == notation

[Yaël Dillies]

If you want to state that == corresponds to mathematical equality (namely ∀ a b, a = b ↔ a == b), you use docs#LawfulBEq

[Shubham Kumar 🦀 (he/him)]

Interesting, thanks you have given me a lot to think about.

For now, I think deriving BEq should work and probably I don't need to derive an instance

[Shubham Kumar 🦀 (he/him)]

another stupid question, even after deriving DecidableEq it seems like Token doesn't have the DecidableEq instance

def pSym {s : Type} [DecidableEq s] (a : s) : Parser s s :=
  Parser.P (λ inp =>
    match inp with
    | s :: ss => if a = s then [(s, ss)] else []
    | _ => [])

inductive Token : Type :=
  | Id : Token -- | Terminal Symbol
  | Ident : String -> Token -- | Token contains a String Identifier
  | Number : Nat -> Token -- | Token contains an Int value
  | If_Symbol : Token
  | Then_Symbol : Token
deriving DecidableEq, BEq

def pIdent := pSym Id

error

error: typeclass instance problem is stuck, it is often due to metavariables
  DecidableEq ?m.4178

[Henrik Böving]

You want to write pSym Token.Id

[Shubham Kumar 🦀 (he/him)]

Thanks! I knew it was something stupid

[Shubham Kumar 🦀 (he/him)]

so in the previously stated messages (not sure if it would be clear) I was trying to get to a place where after defining my token Inductive type I can define a concrete equality where Token.Id = Token.Ident "" should be true but the automatic derivation leads to false

inductive Token : Type :=
  | Id : Token -- | Terminal Symbol
  | Ident : String -> Token -- | Token contains a String Identifier
  | Number : Nat -> Token -- | Token contains an Int value
  | If_Symbol : Token
  | Then_Symbol : Token
deriving DecidableEq, BEq

#eval Token.Id = Token.Ident "" -- | should be true

image showing false
Screenshot-from-2024-03-27-13-26-46.png

How to I go about defining equality if I want it to be true?

[Markus Schmaus]

The direct answer to your question is docs#Quotient. Given an equivalence relation, this creates a new type for which this equivalence relation defines Eq equality. But If your goal is simply Token.Id = Token.Ideny "", the simpler solution would be to define the former in terms of the latter.

[Kyle Miller]

Make sure not to derive both DecidableEq and BEq. You get BEq for free from DecidableEq.

And also Markus's suggestion is the right one for overriding the equality for a type. Quotients are the way you create a type from another type with a looser Eq. (This is not done with typeclasses.) I suppose you could define BEq on the original type to correspond exactly to the Eq on the quotient type — I'm not sure how much people have explored that design pattern.

[Shubham Kumar 🦀 (he/him)]

I would like to do the simple thing but first maybe waste time on understanding what quotient is, I found something related to quotient types but if there are easier ways to approach this I'll be happy to look looking at Wikipedia.

Thanks for the help!