path: a lambda calculus to explore type-directed program synthesis

Overview

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.

Getting started

Development of path typically uses cabal new-build:

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