ToString

ToString は、文字列への変換を行う型クラスです。

structure Point (α : Type) where
  x : α
  y : α

def origin : Point Int := ⟨0, 0⟩

-- 文字列補完により文字列に変換しようとしても、
-- 最初はどう変換したらいいのかわからないのでエラーになる
/--
error: failed to synthesize
  ToString (Point Int)
Additional diagnostic information may be available using the `set_option diagnostics true` command.
-/
#guard_msgs (error) in #check s!"{origin}"

/-- `ToString` のインスタンスを登録する -/
instance : ToString (Point Int) where
  toString p := s!"Point: ({p.x}, {p.y})"

-- これで文字列に変換できる
/-- info: "Point: (0, 0)" -/
#guard_msgs in #eval s!"{origin}"

Repr と ToString

Repr のインスタンスはないが、ToString のインスタンスはあるという状態で #eval しようとすると、Repr の代わりに ToString のインスタンスが使用されます。Repr のインスタンスを与えればそちらが優先して使用されます。

/-- info: Point: (0, 0) -/
#guard_msgs in #eval origin

-- `Repr` のインスタンスを自動生成して登録する
-- 以降は、`#eval` 時には `Repr` のインスタンスが使用される
deriving instance Repr for Point

/-- info: { x := 0, y := 0 } -/
#guard_msgs in #eval origin

逆に、Repr のインスタンスはあるが、ToString のインスタンスがないとき、ToString の代わりに Repr が呼び出されることはありません。エラーになります。

structure Person where
  name : String
  age : Nat
deriving Repr

def david := Person.mk "David" 42

-- #eval はできる
#eval david

-- `ToString` のインスタンスがないのでエラーになる
/--
error: failed to synthesize
  ToString Person
Additional diagnostic information may be available using the `set_option diagnostics true` command.
-/
#guard_msgs (error) in #check s!"{david}"