Set Theoretic Algebraic Constructive Calculus
summary
Claims a set‑theoretic dependent calculus (Stacc) that encodes types as sets of predicates and uses union for application and coproducts for data, demonstrates Peano naturals and lists built from the empty set and successor, and exposes constructive evaluation that aborts on absurdity rather than returning booleans. An early REPL and Scala prototype exist on GitHub but the type‑checker proof is still pending, and the language targets a new JVM dependently‑typed implementation.
AI-written summary · about
chapters (18)
- 0:00Introduction
- 0:18Core Language
- 0:58Why Lambda Calculus
- 2:47The Stack
- 4:00Algebraic
- 5:10Constructivism
- 6:40Intuition
- 8:02Syntax
- 12:55Recap
- 24:12Dependent typing
- 29:15Invariants
- 33:39New Types
- 36:14Building
- 39:31Recursion
- 40:24Naturals
- 42:53Induction steps
- 45:57Parametric city
- 48:05Invariant
related talks
55mKeynote: Propositions as Types
30mConstraint Typing with Boolean Algebra
01h 12mTruth about Types
16mWhat's in the Box: Ergonomic and Expressive Capture Tracking over Generic Data(…)
49mThe Trouble With Types
36mAlgebraic DataTypes in Scala. Where is the algebra? What other algebras are there?
28mType-Driven Prompt Programming: From Typed Interfaces to a Calculus of Constraints
47mHistory and Philosophy of types