gostlc - Simply Typed Lambda Calculus Interpreter

Go implemetation of Simple Typed Lambda Calculus (STLC) with base types - with zero external dependencies.

This is a toy interpreter for self learning purposes.

Features

Core Functionality

• STLC support: Lambda abstractions, applications, and variables
• Type system: Static type checking with Int and Bool base types, plus function types
• Conditional expressions: if-then-else constructs with type checking
• Literals: Integer and boolean literal support
• Builtin functions: Arithmetic, boolean, comparison operations with currying support

Language Features

Supported Types

• Int - Integer type
• Bool - Boolean type
• T1 -> T2 - Function type from T1 to T2

Supported Syntax

The EBNF grammar for the supported subset of STLC is as follows:

expr ::= var
       | "\" var ":" type "." expr         (* abstraction *)
       | expr expr                         (* application *)
       | "(" expr ")"                      (* grouping *)
       | "true" | "false"                  (* boolean literals *)
       | "if" expr "then" expr "else" expr (* conditional *)
       | digit+                            (* integer literals *)

type ::= "Bool"                            (* boolean type *)
       | "Int"                             (* integer type *)
       | type "->" type                    (* function type *)
       | "(" type ")"                      (* grouping *)

var  ::= letter (letter | digit)*          (* variable names *)

Builtin Functions

Arithmetic operations:

• add : Int -> Int -> Int - Addition
• sub : Int -> Int -> Int - Subtraction

Comparison operations:

• eq : Int -> Int -> Bool - Equality
• ne : Int -> Int -> Bool - Inequality
• lt : Int -> Int -> Bool - Less than
• le : Int -> Int -> Bool - Less than or equal
• gt : Int -> Int -> Bool - Greater than
• ge : Int -> Int -> Bool - Greater than or equal

Boolean operations:

• and : Bool -> Bool -> Bool - Logical AND
• or : Bool -> Bool -> Bool - Logical OR
• not : Bool -> Bool - Logical NOT

Installation

go install github.com/shota3506/gostlc/cmd/gostlc@latest

Usage

Interactive REPL

Start the REPL by running gostlc without arguments:

$ gostlc
STLC REPL
Type :quit or :q to exit, :help for help

gostlc> (\x:Int. x) 42
=> 42
gostlc> if true then 1 else 0
=> 1

Execute from File

gostlc sample.stlc

Execute from Command Line

gostlc -c "(\x:Int. x) 42"

Execute from stdin

echo "(\x:Bool. x) true" | gostlc -

Examples

Identity Function

(\x:Int. x) 42
# Result: 42

Function Composition

(\f:Int->Int. \g:Int->Int. \x:Int. f (g x))

Church Numerals

# Church numeral for 2
\f:Int->Int. \x:Int. f (f x)

# Church numeral for 3
\f:Int->Int. \x:Int. f (f (f x))

Conditional Logic

if (\x:Bool. x) true then 100 else 200
# Result: 100

Higher-Order Functions

(\f:Int->Int. f 10) (\x:Int. x)
# Result: 10

Arithmetic Operations

# Simple arithmetic
add 2 3
# Result: 5

sub 10 4
# Result: 6

# Partial application
(\inc:Int->Int. inc 10) (add 1)
# Result: 11

# Composition with builtins
add (sub 10 3) 5
# Result: 12

Boolean Operations

# Logical AND
and true false
# Result: false

# Logical OR
or false true
# Result: true

# Logical NOT
not true
# Result: false

# Complex boolean expressions
and (or false true) (not false)
# Result: true

# Using with conditionals
if (and true true) then 1 else 0
# Result: 1

Comparison Operations

# Equality
eq 5 5
# Result: true

# Inequality
ne 3 7
# Result: true

# Less than
lt 3 5
# Result: true

# Less than or equal
le 5 5
# Result: true

# Greater than
gt 10 3
# Result: true

# Greater than or equal
ge 7 7
# Result: true

# Using comparisons with conditionals
if (lt 3 5) then 100 else 200
# Result: 100

TODOs

• Let bindings: let x = e1 in e2 for local variable binding
• Recursive functions: Fixed-point operator or recursive let bindings
• Product types: Pairs/tuples with projection operations
• Sum types: Either/variant types with pattern matching
• Unit type: () for side-effect operations
• Type inference: Hindley-Milner style type inference to reduce type annotations
• Arithmetic operators: mul, div, mod (add and sub are already implemented)
• String type and operations: String literals and concatenation
• Debugger: AST inspection and step-by-step evaluation

License

This project is licensed under the MIT License.