A statically-typed functional programming language with advanced type system features, inspired by ML and Scala.
Umλ combines the elegance of lambda calculus with modern programming language features. It's designed for:
- Type safety - Catch errors at compile time
- Expressiveness - Pattern matching, polymorphism, and rich type system
- Simplicity - Clean syntax without unnecessary ceremony
- Correctness - Formal verification of core semantics in Coq
- Simply Typed Lambda Calculus foundation
- System F polymorphism - Generic functions with type parameters
- Subtyping for records (width and depth)
- Hindley-Milner type inference - Write less type annotations
- Algebraic data types via pattern matching
- First-class functions - Lambdas and closures
- Pattern matching - Elegant case analysis on data structures
- Records - Structural typing with subtyping
- Lists - Built-in list type with cons/nil
- Recursive functions - Via fixpoint combinator
- Let polymorphism - Generalize types in let bindings
- Interactive REPL - Explore and test code interactively
- Comprehensive tests - Parser, type checker, and evaluator
- CI/CD - Automated testing with GitHub Actions
- Formal verification - Type safety proofs in Coq
# Clone the repository
git clone https://github.com/oguricap0327/umlambda.git
cd umlambda
# Build with sbt
sbt compile
# Run REPL
sbt runumλ> 42 + 8
50 : Int
umλ> (x: Int) => x * 2
<function> : (Int => Int)
umλ> let double = (x: Int) => x * 2 in double 21
42 : Int// Integers
42
-17
// Booleans
true
false
// Strings
"Hello, world!"
"Uma" ++ "Lambda" // String concatenation// Lambda expressions
(x: Int) => x + 1
// Named functions with let
let inc = (x: Int) => x + 1 in inc 41
// Multi-parameter functions (curried)
let add = (x: Int) => (y: Int) => x + y in add 10 32// Record literals
{ x = 10, y = 20 }
// Field access
let point = { x = 5, y = 3 } in point.x
// Record types with subtyping
let origin: { x: Int, y: Int } = { x = 0, y = 0, z = 0 } // OK! Width subtyping// List literals
[1, 2, 3, 4, 5]
// Empty list (needs type annotation)
Nil[Int]
// Cons constructor
1 :: 2 :: 3 :: Nil[Int]// Match on lists
let sum = fix sum: List[Int] => Int = (xs: List[Int]) =>
match xs with
| [] => 0
| x :: xs => x + sum xs
in sum [1, 2, 3, 4, 5]
// Match on records
let getX = (p: { x: Int, y: Int }) =>
match p with
| { x = x, y = _ } => x
// Match on literals
let isZero = (n: Int) =>
match n with
| 0 => true
| _ => false// Factorial
fix fact: Int => Int = (n: Int) =>
if n == 0 then 1 else n * fact (n - 1)
// Fibonacci
fix fib: Int => Int = (n: Int) =>
if n <= 1 then n else fib (n - 1) + fib (n - 2)
// List length
fix length: List[Int] => Int = (xs: List[Int]) =>
match xs with
| [] => 0
| _ :: xs => 1 + length xs// Polymorphic identity function
Λ[A] => (x: A) => x
// Type application
let id = Λ[A] => (x: A) => x in id[Int] 42
// Polymorphic list functions
let map = Λ[A] => Λ[B] =>
fix map: (A => B) => List[A] => List[B] =
(f: A => B) => (xs: List[A]) =>
match xs with
| [] => Nil[B]
| x :: xs => f x :: map f xs:help, :h Show help
:quit, :q Exit REPL
:type <expr> Show type of expression
:env Show current environment
:clear Clear environment
src/main/scala/umlambda/
├── AST.scala # Abstract syntax tree definitions
├── Parser.scala # Parser combinators
├── TypeChecker.scala # Type checking with subtyping
├── TypeInference.scala # Hindley-Milner type inference
├── Evaluator.scala # Environment-based interpreter
├── Stdlib.scala # Standard library functions
└── REPL.scala # Interactive read-eval-print loop
formal/
└── STLC.v # Coq formalization of type safety
Umλ uses a bidirectional type system:
- Type checking - Verify explicitly typed terms
- Type inference - Infer types for unannotated terms
- Subtyping - Records support width and depth subtyping
The type system is proven sound via progress and preservation theorems (see formal/STLC.v).
# Run all tests
sbt test
# Run specific test suite
sbt "testOnly umlambda.ParserTest"
sbt "testOnly umlambda.TypeCheckerTest"
sbt "testOnly umlambda.EvaluatorTest"
# Verify Coq proofs
cd formal && coqc STLC.vThe formal/ directory contains Coq proofs of type safety for the core STLC fragment:
- Progress - Well-typed terms are either values or can take a step
- Preservation - Types are preserved under evaluation
- Type Safety - Well-typed programs don't get stuck
Theorem type_safety : ∀ t t' τ,
[] ⊢ t ∈ τ →
t ⟶* t' →
value t' ∨ ∃ t'', t' ⟶ t''fix qsort: List[Int] => List[Int] = (xs: List[Int]) =>
match xs with
| [] => []
| pivot :: rest =>
let smaller = filter ((x: Int) => x < pivot) rest in
let larger = filter ((x: Int) => x >= pivot) rest in
qsort smaller ++ [pivot] ++ qsort larger// Map
fix map: (Int => Int) => List[Int] => List[Int] =
(f: Int => Int) => (xs: List[Int]) =>
match xs with
| [] => []
| x :: xs => f x :: map f xs
// Filter
fix filter: (Int => Bool) => List[Int] => List[Int] =
(p: Int => Bool) => (xs: List[Int]) =>
match xs with
| [] => []
| x :: xs => if p x then x :: filter p xs else filter p xs// Binary tree as nested records
type Tree = { tag: String, value: Int, left: Tree, right: Tree }
let leaf = (n: Int) => { tag = "leaf", value = n, left = {}, right = {} }
let node = (n: Int) => (l: Tree) => (r: Tree) =>
{ tag = "node", value = n, left = l, right = r }
// Tree sum
fix treeSum: Tree => Int = (t: Tree) =>
match t.tag with
| "leaf" => t.value
| "node" => t.value + treeSum t.left + treeSum t.right- Module system
- Type classes / traits
- Effect system
- Dependent types (Pi types)
- Compile to LLVM or JVM
- Standard library expansion
- Package manager
- Language server protocol (LSP)
Contributions are welcome! This is a learning project, so feel free to:
- Add new language features
- Improve error messages
- Extend the standard library
- Write more tests
- Improve documentation
- Pierce, Benjamin C. Types and Programming Languages
- Cardelli, Luca. Type Systems
- Milner, Robin. A Theory of Type Polymorphism in Programming
- Software Foundations (Coq proof assistant)
MIT License - See LICENSE file for details
Oguri Cap 🐎
- GitHub: @oguricap0327
Built with ❤️ and 🐎 energy