path: a lambda calculus to explore type-directed program synthesis
path was initially based on the calculus described in A tutorial implementation of a dependently typed lambda calculus. It has been extended with the quantitative type theory described in Syntax and Semantics of Quantitative Type Theory.
path typically uses
cabal new-build # build the library and pathc cabal new-repl # load the library in GHCI
Path’s REPL can be run from GHCI:
λ import Path.REPL λ repl (packageSources basePackage) λ: …
or from the CLI:
cabal new-run pathc -- -i src/Base/*.path