Programs

Type classes and instances

Write one function whose behavior depends on the input type.

class Describe (α : Type) where
  describe : α → String

instance : Describe Nat where
  describe n := s!"Natural number: {n}"

instance : Describe Bool where
  describe b := if b then "yes" else "no"

def report {α : Type} [Describe α] (value : α) : String :=
  Describe.describe value

def main : IO Unit := do
  IO.println (report (42 : Nat))
  IO.println (report true)

Explanation

`class · instance`

The class declares an interface. Each instance supplies its implementation for a particular type.

`{α : Type}`

An implicit type parameter, usually inferred from value.

`[Describe α]`

An instance parameter resolved by Lean’s type class search. This mechanism also supplies operations and laws in mathematical libraries.

Expected output

Reference only. Run the file to check its actual result.

Natural number: 42
yes

Exercise

Add a Describe String instance and call report on a string.

Related examples

Structures