Type inference and polymorphism

Stream: new members

[David Wang]

Hello. I am trying to define the typeclass, which characterises a set with an additional operation that picks a member of type α. I have the following lines:

class Sel (γ : Type v) (α : outParam (Type u)) where
  sel : γ → α

class Set_Choose (α : Type u) {γ : Type v} [Membership α γ] [EmptyCollection γ] [Sel γ α] where
  not_empty_implies_in {S : γ}: ¬ (S = emptyCollection) → ((Sel.sel S) ∈ S)


class Map (α : Type u) (β : Type v) (γ : Type w) where
  lookup : α → β → (Option γ)
  delete : α → β → α

class Lawful_Map {α : Type u} {β : Type v} {γ : Type w} [m: Map α β γ] where
  delete_imp_not_in : m.lookup (m.delete M x) x = none

class Graph {adjacency : Type u} (vertex : Type u) [neighb: Set_Choose vertex] where

I get the following error:

failed to synthesize
  Sel ?m.623 vertex
use `set_option diagnostics true` to get diagnostic information

I have tried to play around with the annotations and type parameters, by making some explicit and some implicit.

Another question: Is it possible to set this option in the VSCode extension?

[Brendan Seamas Murphy]

Lean can't figure out what γ should be in [@Set_Choose α γ _ _ _], and also it's failing because Set_Choose expects there to be an instance of Sel γ α (which it can't find because you haven't declared any instances, and also it doesn't know what γ is and uses γ to determinant α)

[Brendan Seamas Murphy]

When you write Set_Choose vertex in neighb : Set_Choose vertex, what's your intended value of γ?

[David Wang]

On the second point. Is there a way to reason about typeclasses without providing any instance?

[David Wang]

The intended value of \gamma is Set vertex

[Brendan Seamas Murphy]

You can assume an instance exists, so eg prove something of the form example mylemma (α γ) [Sel γ α] : True := by trivial

[Brendan Seamas Murphy]

But it sounds like you have a specific Sel (Set α) α instance you want to use

[David Wang]

Brendan Seamas Murphy said:

You can assume an instance exists, so eg prove something of the form example mylemma (α γ) [Sel γ α] : True := by trivial

Thank you. I have no specific instance.

[Brendan Seamas Murphy]

David Wang said:

The intended value of \gamma is Set vertex

That makes sense. Unfortunately lean no has no idea this is what you want, there's nowhere in the code that pins down γ as this. Is Set_Choose supposed to be for sets or for an arbitrary γ? If it's the latter it should probably be an explicit argument, because there's no way to infer it's value from just Set_Choose α

[David Wang]

Brendan Seamas Murphy said:

David Wang said:

The intended value of \gamma is Set vertex

That makes sense. Unfortunately lean no has no idea this is what you want, there's nowhere in the code that pins down γ as this. Is Set_Choose supposed to be for sets or for an arbitrary γ? If it's the latter it should probably be an explicit argument

The naming is perhaps confusing. Set_Choose should characterise a collection, which has the membership operation and can be empty, and if it is not empty has an operation which picks an arbitrary value from it. I have no idea how I would implement it for Set, but for Lists, sel could be head

[Brendan Seamas Murphy]

Right, then γ should definitely be explicit. If you write Set_Choose α, how is Lean (or the reader) supposed to know you're talking about Set α or about List α?

[Brendan Seamas Murphy]

And then additionally you need to implement an instance of [Sel (Set α) α] or assume one exists

[David Wang]

Brendan Seamas Murphy said:

Right, then γ should definitely be explicit. If you write Set_Choose α, how is Lean (or the reader) supposed to know you're talking about Set α or about List α?

They are not. They should be able to plug in the type later on.

Brendan Seamas Murphy said:

And then additionally you need to implement an instance of [Sel (Set α) α] or assume one exists

This is what I needed, I think.

[Brendan Seamas Murphy]

David Wang said:

Brendan Seamas Murphy said:

Right, then γ should definitely be explicit. If you write Set_Choose α, how is Lean (or the reader) supposed to know you're talking about Set α or about List α?

They are not. They should be able to plug in the type later on.

But there's no γ argument in Graph, so they can't set it