qpf and type class instances

Stream: general

[matt rice]

checking out qpf's I built a few things, but i'm not sure how to deal with typeclasses
I managed to invoke repr, but couldn't figure out if there is a way to build an instance has_repr alt,
if anyone has any ideas

import data.fix.parser.equations data.fix.parser.basic
variables {α β γ : Type}

data alt
| l : α → alt
| r : β → alt

def alt.elim (from_l : α → γ) (from_r : β → γ) (it : @alt α β)
: γ
:= it.rec (from_l) (from_r)

def alt.repr {α β : Type} [lrepr : has_repr α] [rrepr : has_repr β] : (@alt α β) → string
:= (λ it, it.rec (λ l, "alt.l " ++ repr l) (λ r, "alt.r " ++ repr r))

/- Don't know how to synthesize placeholder content
 or type class instances if i try to add type class instances like above. -/
-- instance repr : has_repr alt := ⟨alt.repr⟩

def x := [alt.l "foo", alt.r 0]
def z : @alt string string := alt.l "foo"

#eval list.map (alt.repr) (x)
#eval z.rec repr repr
#eval list.map (alt.elim (λ l, alt.l (string.length l)) (λ r, alt.r(r + 1))) x

[Simon Hudon]

There’s not much meta information available able those data types but I’m planning on adding it. That should allow you to derive type classes like has_repr

[Simon Hudon]

Sorry, I just understood you were asking something different.

[Simon Hudon]

Try this:

instance alt.has_repr [has_repr α] [has_repr β] : has_repr (@alt α β) := ⟨@alt.repr α β _ _⟩

[Simon Hudon]

instead of the instance you commented out

[Simon Hudon]

You were running into issues because the type parameters of alt are marked as implicit but they cannot be inferred.

[Simon Hudon]

I recommend you declare alt as:

variables (α β γ : Type)

data alt
| l : α → alt
| r : β → alt

variables {α β γ}

[Simon Hudon]

its type parameters will be explicit but your functions will only use them as implicit type parameters

[matt rice]

nice that works, for the has_repr, will change the other

[Simon Hudon]

:+1: