Type-driven Development with Idris by Edwin Brady

What people said (1)

• mdm12 · 2026-02-21 in Parse, Don't Validate and Type-Driven Design in Rust

  One option is dependent pairs, where one value of the pair (in this example) would be the length of the array and the other value is a type which depends on that same value (such as Vector n T instead of List T). Type-Driven Development with Idris[1] is a great introduction for dependently typed languages and covers methods such as these if you're interested (and Edwin Brady is a great teacher). …