Stash old idea: Add interpreter for a Direct Calc

Includes an attempt at typing.  Not planning to pursue this further.

Author: gregr

DirectCalc.hs

@@ -0,0 +1,127 @@
+{-# LANGUAGE NoMonomorphismRestriction, TupleSections #-}
+module DirectCalc where
+
+import qualified Data.Map as M
+import Data.Maybe
+import Control.Monad.State
+import Control.Monad.Error
+
+type Ident = String
+type Arity = Int
+type EnvKey = Arity
+type Env = [Value]
+data Name = Free Ident | Bound EnvKey
+  deriving (Show, Eq, Ord)
+
+data Term =
+  Type | Arrow Term Term | Ann Term Term |
+  Var Name | App Term Term | Lam Term
+  deriving (Show, Eq)
+
+data Neutral = NVar Ident | NApp Neutral Value
+  deriving (Show, Eq)
+
+type Closure = (Env, Term)
+data Value = VNeut Neutral | VClo Closure | VType | VArrow Value Value
+  deriving (Show, Eq)
+
+vvar (Free ident) env = VNeut $ NVar ident
+vvar (Bound key) env = env !! key
+vapp (VNeut neutral) arg = VNeut $ NApp neutral arg
+vapp (VClo (cenv, cbody)) arg = bigstep cbody $ arg : cenv
+
+bigstep (Var name) env = vvar name env
+bigstep (App tproc targ) env = vapp proc arg
+  where proc = bigstep tproc env
+        arg = bigstep targ env
+bigstep (Lam body) env = VClo (env, body)
+
+data TContext = TContext{tc_tvars :: M.Map EnvKey Term,
+                         tc_bvars :: M.Map Name [Term],
+                         tc_nextFresh :: EnvKey}
+tc_fresh = do
+  cxt <- get
+  let fresh = tc_nextFresh cxt
+  put $ cxt{tc_nextFresh = fresh + 1}
+  return $ Var $ Bound fresh
+tc_bvarFresh name = do
+  fresh <- tc_fresh
+  cxt <- get
+  let tys = fresh : (maybe [] id $ M.lookup name $ tc_bvars cxt)
+  put $ cxt{tc_bvars = M.insert name tys $ tc_bvars cxt}
+  return fresh
+tc_find key = do
+  cxt <- get
+  let (term, tvars) = _find (tc_tvars cxt) key []
+  put $ cxt{tc_tvars = tvars}
+  return term
+  where
+    _find tvars key accKeys = case M.lookup key tvars of
+      Just (Var (Bound next)) -> _find tvars next $ key : accKeys
+      Just term -> (term, merge term)
+      Nothing -> (vkey, merge vkey)
+      where vkey = Var $ Bound key
+            merge term = M.union tvars $ M.fromList $ map (, term) accKeys
+tc_assign key term = do
+  cxt <- get
+  put $ cxt{tc_tvars = M.insert key term $ tc_tvars cxt}
+
+subterms (Arrow ta tb) = [ta, tb]
+subterms (App ta tb) = [ta, tb]
+subterms (Ann ta tb) = [ta, tb]
+subterms (Lam body) = [body]
+subterms _ = []
+
+occurs name (Var vname) = name == vname
+occurs name term = any (occurs name) $ subterms term
+
+sunify (Ann ta tb) other = liftM (Ann ta) $ sunify tb other
+sunify other ann@(Ann ta' tb') = sunify ann other
+sunify (Var (Free _)) _ = error "something went wrong"
+sunify tvar@(Var (Bound key)) other = do
+  term <- tc_find key
+  if tvar == term
+    then if occurs (Bound key) term
+      then throwError $ "occurs check failed: " ++ show (key, term)
+      else tc_assign key term >> return term
+    else sunify term other
+sunify other (Var name) = sunify (Var name) other
+sunify Type Type = return Type
+sunify (Arrow ta tb) (Arrow ta' tb') =
+  liftM2 Arrow (sunify ta ta') $ sunify tb tb'
+-- TODO: reduce apps and inside lambdas for non-simple unify
+sunify (App ta tb) (App ta' tb') = liftM2 App (sunify ta ta') $ sunify tb tb'
+sunify (Lam body) (Lam body') = liftM Lam $ sunify body body'
+sunify ta tb = throwError $ "type mismatch: " ++ show (ta, tb)
+
+--sunifyE lenv renv = undefined
+
+sbvar name = do
+  cxt <- get
+  let bvars = tc_bvars cxt
+  case M.lookup name bvars of
+    Nothing -> tc_bvarFresh name
+    Just (ty : tys) -> do
+      final <- foldM sunify ty tys
+      put $ cxt{tc_bvars = M.insert name [final] bvars}
+      return final
+
+bigtype Type = return Type
+bigtype (Arrow ta tb) = bigtype ta >> bigtype tb >> return Type
+bigtype (Ann term ty) =
+  bigtype ty >>= sunify Type >> bigtype term >>= sunify ty >> return ty
+bigtype (Var name) = tc_bvarFresh name
+bigtype (Lam body) = do -- TODO: how to quantify? free var dependencies?
+  tbody <- bigtype body
+  targ <- sbvar $ Bound 0
+  return $ Arrow targ tbody
+
+{-bigtype (App proc arg) = (tyRes, env')-}
+  {-where (tyProc, penv) = bigtype proc-}
+        {-(tyArg, aenv) = bigtype arg-}
+        {-tyRes = undefined -- create fresh var-}
+        {-tenv = sunify tyProc $ Arrow tyArg tyRes-}
+        {-env = sunifyE penv aenv-}
+        {-env' = sunifyE env tenv-}
+
+-- data TermD_ lterm rterm =