seq の実装と Monad 実装から誘導される seq の実装が一致しない例

Functional programming in Lean より

structure NonEmptyList (α : Type) where
  head : α
  tail : List α

def NonEmptyList.toList {α : Type} (xs : NonEmptyList α) : List α :=
  xs.head :: xs.tail

def NonEmptyList.append {α : Type} (xs : NonEmptyList α) (ys : NonEmptyList α) : NonEmptyList α :=
  ⟨xs.head, xs.tail ++ ys.toList⟩

instance [ToString α] : ToString (NonEmptyList α) where
  toString xs := toString xs.toList

#eval { head := 1, tail := [2, 3] : NonEmptyList Nat}

instance {α : Type} : Append (NonEmptyList α) := ⟨NonEmptyList.append⟩

structure RawInput where
  name : String
  birthYear : String
deriving Repr

structure CheckedInput (thisYear : Nat) : Type where
  name : {n : String // n ≠ ""}
  birthYear : {y : Nat // y > 1900 ∧ y ≤ thisYear}
deriving Repr

def CheckedInput.toString {thisYear : Nat} : CheckedInput thisYear → String
  | ⟨name, birthYear⟩ => s!"name: {name}, birth year: {birthYear}"

instance (y : Nat) : ToString (CheckedInput y) where
  toString := CheckedInput.toString

/-- ε がエラーの型を表していて、エラーが一つ出たら即終了ではなくて、
全部のエラーを集めて出力できるようにする -/
inductive Validate (ε α : Type) : Type where
  | ok : α → Validate ε α
  | errors : NonEmptyList ε → Validate ε α

def Validate.toString {ε α : Type} [ToString ε] [ToString α] : Validate ε α → String
  | .ok x => s!"ok {x}"
  | .errors errs => s!"errors {errs}"

instance {ε α : Type} [ToString ε] [ToString α] : ToString (Validate ε α) where
  toString := Validate.toString

instance : Functor (Validate ε) where
  map f
   | .ok x => .ok (f x)
   | .errors errs => .errors errs

instance : Applicative (Validate ε) where
  pure := .ok
  seq f x :=
    match f with
    | .ok g => g <$> (x ())
    | .errors errs =>
      match x () with
      | .ok _ => .errors errs
      | .errors errs' => .errors (errs ++ errs')

abbrev Field := String

example : Repr (Field × String) := by infer_instance

def reportError (f : Field) (msg : String) : Validate (Field × String) α :=
  .errors { head := (f, msg), tail := [] }

def checkName (name : String) : Validate (Field × String) {n : String // n ≠ ""} :=
  if h : name = "" then
    reportError "name" "Required"
  else pure ⟨name, h⟩

/-- エラーが出ていた時にチェックを早期にやめてしまう -/
def Validate.andThen (val : Validate ε α) (next : α → Validate ε β) : Validate ε β :=
  match val with
  | .errors errs => .errors errs
  | .ok x => next x

#check Monad.toBind
#check Bind.bind

#eval "21".toNat?
#eval "attack 21".toNat?
#eval "21 ".toNat?
#eval "21 ".trim.toNat?

/-- 文字列として与えられた年のフィールドが数値かどうか -/
def checkYearIsNat (year : String) : Validate (Field × String) Nat :=
  match year.trim.toNat? with
  | none => reportError "birth year" "Must be digits"
  | some n => pure n

def checkBirthYear (thisYear year : Nat) : Validate (Field × String) {y : Nat // y > 1900 ∧ y ≤ thisYear} :=
  if h : year > 1900 then
    if h' : year ≤ thisYear then
      pure ⟨year, by simp [*]⟩
    else reportError "birth year" s!"Must be no later than {thisYear}"
  else reportError "birth year" "Must be after 1900"

def checkInput (year : Nat) (input : RawInput) : Validate (Field × String) (CheckedInput year) :=
  pure CheckedInput.mk <*>
    checkName input.name <*>
    (checkYearIsNat input.birthYear).andThen fun birthYearAsNat =>
      checkBirthYear year birthYearAsNat

#eval checkInput 2021 { name := "Alice", birthYear := "1999" }
#eval checkInput 2021 { name := "Alice", birthYear := "1899" }
#eval checkInput 2021 { name := "", birthYear := "1999" }
#eval checkInput 2021 { name := "Alice", birthYear := "attack" }

def notFun : Validate String (Nat → String) :=
  .errors { head := "First error", tail := [] }

def notArg : Validate String Nat :=
  .errors { head := "Second error", tail := [] }

#check notFun <*> notArg
#eval notFun <*> notArg

open Validate in 

-- Monad インスタンスから誘導される Seq.seq のデフォルト実装
def Validate.seq {α β ε : Type} (f : Validate ε (α → β)) (x : Unit → Validate ε α) : Validate ε β :=
  andThen f fun g =>
  andThen (x ()) fun y =>
  pure (g y)

#check Seq.seq notFun (fun () => notArg)
#eval Validate.seq notFun (fun () => notArg)

Start with the Validate Applicative instance and the separate Validate.seq definition shown in the issue, then run the two #check and #eval examples for notFun and notArg. Compare their results and determine what behavior should match; done means the direct implementation and the Monad-derived seq implementation agree on the reported result.