Higher Order Abstract Syntax parser and evaluator.

Higher.hs

module Higher where

-- https://github.com/MaiaVictor/Cedille-Core/blob/master/old_haskell_implementation/Core.hs

type Name = String

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

toString :: Term -> String
toString (Var var)      = var
toString (Lam var body) = concat ["\\", var, " ", toString (body (Var var))]
toString (App fun arg)  = concat [".", toString fun, " ", toString arg]

fromString :: String -> Term
fromString src = snd (go src) []
    where
    go :: String -> (String, [(String, Term)] -> Term)

    go (' ' : src) = go src

    -- Lambda
    go ('\\' : src) = let
        (src', var) = name src
        (src'', body) = go src'
        in (src'', \ctx -> Lam var (\arg -> body ((var, arg) : ctx)))

    -- Application
    go ('.' : src) = let
        (src', fun) = go src
        (src'', arg) = go src'
        in (src'', \ctx -> App (fun ctx) (arg ctx))

    go src = let
        (src', var) = name src
        in (src', \ctx ->
            case lookup var ctx of
                Just t  -> t
                Nothing -> Var var)

    name :: String -> (String, String)
    name [] = ([], [])
    name (' ' : src) = (src, [])
    name (c : src) = let
        (src', cs) = name src
        in (src', c : cs)

eval :: Term -> Term
eval (Var var)      = Var var
eval (Lam var body) = Lam var (\arg -> eval (body arg))
eval (App fun arg)  = let
    fun' = eval fun
    arg' = eval arg
    in case fun' of
        Lam var body -> eval (body arg)
        fun'         -> App fun' arg'

-- toString $ eval $ fromString "\\a a"
-- toString $ eval $ fromString ".\\a .a a \\a a"
-- toString $ fromString ".\\a ..a a a \\a ..a a a"