The Concept of Type Classes

1-- We want one "show" function that works for many types
2-- But each type has different logic:
3
4def showNat (n : Nat) : String := toString n
5def showBool (b : Bool) : String := if b then "true" else "false"
6def showList (xs : List Nat) : String := s!"[{xs}]"
7
8-- Tedious! We want:
9-- show 42        → "42"
10-- show true      → "true"
11-- show [1,2,3]   → "[1, 2, 3]"

1-- Define what it means to be "showable"
2class Show (α : Type) where
3  show : α → String
4
5-- Implement for specific types
6instance : Show Nat where
7  show n := toString n
8
9instance : Show Bool where
10  show b := if b then "true" else "false"
11
12-- Now we can use show generically
13#eval Show.show 42      -- "42"
14#eval Show.show true    -- "true"

1-- [Show α] means "α must have a Show instance"
2def greet [Show α] (x : α) : String :=
3  s!"Hello, {Show.show x}!"
4
5#eval greet 42       -- "Hello, 42!"
6#eval greet true     -- "Hello, true!"
7
8-- Multiple constraints
9def compare [Ord α] [Show α] (x y : α) : String :=
10  match Ord.compare x y with
11  | .lt => s!"{Show.show x} < {Show.show y}"
12  | .eq => s!"{Show.show x} = {Show.show y}"
13  | .gt => s!"{Show.show x} > {Show.show y}"

1def showTwice [Show α] (x : α) : String :=
2  s!"{Show.show x}, {Show.show x}"
3
4#eval showTwice 7

1-- Built-in, used by string interpolation
2class ToString (α : Type) where
3  toString : α → String
4
5-- This is why s!"x = {x}" works
6#eval s!"value: {42}"        -- "value: 42"
7#eval s!"flag: {true}"       -- "flag: true"

1class BEq (α : Type) where
2  beq : α → α → Bool
3
4-- Enables == operator
5#eval 5 == 5     -- true
6#eval "a" == "b" -- false

1class Ord (α : Type) where
2  compare : α → α → Ordering
3
4-- Ordering is: .lt, .eq, or .gt
5-- Enables <, >, <=, >= operators
6#eval compare 5 3    -- .gt
7#eval 5 < 3          -- false

1class Hashable (α : Type) where
2  hash : α → UInt64
3
4-- Used by HashMap, HashSet
5#eval hash "hello"   -- some UInt64

1class Functor (f : Type → Type) where
2  map : (α → β) → f α → f β
3
4-- map transforms the value inside
5#eval Functor.map (· + 1) (some 5)     -- some 6
6#eval Functor.map (· + 1) [1, 2, 3]    -- [2, 3, 4]
7
8-- Infix operator: <$>
9#eval (· * 2) <$> some 10              -- some 20
10#eval (· * 2) <$> [1, 2, 3]            -- [2, 4, 6]

1class Applicative (f : Type → Type) extends Functor f where
2  pure : α → f α
3  seq : f (α → β) → (Unit → f α) → f β
4
5-- pure wraps a value
6#eval (pure 5 : Option Nat)            -- some 5
7
8-- Apply functions inside containers: <*>
9#eval some (· + 1) <*> some 5          -- some 6
10#eval [(*2), (*3)] <*> [1, 2]          -- [2, 4, 3, 6]

1-- Lean figures out which Show instance to use
2#eval Show.show 42      -- Uses Show Nat
3#eval Show.show "hi"    -- Uses Show String
4
5-- This happens at compile time
6def printTwice [Show α] (x : α) : String :=
7  let s := Show.show x  -- Lean picks the instance
8  s ++ ", " ++ s

1-- deriving generates instances automatically
2structure Point where
3  x : Int
4  y : Int
5  deriving Repr, BEq, Hashable
6
7-- Now these work:
8#eval repr (Point.mk 1 2)            -- Shows the structure
9#eval Point.mk 1 2 == Point.mk 1 2   -- true

1-- 1. Built-in instances (Nat, Bool, String, etc.)
2#eval (5 : Nat) == 5   -- BEq Nat exists
3
4-- 2. Derived instances
5structure RGB where
6  r : UInt8
7  g : UInt8
8  b : UInt8
9  deriving BEq
10
11-- 3. Your own instances
12instance : ToString RGB where
13  toString c := s!"rgb({c.r}, {c.g}, {c.b})"
14
15-- 4. Instances from libraries
16-- (Importing a library may bring instances into scope)