Haskell Code and Commentary

-- Defining MinHS using HOAS.

-- Key point: Recfun will take types τ1 and τ2, and a function,
-- i.e. roughly a lambda binding in Haskell.


data BinOp = Plus | Minus | Times | Equals
  deriving (Show, Eq)

data Type = Bool | IntType | FunType Type Type
  deriving (Show, Eq)

data MinHS =
    Num Int
  | Lit Bool
  | If MinHS MinHS MinHS
  | BinOp BinOp MinHS MinHS
  | Apply MinHS MinHS
    -- The key HOAS idea here (using Haskell as meta-language),
    -- the body element is equivalent to what the substitution mechanism
    -- of FOAS would do with it. It takes in some expressions to replace
    -- f and x with and gives a resulting expression.
  | RecFun Type Type (MinHS -> MinHS -> MinHS)
    -- Tags added as a bit of a hack to make the pretty-printer work.
  | NameTag String
    -- Tags added as a bit of a hack to make the type-checker work.
  | TypeTag Type


-- A minimal version of "show" that prints everything it can, not much
-- in the case of RecFun.
simple_show :: MinHS -> String
simple_show (Num n) = "(Num " ++ show n ++ ")"
simple_show (Lit b) = "(Num " ++ show b ++ ")"
simple_show (If c t f) = concat ["(If ", simple_show c, " ",
    simple_show t, " ", simple_show f, ")"]
simple_show (BinOp b x y) = concat ["(BinOp ", show b, " ",
    simple_show x, " ", simple_show y, ")"]
simple_show (Apply f x) = concat ["(Apply ",
    simple_show f, " ", simple_show x, ")"]
simple_show (RecFun _ _ _) = "(RecFun ?)"
simple_show (NameTag nm) = "(NameTag " ++ show nm ++ ")"
simple_show (TypeTag t) = "(TypeTag ?)"


-- Let's copy our demos into this explicit representation.

factorial :: Int -> Int
factorial 0 = 1
factorial n = n * factorial (n - 1)

{-
Factorial in MinHS concrete syntax, which we aren't doing here.
(We are leaving parsing as an exercise.)

-- inside the recfun, f has type (Int -> Int) and n has type Int
factorial == recfun f :: (Int -> Int) n =
    if n == 0
    then 1
    else n * f (n - 1)


-- what happens with factorial 2?

factorial 2 ≡ (recfun f :: (Int -> Int) n =
    if n == 0
    then 1
    else n * f (n - 1)) 2
  |->
  (if n == 0
    then 1
    else n * f (n - 1)) [n := 2, f := recfun ... ]
  ≡
  (if 2 == 0
    then 1
    else 2 * ((recfun f :: (Int -> Int) n =
      if n == 0
      then 1
      else n * f (n - 1)) (2 - 1)))
  |->*
  (2 * ((recfun f :: (Int -> Int) n =
      if n == 0
      then 1
      else n * f (n - 1)) 1)
  |->*
  (2 * ((if n == 0
    then 1
    else n * f (n - 1)) [n := 1, f := recfun ... ])
  |->* ...
  (2 * 1 * ((if n == 0
    then 1
    else n * f (n - 1)) [n := 0, f := recfun ... ]))
  |->* ...
  (2 * 1 * (if 0 == 0 then 1 else ...))
  |->* ...
  (2 * 1 * 1)

-}


-- Factorial and add as MinHS HOAS syntax.
factorial_minhs :: MinHS
factorial_minhs = RecFun IntType IntType (\f n ->
    If (BinOp Equals n (Num 0))
      (Num 1) (BinOp Times n (Apply f (BinOp Minus n (Num 1)))))

add_minhs :: MinHS
add_minhs = RecFun IntType (FunType IntType IntType) (\f x ->
    RecFun IntType IntType (\f y -> BinOp Plus x y))

-- Some pretty-printer setup

pretty_type :: Type -> String
pretty_type Bool = "Bool"
pretty_type IntType = "Int"
pretty_type (FunType t1 t2) =
    concat ["(", pretty_type t1 , " -> ", pretty_type t2, ")"]

-- A pretty printer. Its argument is a counter, a simple way of
-- picking fresh names. The generated names like f1, x2 are sometimes
-- called "genvars". This is a useful mechanism, but users don't like
-- it much when terms full of names like "n1268" get printed.

printer :: Int -> MinHS -> String
printer ix minhs = case minhs of
  Num n -> show n
  Lit b -> show b
  BinOp Plus x y -> concat ["(", printer ix x, " + ", printer ix y, ")"]
  BinOp Minus x y -> concat ["(", printer ix x, " - ", printer ix y, ")"]
  BinOp Times x y -> concat ["(", printer ix x, " * ", printer ix y, ")"]
  BinOp Equals x y ->
        concat ["(", printer ix x, " == ", printer ix y, ")"]
  Apply x y -> concat ["(", printer ix x, " ", printer ix y, ")"]
  If c x y -> concat ["(if ", printer ix c, " then ", printer ix x,
        " else ", printer ix y, ")"]
  RecFun t1 t2 body -> concat ["(recfun ", f_nm, " :: (", pretty_type t1,
        " -> ", pretty_type t2, ") ", x_nm, " = ",
        printer (ix + 1) (body (NameTag f_nm) (NameTag x_nm)), ")"]
      -- key idea: body is a substitution, substitute in things that
      -- pretty-print as "f" and "x" (adding them to the AST for this)
    where
      f_nm = "f" ++ show ix
      x_nm = "x" ++ show ix
  NameTag nm -> nm
  -- _ -> error ("printer: unimplemented: " ++ simple_show minhs)


binop_argument_types :: BinOp -> [Type]
binop_argument_types Plus = [Int, Int]
binop_argument_types Minus = [Int, Int]
binop_argument_types Times = [Int, Int]
binop_argument_types Equals =
    error "binop_argument_types: Equals is polymorphic"

binop_return_type :: BinOp -> Type
binop_return_type Plus = Int
binop_return_type Minus = Int
binop_return_type Times = Int
binop_return_type Equals = Bool

-- A type checker for MinHS. 
type_check :: MinHS -> Type
type_check (Num _) = IntType
type_check (Lit _) = Bool
type_check (If c t f) = if ct == Bool && tt == ft
        then tt
        else (error ("type_check: If got types: " ++ show [ct, tt, ft]))
    where
      ct = type_check c
      tt = type_check t
      ft = type_check f
type_check (BinOp Equals x y) = if xt == yt then Bool
        else error ("type_check: Equals: argument types: "
                ++ show [xt, yt])
    where
      xt = type_check x
      yt = type_check y
type_check (BinOp bop x y) = if arg_tys == binop_argument_types bop
        then binop_result_type bop else error (concat
            ["type_check: binop: ", show bop, ": argument types: ",
                show arg_tys])
    where
      arg_tys = map type_check [x, y]
type_check (Apply f x) = case type_check f of
    FunType t1 t2 -> (if type_check x == t1 then t2
        else error ("type_check: apply: " ++
            show (map type_check [f, x]))
    ty -> error ("type_check: apply: operator had type: " ++ show ty)
type_check (RecFun t1 t2 body) =
    FunType t1 (type_check (body (TypeTag (FunType t1 t2)) (TypeTag t1)))
type_check (TypeTag ty) = ty
type_check x = error ("type_check: unexpected: " ++ simple_show x)




-- Interesting point about our HOAS: our RecFun already contains
-- the substitution operator we need for evaluating, so evaluating
-- isn't that complicated to write (especially if we skip the
-- arithmetic bits).

eval :: MinHS -> MinHS
eval x = case x of
  Num _ -> x
  Lit _ -> x
  RecFun _ _ _ -> x
  If cond true_case false_case -> case eval cond of
    Lit True -> eval true_case
    Lit False -> eval false_case
    v -> error ("eval: type error: If cond eval-ed to: " ++ simple_show v)
  BinOp bop lhs rhs -> error ("unimplemented: " ++ simple_show x)
  Apply f x -> case eval f of
    RecFun t1 t2 body -> eval (body (RecFun t1 t2 body) (eval x))
    v -> error ("eval: type error: Apply lhs eval-ed to: "
            ++ simple_show v)
  _ -> error ("eval: evaluating: " ++ simple_show x)