Experiment with type classes

Stream: new members

[misterdrgn]

Hi all. I've got a question, based on trying to implement a new type class after reading through parts of the programming in lean4 manual. I think the easiest way to do this is paste in a modestly sized block of code. The key problem area is when I try to define a new function, List.filterByMatch, that uses my new type class. That's at the very bottom of the code block. The rest is provided for context, but could likely be skipped to answer my main question. Any help there would be appreciated. Thanks!

-- Any example of an element
structure Point where
  x : Int
  y : Int
deriving Repr

-- All the types of elements. Imagine the types other than Point are defined elsewhere
inductive Element where
  | point (data : Point) : Element
  | region (data : Region) : Element
  | size (data: Size) : Element

-- Create a Point.Matcher type that can be used to match on Points
-- MatchValue is defined elsewhere (can provide if anyone is interested)
namespace Point
  structure Matcher where
    x : MatchValue Int
    y : MatchValue Int

  -- Default matcher
  def matcher : Matcher := {x := .noMatch, y := .noMatch}

  -- Check whether a matcher matches a particular Point
  def Matcher.matches (matcher : Matcher) (point: Point) : Bool :=
    matcher.x.matches (point.x) &&
      matcher.y.matches (point.y)

end Point

-- Now, we can use the Point.Matcher to cast Elements as Points.
-- One question here--afaik, Lean4 doesn't have guards that would allow the if let and let lines to be combined?
def Point.Matcher.cast (matcher : Point.Matcher) (ele : Element) : Option Point :=
  if let Element.point data := ele then
    if matcher.matches data then
      some data
    else
      none
  else
    none

-- Type class for all types that have a matcher.
-- Here, α is the matcher, for example Point.Matcher and β is the target type, for example Point
-- I don't know if there's a way to constrain this such that α will always be β.Matcher
class AnyMatcher (α : Type) (β : Type) where
  cast : α → Element → Option β

-- A couple of problems here. First, why is "{α : Type} {β : Type}" needed? I thought the guide indicated that was optiona.
-- Second, AnyMatcher.cast as used here doesn't compile. I'm not sure what's needed here.
def List.filterByMatch {α : Type} {β : Type} [AnyMatcher α β] (list : List Element) (matcher : α) : List Element :=
  list.filter (fun ele => (AnyMatcher.cast α ele).isSome)

[misterdrgn]

Here is an unsuccessful attempt to make the type class take just a single type.

class Matchable (α : Type) where
  Matcher : α → Type
  cast : Matcher α → Element → Option α

[Aaron Liu]

I'm not sure what you want. Can you explain what you want to do with the typeclass?

[Aaron Liu]

In particular, what is a "matcher"?

[Aaron Liu]

Can you post a #mwe?

[misterdrgn]

@Aaron Liu I'm mostly just trying to understand better how to use type classes--my questions are primarily about the last five lines of code in that code block, baked into the comments. If you read the questions in the comments for the code related to type classes, you'll see where I'm struggling. The rest is provided for context.

That said, I'm sure it's easier to provide feedback if you understand what the rest of the code is actually meant to do. Matchers are data structures for performing partial matches on their corresponding type. They're a concept my research group used in Clojure, and later in Swift. When I'm looking at a new language, I tend to be interested in trying them out in that language. Note that they involve a lot of boilerplate, and ideally matchers would be generated by macros, which I suspect is possible in Lean4, but I haven't really gotten to that part yet.

The idea is that you can do the following.

def ele := Element.point { x := 0, y := 0}

-- Try to turn an element into a point
#eval ele |> Point.matcher.cast

-- Try to turn an element into a point, provided its x value is 0.
#eval Element.point { x := 0, y := 0} |> {Point.matcher with x := .val 0}.cast

-- Try to turn an element into a point, provided its y value is < 10
#eval Element.point { x := 0, y := 0} |> {Point.matcher with y := .fn (· < 10) }.cast

In general, I like how this works in Lean4. The next question is whether I can write functions that are polymorphic over matchers for any type, which is what I am trying and failing to do in the code above.

Thanks.

[Aaron Liu]

In this case to solve your problem you want to say (AnyMatcher.cast matcher ele : Option β)

[Aaron Liu]

If you don't want to have the type ascription you need to make β a docs#outParam.

[misterdrgn]

@Aaron Liu Thanks. Both of those worked, and I think I have a better understanding of things now. In the following example, can you tell me why I need to include {α : Type} {β : Type} in the definition of filterByMatch? The manual suggested those could be left out and simply implied. Thank you.

class AnyMatcher (α : Type) (β : outParam Type) where
  cast : α → Element → Option β

def List.filterByMatch {α : Type} {β : Type} [AnyMatcher α β] (list : List Element) (matcher : α) : List Element :=
  list.filter (fun ele => (AnyMatcher.cast matcher ele).isSome)

[Aaron Liu]

They can be left out if you have autoImplicit set as true

[misterdrgn]

Got it, thanks.