FreshML
1 program
Added 2026-02-26T12:00:00Z
Agent: claude-codeModel: claude-sonnet-4-6WebSearch: disabled
Evidence
Report issue
View issues
Aliases: Fresh O'Caml
Provenance: commit 9c2f0c9777 · authored 2026-02-26T17:49:36+01:00 · agent claude-code · model claude-sonnet-4-6
Sources mentioning this language
1 source · not in taxonomy (canonical name didn't match any upstream)
Related languages
LLM-contributed programs
Lambda Calculus with Native Binders
Provenance: commit 9c2f0c9777 · authored 2026-02-26T17:49:36+01:00 · agent claude-code · model claude-sonnet-4-6 · WebSearch disabled
(* FreshML - Lambda Calculus with Native Binders *)
(* FreshML extends Standard ML with abstract names and binding types *)
(* Lambda calculus term type *)
datatype term =
Var of name (* variable reference *)
| App of term * term (* function application *)
| Lam of <<name>> term (* lambda abstraction with binder *)
(* Structural size of a term *)
fun size (Var _) = 1
| size (App(t1, t2)) = 1 + size t1 + size t2
| size (Lam(<<_>> t)) = 1 + size t
(* Depth of the term tree *)
fun depth (Var _) = 0
| depth (App(t1, t2)) = 1 + Int.max(depth t1, depth t2)
| depth (Lam(<<_>> t)) = 1 + depth t
(* Free variable check: is x free in t? *)
fun is_free (x : name) (Var y) = (x = y)
| is_free x (App(t1, t2)) = is_free x t1 orelse is_free x t2
| is_free x (Lam(<<y>> t)) = is_free x t (* y is fresh, so y <> x *)