VictorTaelin / lambda-calculus

A simple, clean and fast implementation of the λ-calculus on JavaScript.
MIT License
44 stars 6 forks source link

Cleaner implementation #1

Open VictorTaelin opened 4 years ago

VictorTaelin commented 4 years ago

A few years later this is my cleaned up implementation:

// Term
const Var = (name)      => ({ctor:"Var",name});
const Lam = (name,body) => ({ctor:"Lam",name,body});
const App = (func,argm) => ({ctor:"App",func,argm});

// List
const Nil = ()          => ({ctor:"Nil",size: 0});
const Ext = (head,tail) => ({ctor:"Ext",head,tail,size:tail.size+1});

// Finds first value in a list satisfying `cond`
function find(list, cond) {
  switch (list.ctor) {
    case "Nil": throw "Not found.";
    case "Ext": return cond(list.head) ? list.head : find(list.tail, cond);
  };
};

// Stringification
function show(term) {
  switch (term.ctor) {
    case "Var": return term.name;
    case "Lam": return "λ"+term.name+"."+show(term.body(Var(term.name)));
    case "App": return "("+show(term.func)+" "+show(term.argm)+")";
  };
};

// Parsing
function parse(code, indx) {
  var indx = 0;
  function parse_char(chr) {
    if (code[indx++] !== chr) throw "Bad parse.";
  };
  function parse_name() {
    return /[0-9A-Z_a-z]/.test(code[indx]) ? code[indx++]+parse_name() : "";
  };
  function parse_term() {
    while (/[ \n]/.test(code[indx])) ++indx;
    var chr = code[indx++];
    switch (chr) {
      case "λ":
        var name = parse_name();
        var skip = parse_char(".");
        var body = parse_term();
        return ctx => Lam(name, (x) => body(Ext([name,x],ctx)));
      case "(":
        var func = parse_term();
        var argm = parse_term();
        var skip = parse_char(")");
        return ctx => App(func(ctx), argm(ctx));
      default:
        --indx;
        var name = parse_name();
        return ctx => find(ctx, (x) => x[0] === name)[1];
    };
  };
  return parse_term()(Nil());
};

// Reduce to weak head normal form
function reduce(term) {
  switch (term.ctor) {
    case "Var": return Var(term.name);
    case "Lam": return Lam(term.name, term.body);
    case "App":
      var func = reduce(term.func);
      switch (func.ctor) {
        case "Lam": return reduce(func.body(term.argm));
        default   : return App(func, term.argm);
      };
  };
};

// Reduce to normal form
function normalize(term) {
  var term = reduce(term);
  switch (term.ctor) {
    case "Var": return Var(term.name);
    case "Lam": return Lam(term.name, x => normalize(term.body(x)));
    case "App": return App(normalize(term.func), normalize(term.argm));
  };
};

var t;
t = parse("(λf.λx.(f (f x)) λg.λy.(g (g y)))");
t = normalize(t);
t = show(t);
console.log(t);

This is just cleaner, simpler and fast (HOAS). Won't PR because busy, but wanted to leave this here. Good template to start experimenting with language development in JS.

coproduto commented 4 years ago

I made a Haskell "translation" of your implementation. It can probably still be improved (most obvious would be use the State Monad to get rid of explicit threading of the parsed string), but I guess it might serve as a starting point for messing around with the lambda calculus in Haskell :)

import Data.Char (isLetter, isNumber, isSpace)
import Data.List (span, dropWhile, lookup)

type ParseError = String

-- A parser is a function that takes a string and returns a parse error or a
-- pair of the parsed data and the remaining string.
type Parser a = String -> Either ParseError (a, String)

type Context = [(String, Term)]

data Term = Var String
          | Lam String (Term -> Term)
          | App Term Term

instance Show Term where
  show (Var s)        = s
  show (Lam arg body) = "λ" ++ arg ++ "." ++ show (body (Var arg))
  show (App f x)      = "(" ++ (show f) ++ " " ++ (show x) ++ ")"

reduce :: Term -> Term
reduce (App (Lam arg body) x) = reduce (body x)
reduce term                   = term

normalize :: Term -> Term
normalize term = case reduce term of
  (Var name)     -> Var name
  (Lam arg body) -> Lam arg (\x -> normalize (body x))
  (App f x)      -> App (normalize f) (normalize x)

parseChar :: Char -> Parser Char
parseChar target (char:rest)
  | target == char = Right (char, rest)
  | otherwise      = Left ("Bad parse: unexpected " ++ [char])

slurpChar :: Parser Char
slurpChar (x:xs) = Right (x, xs)
slurpChar []     = Left "Bad parse: unexpected end of input"

parseName :: Parser String
parseName = Right . span (\c -> isLetter c || isNumber c)

parseWhitespace :: Parser ()
parseWhitespace s = Right ((), dropWhile isSpace s)

parseLam :: Parser (Context -> Term)
parseLam s = do
  (name, rest)   <- parseName s
  (_, rest')     <- parseChar '.' rest
  (body, rest'') <- parseTerm rest'
  return ((\ctx -> Lam name (\x -> body((name, x):ctx))), rest'')

parseApp :: Parser (Context -> Term)
parseApp s = do
  (f, rest)    <- parseTerm s
  (arg, rest') <- parseTerm rest
  (_, rest'')  <- parseChar ')' rest'
  return ((\ctx -> App (f ctx) (arg ctx)), rest'')

parseBoundName :: Parser (Context -> Term)
parseBoundName s = do
  (name, rest) <- parseName s
  return
    (
      (\ctx -> case lookup name ctx of
          Just value -> value
          Nothing    -> error ("Unknown variable " ++ name)),
      rest
    )

parseTerm :: Parser (Context -> Term)
parseTerm s = do
  ((), rest)    <- parseWhitespace s
  (char, rest') <- slurpChar rest
  case char of
    'λ' -> parseLam rest'
    '(' -> parseApp rest'
    _   -> parseBoundName (char:rest')

parse :: Parser Term
parse s = do
  (termFunction, rest) <- parseTerm s
  return $ (termFunction [], rest)

printTerm :: Term -> IO ()
printTerm = print . normalize

main :: IO ()
main =
  let term = "(λf.λx.(f (f x)) λg.λy.(g (g y)))"
  in case parse term of
    Left parseError   -> putStrLn parseError
    Right (result, _) -> printTerm result