Custom Type Classes

1-- A class for types that can be serialized to JSON
2class ToJson (α : Type) where
3  toJson : α → String
4
5-- Instances for basic types
6instance : ToJson Nat where
7  toJson n := toString n
8
9instance : ToJson String where
10  toJson s := s!""{s}""
11
12instance : ToJson Bool where
13  toJson b := if b then "true" else "false"
14
15#eval ToJson.toJson 42        -- "42"
16#eval ToJson.toJson "hello"   -- ""hello""
17#eval ToJson.toJson true      -- "true"

1class Serializable (α : Type) where
2  serialize : α → String
3  deserialize : String → Option α
4
5instance : Serializable Nat where
6  serialize n := toString n
7  deserialize s := s.toNat?
8
9#eval Serializable.serialize 123          -- "123"
10#eval Serializable.deserialize "456"      -- some 456
11#eval (Serializable.deserialize "abc" : Option Nat)  -- none

1-- A Monoid has an identity and an associative operation
2class Monoid (α : Type) where
3  empty : α
4  append : α → α → α
5  -- Laws (not enforced, but expected):
6  -- append empty x = x
7  -- append x empty = x
8  -- append (append x y) z = append x (append y z)
9
10instance : Monoid String where
11  empty := ""
12  append := String.append
13
14instance : Monoid (List α) where
15  empty := []
16  append := List.append
17
18-- Generic function using Monoid
19def concat [Monoid α] (xs : List α) : α :=
20  xs.foldl Monoid.append Monoid.empty
21
22#eval concat ["a", "b", "c"]       -- "abc"
23#eval concat [[1,2], [3], [4,5]]   -- [1, 2, 3, 4, 5]

1-- Semigroup: just append
2class Semigroup (α : Type) where
3  append : α → α → α
4
5-- Monoid extends Semigroup with identity
6class Monoid' (α : Type) extends Semigroup α where
7  empty : α
8
9-- Instances must provide all methods
10instance : Monoid' Nat where
11  empty := 0
12  append := Nat.add
13
14-- Functions can use parent class methods
15def reduce [Monoid' α] (xs : List α) : α :=
16  xs.foldl Semigroup.append Monoid'.empty

1-- Convert between types
2class Convertible (α β : Type) where
3  convert : α → β
4
5instance : Convertible Nat Int where
6  convert n := Int.ofNat n
7
8instance : Convertible Int String where
9  convert i := toString i
10
11#eval (Convertible.convert 42 : Int)     -- 42
12#eval (Convertible.convert (42 : Int) : String)  -- "42"

1-- The element type determines the collection type uniquely
2class Collection (elem : Type) (coll : outParam Type) where
3  empty : coll
4  insert : elem → coll → coll
5  toList : coll → List elem
6
7-- For Nat, the collection is List Nat
8instance : Collection Nat (List Nat) where
9  empty := []
10  insert := List.cons
11  toList := id
12
13-- Lean infers coll from elem
14def build [Collection α coll] (xs : List α) : coll :=
15  xs.foldl (fun c x => Collection.insert x c) Collection.empty

1class Printable (α : Type) where
2  -- Required method
3  repr : α → String
4  
5  -- Optional with defaults
6  print : α → IO Unit := fun x => IO.println (repr x)
7  printList : List α → IO Unit := fun xs => 
8    xs.forM (fun x => print x)
9
10-- Only need to implement repr
11instance : Printable Nat where
12  repr := toString
13
14-- print and printList work automatically
15#eval (Printable.print 42 : IO Unit)

1-- Expression type class
2class Expr (α : Type) where
3  lit : Int → α
4  add : α → α → α
5  mul : α → α → α
6
7-- Evaluator instance
8instance : Expr Int where
9  lit n := n
10  add := Int.add
11  mul := Int.mul
12
13-- Pretty printer instance
14instance : Expr String where
15  lit n := toString n
16  add x y := s!"({x} + {y})"
17  mul x y := s!"({x} * {y})"
18
19-- One expression, multiple interpretations
20def expr [Expr α] : α :=
21  Expr.add (Expr.lit 1) (Expr.mul (Expr.lit 2) (Expr.lit 3))
22
23#eval (expr : Int)     -- 7
24#eval (expr : String)  -- "(1 + (2 * 3))"