Typeclass constraints

Stream: new members

[Shubham Kumar 🦀 (he/him)]

I am trying to convert a parser combinator tutorial in lean4 the following haskell code has Eq as the typeclass constraint passed as an argument is there a way to write an equivalent in lean4?

pSym :: Eq s ⇒ s → Parser s s
pSym a = P (λinp → case inp of
(s : ss) | x ≡ a → [(s, ss)]
5
otherwise → [ ]
)

in lean

def pSym (a : Eq s) : s -> Parser s s :=
  Parser.P (λ inp =>
    match inp with
    | s :: ss => if Eq.refl a s then [(s, ss)] else []
    | _ => [])

but this is incorrect, the error is

error: type expected, got
  (Eq s : ?m.911 → Prop)

[Yaël Dillies]

What's the type of s in the Haskell code?

[Shubham Kumar 🦀 (he/him)]

There isn't, I think to make it generic

[Yaël Dillies]

Are you sure s isn't the type?

[Shubham Kumar 🦀 (he/him)]

it is but there is no concrete type

[Yaël Dillies]

... in which case you can just remove that Eq s argument since the Lean type s will automatically have access to = notation (docs#Eq is defined for all types)

[Shubham Kumar 🦀 (he/him)]

Ok but pSym in the haskell code consumes a type with identifier a and returns a function of type s -> Parser s s if I remove Eq s then I just pass a without any explicit types?

[Shubham Kumar 🦀 (he/him)]

something like this

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

[Yaël Dillies]

The Lean version should be of the form pSym {s : Type} : s → Parser s s (for some definition of Parser)

[Yaël Dillies]

Note that the Haskell code is using s for two different things!

[Yaël Dillies]

s refers to both a type and an element of that type

[Shubham Kumar 🦀 (he/him)]

Oh thanks!

[Shubham Kumar 🦀 (he/him)]

do we also need to define an instance of Decidable? because it is unable to generate Decidable (a = s) instance

[Timo Carlin-Burns]

You might need [DecidableEq s] for the if

[Yaël Dillies]

Just assume [DecidableEq s]

[Shubham Kumar 🦀 (he/him)]

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

is the above code correct? if I place [DecidableEq s] before the {s : Type} I get the same error, right now I am getting a different error where lean compiler errors out with

error: type mismatch
  Parser.P fun inp =>
    match inp with
    | s_1 :: ss => if a = s_1 then [(s_1, ss)] else []
    | x => []
has type
  Parser s s : Type
but is expected to have type
  s → Parser s s : Type

[Yaël Dillies]

What's Parser.P? Can you provide a #mwe ?

[Shubham Kumar 🦀 (he/him)]

yep, just a sec

[Yaël Dillies]

Wait, actually, the error is easy to spot

[Yaël Dillies]

You meant either (a : s) : Parser s s := or : s -> Parser s s := fun a ↦, but not both

[Shubham Kumar 🦀 (he/him)]

inductive Parser (s t : Type u) : Type u :=
  | P : ParserType s t -> Parser s t

this is how I have defined it, in the tutorial

newtype Parser s t = P ([s ] → [(t, [s ])])

[Shubham Kumar 🦀 (he/him)]

Yaël Dillies said:

You meant either (a : s) : Parser s s := or : s -> Parser s s := fun a ↦, but not both

I wanted the former, usually in haskell or ML like languages one can assume both, I am not sure that is correct in lean

[Shubham Kumar 🦀 (he/him)]

ParserType is just abbrev ParserType s t := List s -> List (Prod t (List s))

[Shubham Kumar 🦀 (he/him)]

is there something wrong in the assumptions I've made?

[Yaël Dillies]

Yaël Dillies said:

You meant either (a : s) : Parser s s := or : s -> Parser s s := fun a ↦, but not both

Did you understand my message above? :point_up:

[Shubham Kumar 🦀 (he/him)]

The only difference I know is that it's syntactic sugar but I'm sure it's wrong and I have missed something

[Yaël Dillies]

Simply change your code to

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 []
    | _ => [])

[Shubham Kumar 🦀 (he/him)]

I'm sorry, I'm such a big idiot, thanks for helping a fool! :man_facepalming:

[Shubham Kumar 🦀 (he/him)]

it was right there, I couldn't see it

[Yaël Dillies]

No problem :smile:

[Eric Wieser]

if I place [DecidableEq s] before the {s : Type} then ...

I strongly recommend adding set_option autoImplicit false to the top of your file so that this gives a much stronger error messag