A curated collection of functional programming patterns and advanced techniques
implemented in Idris
This repository showcases various functional programming concepts, from effects and
continuations to category theory-inspired patterns and SMT-based constraint solving.
Each snippet is self-contained and demonstrates idiomatic Idris code with
dependent types.
File
Description
Eff.idr Extensible effects using free monad with State and Reader interpreters
EffCont.idr Continuation-based implementation of extensible effects
EffContSimp.idr Simplified continuation-based effect handlers with Maybe example
EffFTCQueue.idr Extensible effects using fast type-aligned sequences (FTCQueue)
HEff.idr Heterogeneous/indexed effects with resource tracking
HEffCont.idr Continuation-based heterogeneous effects with state machine example
FreerCont.idr Church-encoded freer monad with State effect
FreeDelivery.idr Free applicative functors for batch/static analysis
FreeSelectiveDelivery.idr Free selective functors for static analysis with branching
Runner.idr Effect runners (handlers) separating user and kernel computations
MonadLogic.idr LogicT monad transformer for backtracking search
ITree.idr Interaction trees (coinductive free monad with visible effects)
IxFreer.idr Indexed freer monad for state machine effects (login/logout)
Continuations and Control Flow
File
Description
ContT.idr Continuation monad transformer with shift/reset and callCC
Delim.idr Delimited continuations with prompts and subcontinuations
Select.idr Selection monad for backtracking/search (e.g., binary search)
YinYang.idr The famous yin-yang continuation puzzle
Lazy Evaluation and Circular Programming
File
Description
Repmin.idr Bird's repmin problem solved with circular/lazy programming
Metamorphic.idr Metamorphisms combining folds and unfolds with streaming
Category Theory and Abstractions
File
Description
Adjoint.idr Adjoint functors and deriving monads from adjunctions (State)
Kan.idr Kan extensions (Ran, Lan) including Yoneda and Codensity
RelativeMonad.idr Formalization of relative monads with category theory foundations
Naperian.idr Naperian (representable) functors with logarithms and tabulators
File
Description
Classical.idr Classical logic principles (TND, RAA, Pierce's law) and their equivalences
Leibniz.idr Leibniz equality as substitutability in any context
Russell.idr Russell's paradox demonstrating Type-in-Type inconsistency
UnivalenceFromScratch.idr Univalence axiom and equivalences formalization
Ordinals.idr Transfinite ordinal numbers (omega, epsilon-naught)
WTypes.idr W-types (well-founded trees) encoding naturals and binary trees
Dijkstra.idr Dijkstra monad for specification and verification of stateful programs
Hoare.idr Hoare state monad with pre/post conditions for verification
PredicateTransformer.idr Predicate transformers for program specification (weakest preconditions)
SMT Solvers and Constraint Programming Interpreters and Languages
File
Description
HOAS.idr Higher-order abstract syntax interpreter with fixpoints
STLCInterp.idr Simply-typed lambda calculus interpreter with staged compilation
TypedNBE.idr Normalization by evaluation for typed lambda calculus
TypeIndexedTypeChecker.idr Type-indexed type checker with typed syntax output
LambdaSKI.idr Lambda calculus to SKI combinator compilation
SKICorrect.idr Verified SKI combinator translation preserving semantics
Unlambda.idr Unlambda esoteric language interpreter with continuations
MiniForth.idr Type-indexed Forth-like stack machine interpreter
Simplicity.idr Simplicity blockchain language implementation
HarperRegexV1.idr Regex matching with mendler-style catamorphisms
HarperRegexV2.idr Regex with generic recursion (divide-and-conquer)
Expr.idr Tagless-final DSL for imperative expressions with code generation
Data Structures and Algorithms
File
Description
FTCQueue.idr Fast type-aligned catenable queue for efficient monadic bind
HRAL.idr Heterogeneous binary random-access lists
Matrix.idr Block-partitioned matrices with LAoP (linear algebra of programming)
Tensor.idr Multi-dimensional tensors with Naperian functor structure
Network.idr Type-safe neural network layer specification DSL
GridOps.idr Grid operations (shifting, neighbor lookup) for 2D puzzles
Stream Processing and Fusion
File
Description
StreamFusion.idr Stream fusion for efficient staged pipeline compilation
FoldFusion.idr Fold fusion with tagless-final representation
ZipFolds.idr Zipping church-encoded folds (single-pass zip)
Ziria.idr Ziria streaming DSL with take/emit and pipeline composition
ZiriaCont.idr Continuation-based Ziria streaming implementation
File
Description
Circuits.idr Boolean circuit DSL with multiple interpretations (eval, show)
Capabilities.idr Lightweight static guarantees via phantom types (sorted lists)
Diff.idr Automatic differentiation via reverse-mode AD with code generation
Enumeration.idr Fair enumeration combinators for test generation
MonadicMemo.idr Monadic memoization using state monad
MonoidSolver.idr Reflection-based monoid equation solver with soundness proof
NonDet.idr Non-determinism with tagless-final style (permutations)
Printf.idr Type-safe printf using dependent types
SqlDsl.idr Type-safe SQL query DSL with schema tracking
Tasks.idr Build system abstraction (applicative vs monadic tasks)
ZipperTraversable.idr Generic zipper for any traversable using continuations
Most files include example expressions that can be evaluated directly in the Idris REPL:
See LICENSE for details.