Research internship In progress
Aristarchus
A verifier for the Hypatia proof language
A Metamath-style proof checker: it validates a derivation instead of searching for one, and reports every error in a single run.
-- Errors accumulate instead of short-circuiting:
-- one run reports every problem, not just the first.
data Result e a
= Failure [e]
| Success a
instance Applicative (Result e) where
pure = Success
Success f <*> Success x = Success (f x)
Failure e1 <*> Failure e2 = Failure (e1 ++ e2)
Failure e1 <*> Success _ = Failure e1
Success _ <*> Failure e2 = Failure e2