Idris2-Table: Evaluating dependently-typed tables with... (Extended Abstract)
summary
Built an Idris 2 library that encodes table schemas as dependent types and implements the Brown Benchmark for Table Types examples and programs, covering example tables and all but one of the table API; schema shapes and column access become compile‑time proofs so column name/index errors are rejected before run. Type‑level computation supports adding/dropping columns and user‑definable constraints (quiz* columns must be numeric, p‑hacking example finds a jelly‑bean–acne correlation). Performance is not optimized; FFI to C is deferred.
AI-written summary · about
chapters (4)
related talks
41mPrograms and Proofs — Dependent Typing as a Way to Structure Your Code
43mIdris 2: Type-driven development of Idris
24mImperative Syntax for Dependent Types
39mDependent Type Driven Program Synthesis in Idris
01h 06mKeynote – Edwin Brady
58mPanel discussion: Types for All: From weak to strong, from static to dynamic
20mFirst-class Algebraic Presentations with Elaborator Reflection (Extended Abstract)
25mBinding Syntax for Dependently-Typed Programs