idris-book
examples (some) and solutions to the exercices in "Type-Driven Development with Idris"
- chapter 2 (basics, lists)
- chapter 3 (pattern matching, type-driven interactive development, implicit arguments, vectors)
- chapter 4 (data types, enumeration types, union types, generic types, dependent types, interactive programs,
Maybe,Either,impossible) - chapter 5 (interactive programs extended, handling IO errors, dependent pairs, files,
IO,doand>>=) - chapter 6 (type synonyms, type-level functions, type computation, record data type)
- chapter 7 (interfaces, function composition, partial application,
Eq,Ord,Show,Num,Neg,Integral,Fractional,Abs,Cast,Functor,Foldable,Monad) - chapter 8 (properties of functions and data, equalities, proofs, rewrite rules,
=,Void,Dec,DecEq) - chapter 9 (predicates, contracts, program states,
Elem,Uninhabited,absurd,auto) - chapter 10 (views, covering functions, data structure traversals, recursive views and termination, modules, data representation hiding,
SnocList,SplitRec,VList,Lazy,Delay,Force,$,with) - chapter 11 (streams and infinite data, recursion/corecursion, data/codata, terminating/productive functions, namespaces,
Inf,Lazy,Delay,Force,Delayed,Divides,mutual) - chapter 12 (mutable state, state management, record update syntax)
- chapter 13 (state machines, protocols in types, preconditions/postconditions, dependent types in states)
- chapter 14 (handling errors in state transitions, security properties in types, abstract vs concrete state)
- chapter 15 (concurrency, message-passing communication, behavioral types)