Phi is a lightweight interpreter for pure lambda calculus, implemented in Haskell. It provides a simple yet powerful environment for experimenting with lambda calculus expressions.
- Pure Lambda Calculus Support: Implements β-reduction and variable substitution
- Lazy Evaluation: Uses Haskell's natural lazy evaluation strategy
- Robust Parser: Handles nested expressions and complex lambda terms
- Comment Support: Handles both single-line (
--
) and multi-line ({- -}
) comments - Maximum Step Limit: Prevents infinite recursion with configurable step limits
- Stack build tool
# Clone the repository
git clone https://github.com/sergiobonatto/phi.git
cd phi
# Build the project
stack build
# install the project
stack install
-- Single line comments start with --
{- Multi-line comments
use {- and -} -}
-- Basic boolean operations
let true = λt.λf.t
let false = λt.λf.f
let neg = λb. (b false true)
-- List implementation using Scott encoding
let cons = λh.λt.λc.λn. (c h (t c n))
let nil = λc.λn.n
stack exec phi -- <file> [-s] [-c]
Options:
-s Display execution statistics (reduction steps and time)
-c Show final environment state
The interpreter follows a modular design with clear separation of concerns:
Expression.hs
: Core lambda calculus expression types and data structuresEnvironment.hs
: Environment management and variable bindingsEvaluator.hs
: Expression evaluation and reduction strategiesSubstitution.hs
: Variable substitution and β-reduction implementation
Tokenize.hs
: Lexical analysis and token generationParser.hs
: Main parsing orchestration and integrationParseCommon.hs
: Shared parsing utilities and helpersParseExpr.hs
: Lambda expression parsing logicParseApp.hs
: Function application parsingParseDefinition.hs
: Let-binding and definition parsingParseError.hs
: Comprehensive error handling types and messages
ProcessCode.hs
: Source code processing and evaluation pipelineParseTypes.hs
: Core parsing types and data structures
The project includes a test suite covering the main components:
stack test
Tests include:
- Tokenization
- Expression parsing
- Definition processing
- Evaluation logic
BSD-3-Clause License.