Conditional on type belonging to a type class

Stream: general

[DSB]

Hello, folks. I'm trying to learn Lean for functional programming, and I was wondering if the following was possible. Consider the code below:

class MInterface (a : Type) where
  fm : a -> Int

instance :  MInterface Nat where
  fm x := x + 1
instance :  MInterface String where
  fm x := String.length (x) + 1

structure M where
  {T : Type}
  [inst : MInterface T]
  [repr : Repr T]
  val : T

instance : Repr M where
  reprPrec m n := @Repr.reprPrec m.T m.repr m.val n

def x : M := ⟨1⟩
def lx : List M := [⟨1⟩, ⟨"ok"⟩]
#eval x -- 1
#eval lx -- [1, "ok"]

This M structure allows me to create lists having distinct types, as long as these types are all instances of some given class(es). All very good. Here is my "problem". In the code above, I've constrained M on [repr : Repr T], which allowed me to make M an instance of Repr.

Yet, I'd want to get rid of the [repr: Repr T] constraint, and instead make M an instance of Repr by providing a function that uses the repr for a given type if it belongs to such class, and otherwise it does something generic (like write the string "no-repr"). For example:

structure MyType where
  _1 : Int
  _2 : Int
instance :  MInterface MyType where
  fm m := m._1 + m._2

def m1 : MyType := MyType.mk 1 2
def l2 : List M := [⟨1⟩, ⟨"ok"⟩, ⟨m1⟩] -- [1, "ok", "no-repr"]
#eval l2

This code fails, since MyType is not Repr, but I've commented what the desired output should be.
An even better output would be using the deriving Repr.

I mean, when I define MyType without the deriving Repr, Lean seems to infer it, since I can still use #eval. I was wondering if I could mimic this behavior.

[Edward van de Meent]

i don't think there's a safe way to do that, without doing some elaboration shenanigans.

[Yaël Dillies]

What about adding a default low priority Repr instance for all types? Something like

instance (priority := 1) (α : Type*) : Repr α where reprPrec m n := "no-repr"

[Edward van de Meent]

i'd recommend you inline the instance in a custom constructor

[Edward van de Meent]

otherwise, maybe something like [repr:Repr T := default_repr T] works? i don't know if instance synthesis or default argument takes precedence in this case though...

[Alex Meiburg]

structure M where
  {T : Type}
  [inst : MInterface T]
  val : T
  repr : Repr T := by first | infer_instance | exact defaultRepr

instance : Repr M where
  reprPrec m n := @Repr.reprPrec m.T m.repr m.val n

def defaultRepr {T : Type} : Repr T where
  reprPrec _ _ := "no-repr".quote

structure MyType where
  _1 : Int
  _2 : Int
instance :  MInterface MyType where
  fm m := m._1 + m._2

def m1 : MyType := MyType.mk 1 2

def l2 : List M := [M.mk 1, M.mk "ok", M.mk m1] -- [1, "ok", "no-repr"]
#eval l2

essentially does what you want.

[Alex Meiburg]

You won't be able to use the ⟨1⟩ notation though, not unless you make your own similar notation.

[Kyle Miller]

Edward van de Meent said:

maybe something like [repr:Repr T := default_repr T] works?

This isn't valid syntax, optional parameters only work for default binders (x : T := v)

[Edward van de Meent]

right, that makes sense

[Edward van de Meent]

it was just a guess

[Kyle Miller]

DSB said:

if it belongs to such class

If you're coming from other functional languages, just watch out that typeclasses in Lean aren't constraints — instead they're just a mechanism for automatically synthesizing an implicit argument. There's a not very strong sense of "belonging to a class" (one definition might be "Repr T is nonempty", but then every T belongs to "Repr" since it's trivial to write a "no repr" instance, and another might be "synthesis can find a Repr T instance", but that can change depending on what instances are available). This means that unless you do what Alex suggests, with trying to pin down a Repr instance manually, then from within the Repr M instance there's nothing you can do to ask for the Repr M.T instance.

[Kyle Miller]

DSB said:

This M structure allows me to create lists having distinct types

Could you expand on what you're doing? I'm not sure I'm following what's supposed to be distinct from what.

[DSB]

Thanks, @Alex Meiburg ! Why the ⟨ ... ⟩ notation becomes unavailable? Also, is there a way to use the deriving Repr instead of the "no-repr"?

[DSB]

@Kyle Miller , the idea is that M represents something like types that I can render in the screen. Thus, I wish to have a collection (list) of such types, and apply a single render function over the list.

I think, in summary, the idea is of ad-hoc polymorphisms. I want to create a collection of elements, all that have types with a render function, which can then be used individually.

[Alex Meiburg]

That notation sees that M can take two arguments, so it insists on providing both arguments. It doesn't accept the fact that it's got a default value.

[Kyle Miller]

(I've been wondering whether it's an oversight that anonymous constructor notation doesn't know about optParams (default values).)

[DSB]

Alex Meiburg said:

That notation sees that M can take two arguments, so it insists on providing both arguments. It doesn't accept the fact that it's got a default value.

How can one define his own notation? I see that the M.mk is passed to each element in the list. Can I define a quick notation that maps the M.mk to the elements somehow?

[Kyle Miller]

DSB said:

the idea is that M represents something like types that I can render in the screen. Thus, I wish to have a collection (list) of such types, and apply a single render function over the list.

I see, then in that case I think your original solution is best. It's capturing a "closure" of what Lean sees as all the instances, and it's sort of the best you can hope for, beyond perhaps making it easy to have a "no repr" repr in scope when it is needed — that is, Yael's solution is pretty much what you'd be using. Alex's solution is Yael's solution without making the "no repr" repr be a global instance.

[Kyle Miller]

I think it's worth thinking about why you have types that don't have the typeclass available design-wise. Can you instead ensure they all implement an instance for the class?

[DSB]

In the case of Repr, it is just a convenience. Let me explain the whole idea.
The structure M represents graphical primitive shapes. This means that if I create a type, say, Circle, I then create an instance of M for such Circle by providing a render : Circle -> Drawing. Another primitive type could be Rectangle or Square, etc. The idea is that I have these primitive types, each of which I know how to represent as a drawing in the screen. Think of how SVG renders figures.

Now, imagine I have a complex figure, where I have a list of many of such primitives. Hence, to render the whole list I map the render function to each element in the list (which are all instance of M, and therefore have a valid render).

I then have a function that flattens [Drawing] -> Drawing into a single drawing.
All good. Now, for convenience, it would be nice to have a repr for my list of primitives (i.e. values of List M). Just so one can check what is inside, before rendering. I could force the repr in the primitive types. But this would not be "nice" from a design point of view, because having a Repr is not actually part of the specification.

[Kyle Miller]

I think unfortunately that's what you have to live with though, since you're using repr so it's become part of the specification. (One thing to think about: there's no runtime representation for Type, so there's no way to look up a Repr instance at runtime, even using "unsafe" code.)

[Alex Meiburg]

In that case you could 'tighten' Yael's approach, to something like

instance (priority := 1) (α : Type*) [Drawable α] : Repr α where reprPrec m n := "no-repr"

(I'm assuming that Drawable is some class that specifies this render: T -> Drawing method.) Now all Drawable's have a default Repr they can use. But this won't leak over to other types.

[Kyle Miller]

If you know C++, you can think about M as being a way to associate a vtable to a value, and adding this repr field is how you can do the run-time polymorphism.

[Alex Meiburg]

To me, that feels much better than just doing it universal over all types. It's still localized to "your" types you're working with locally, and won't suddenly provide a Repr for e.g. some crazy category theory types.

[DSB]

The code by Yael gives me an error...
unexpected token ')'; expected term

The same error appears in yours implementation, @Alex Meiburg .

[Kyle Miller]

Just to check, that solution still involves putting a Repr instance in the M type, right @Alex Meiburg? The point of it is to avoid polluting the global Repr instances?

[Alex Meiburg]

Yes, exactly

[Kyle Miller]

@DSB Yael was using a mathlib extension. Here:

instance (priority := 1) (α : Type _) : Repr α where reprPrec m n := "no-repr"

[Yaël Dillies]

(apologies!)

[DSB]

Alex Meiburg said:

In that case you could 'tighten' Yael's approach, to something like

instance (priority := 1) (α : Type*) [Drawable α] : Repr α where reprPrec m n := "no-repr"

(I'm assuming that Drawable is some class that specifies this render: T -> Drawing method.) Now all Drawable's have a default Repr they can use. But this won't leak over to other types.

This Drawable would be the M?

[Kyle Miller]

@DSB With that instance, the idea would be

structure M where
  {T : Type}
  [inst : Drawable T]
  [repr : Repr T]
  val : T

Since there's a Drawable T instance around, that enables this particular instance.

[DSB]

Thank you all for the answers!

[DSB]

I guess my last question would be if this "no-repr" could instead be something like the deriving Repr. I mean, instead of a generic string, it somehow inspects the structure and gives something a bit more meaningful.

[Kyle Miller]

Are you types not the sorts of things you can do deriving Repr with? Or post-hoc do the deriving instance Repr for YourTypeName with?

[Kyle Miller]

Whatever it is, it has to be done at compile time and not at runtime. There's no runtime representation for types, so there is not much to introspect at runtime. (There's just enough structure that the runtime is able to free objects and decrement reference counts when reference counts go to zero, but I don't believe any of that is accessible to Lean programs, and I'm sure this is anything you'd want to see in a repr instance anyway.)