Lambda Calculus in Idris.

lambda.idr

-- Because this hasn't reached the prelude yet.
instance Monad (Either x) where
  return = Right
  (Left a) >>= _ = Left a
  (Right a) >>= f = f a

-- In the lambda calculus, expressions are either symbols,
-- function definitions, or applications thereof.
data Expression : Set where
  symbol  : String -> Expression
  lambda  : String -> Expression -> Expression
  applied : Expression -> Expression -> Expression

instance Show Expression where
  show (symbol s) = s
  show (lambda s d) = "(lambda " ++ s ++ " . " ++ show d ++ ")"
  show (applied d e) = "(" ++ show d ++ " " ++ show e ++ ")"

-- A value for now is just a closure -- essentially a lambda with
-- the environment it was evaluated in attached.
record Value : Set where
  closure :
       (environment : List (String, Value))
    -> (parameter   : String)
    -> (body        : Expression)
    -> Value

-- Let us know if bad stuff happened.
data Error : Set where
  -- We tried to evaluate a symbol that wasn't in the environment.
  undefined : String -> Error

-- Apparently I need to forward-declare things for idris??
apply : Value -> Value -> Either Error Value

-- Evaluate an expression.
eval : List (String, Value) -> Expression -> Either Error Value
eval [] (symbol s) = Left $ undefined s
eval ((n, v) :: ss) (symbol s) = if n == s
  then Right v else eval ss (symbol s)
eval e (lambda p b) = Right $ closure e p b
eval e (applied x y) = eval e x >>= \x => eval e y >>= \y => apply x y

-- Apply one value to another.
apply c d = eval ((parameter c, d) :: environment c) $ body c