Bidirectional.hs

module Main where

import qualified Data.Map as Map

type Id = String

data Typ
  = TInt
  | TFun Typ Typ
  deriving (Eq)

data Exp
  = Int Int
  | Id Id
  | Fun Id Exp
  | App Exp Exp
  | Add Exp Exp
  | Typ Typ Exp
  deriving (Eq)

type Env = Map.Map Id Typ

emptyEnv :: Env
emptyEnv = Map.empty

extendEnv :: Id -> Typ -> Env -> Env
extendEnv = Map.insert

lookupEnv :: Id -> Env -> Maybe Typ
lookupEnv = Map.lookup

synth :: Env -> Exp -> Typ
synth _   (Int _) = TInt
synth env (Id x) = case lookupEnv x env of
  Just t -> t
  Nothing -> error ("unbound identifier " ++ x)
synth _   (Fun x e) = error "cannot synthesize the type of a function"
synth env (App e1 e2) = case synth env e1 of
  TFun t1 t2 -> if check env e2 t1 then t2 else error "invalid arg. type"
  _ -> error "expected function"
synth env (Add e1 e2) =
  if check env e1 TInt && check env e2 TInt then
    TInt
  else
    error "something is not an integer in someone's Elm program"
synth env (Typ t e) = 
  if check env e t then t else error "incorrect type annotation"

check :: Env -> Exp -> Typ -> Bool
check _   (Int _) TInt = True
check _   (Int _) _ = False
check env (Id x) t = case lookupEnv x env of
  Just s -> s == t
  Nothing -> error ("unbound identifier " ++ x)
check env (Fun x e) (TFun t1 t2) =
  check (extendEnv x t1 env) e t2
check _   (Fun _ _) _ =
  error "bad error message this is" 
check env (App e1 e2) t = 
  check env e1 (TFun (synth env e2) t)
check env (Add e1 e2) TInt =
  check env e1 TInt && check env e2 TInt
check _ (Add _ _) _ =
  False
check env (Typ t e) s =
  s == t && check env e t


-- Examples that should work:
-- synth emptyEnv (Typ (TFun Int Int) (Fun "x" (Id "x")))

-- synth emptyEnv (Typ TInt (App (Fun "x" (Id "x")) (Int 10)))

-- AddEventListener :: (Event -> Void) -> Void is in my env.
--
-- synth addEventListener(function(evt) { ... })