Telling the Truth with Types
summary
Scala code uses Cats, cats-effect, http4s, kind-projector, partial unification, shapeless and fs2 to lift reasoning into types so behavior is provable at compile time. Examples: replace throwing with ApplicativeError with Throwable and provide a safe divide using a NonZeroInt sealed abstract wrapped in the companion for validation; model sockets → parser → HTTPApp → renderer as Request -> F[Response] with a Resource bracket for stage shutdown to auto-finalize. These patterns compile and eliminate many runtime surprises.
AI-written summary · about
chapters (28)
- 0:00Introduction
- 1:08Communication
- 3:17Naming
- 4:33Not mathematically accurate
- 5:06Baseline setup
- 5:47Typical examples
- 6:20Backdoors
- 7:07meaningless types
- 7:31function types
- 10:20proving that something exists
- 12:14there exists
- 14:20given int
- 15:30generic
- 16:27identity
- 17:04such
- 18:25compound
- 20:27deferred composition
- 21:40IO app
- 22:40HTTP app
- 26:19Useless types
- 27:42Recap
- 28:47Intuition behind there exists
- 30:07Shut down
- 33:22Making it understandable
- 34:42Making it reasonable
- 36:07Throwing vs Raising
- 37:34No Stupid Questions
- 39:24The Rational Type
