Abstract data types in region of abysmal pain & how to navigate them
summary
Defines a typesafe ADT for directed acyclic graphs implemented in Idris, mirroring an inductive mathematical definition (empty | add vertex with parents). Uses dependent types to make parent lists provably members of the earlier graph, so add returns Nothing for invalid parents and parents/children return proofs not Maybes. Builds ancestor traversal that terminates (proves totality), removes the infinite-recursion bug from the naive implementation, and demonstrates with historical-node examples like Leibniz, Russell, Whitehead.
AI-written summary · about
chapters (11)
- 0:00Start
- 1:55History of Functional Programming
- 2:17Graph of Influence
- 10:21Type Constructors
- 13:32Traversal
- 17:20Traversal Functions
- 17:32Function Ancestors
- 24:22Nature of Types
- 27:04Dependent Types
- 30:03Test for Membership
- 38:02Function for Getting the Ancestors of an Element
related talks
40mADTs For The Win!
26mAbstraction Functions as Types
41mPrograms and Proofs — Dependent Typing as a Way to Structure Your Code
58mDomain Driven Design (DDD) with Algebraic Data Types (ADT)
17mComputing with Generic Trees in Agda
41mFun With Categories
47mType-Driven Development in Idris
41mType-driven Development of Communicating Systems in Idris