Experimental changes for System F

SystemF/SystemFBase.hs

 module SystemFBase where
-import Data.List 
+import Data.List
 
-data Variable = Z | STermVar Variable | STypeVar Variable deriving(Show, Eq)
+data Variable = Z | S Variable deriving(Show, Eq)
 
 data Term = TmVar Variable | TmAbs Term Type | TmApp Term Term | TmTApp Term Type | TmTAbs Term deriving(Show, Eq)
 
@@ -10,22 +10,18 @@ data Type = TyVar Variable | TyArr Type Type | TyAll Type | TyBase deriving(Show
 
 plus (Z) h = h
 plus h (Z) = h
-plus x1 (STermVar x2) = (STermVar (plus x1 x2))
-plus x1 (STypeVar x2) = (STypeVar (plus x1 x2))
+plus x1 (S x2) = (S (plus x1 x2))
 
 minus (Z) (Z) = (Z)
 minus (Z) _ = (error "You cannot substract zero with a positive number")
 minus result (Z) = result
-minus (STermVar h1) (STermVar h2) = (minus h1 h2)
-minus (STermVar h1) (STypeVar h2) = (error "differing namespace found in minus")
-minus (STypeVar h1) (STermVar h2) = (error "differing namespace found in minus")
-minus (STypeVar h1) (STypeVar h2) = (minus h1 h2)
+minus (S h1) (S h2) = (minus h1 h2)
 
 generateHnatTermVar 0 c = c
-generateHnatTermVar n c = (STermVar (generateHnatTermVar (n - 1) c))
+generateHnatTermVar n c = (S (generateHnatTermVar (n - 1) c))
 
 generateHnatTypeVar 0 c = c
-generateHnatTypeVar n c = (STypeVar (generateHnatTypeVar (n - 1) c))
+generateHnatTypeVar n c = (S (generateHnatTypeVar (n - 1) c))
 
 termshiftHelpplus d c (TmVar var) = if (var >= c) then (TmVar (plus var d)) else (TmVar var)
 
@@ -41,17 +37,17 @@ typeshiftHelpminus d c (TyVar var) = if (var >= c) then (TyVar (minus var d)) el
 
 termshiftminus d t = (termmap (termshiftHelpminus d) (typeshiftHelpminus d) (Z) t)
 
-typeshiftminus d t = (typemap (typeshiftHelpminus d) (Z) t)
+typeshiftminus d t =  (typemap (typeshiftHelpminus d) (Z) t)
 
 termmap onTermVar onTypeVar c (TmVar var) = (onTermVar c (TmVar var))
-termmap onTermVar onTypeVar c (TmAbs x t) = (TmAbs (termmap onTermVar onTypeVar (STermVar c) x) (typemap onTypeVar c t))
+termmap onTermVar onTypeVar c (TmAbs x t) = (TmAbs (termmap onTermVar onTypeVar (S c) x) (typemap onTypeVar c t))
 termmap onTermVar onTypeVar c (TmApp t1 t2) = (TmApp (termmap onTermVar onTypeVar c t1) (termmap onTermVar onTypeVar c t2))
 termmap onTermVar onTypeVar c (TmTApp t1 t) = (TmTApp (termmap onTermVar onTypeVar c t1) (typemap onTypeVar c t))
-termmap onTermVar onTypeVar c (TmTAbs t1) = (TmTAbs (termmap onTermVar onTypeVar (STypeVar c) t1))
+termmap onTermVar onTypeVar c (TmTAbs t1) = (TmTAbs (termmap onTermVar onTypeVar (S c) t1))
 
 typemap onTypeVar c (TyVar var) = (onTypeVar c (TyVar var))
 typemap onTypeVar c (TyArr t1 t2) = (TyArr (typemap onTypeVar c t1) (typemap onTypeVar c t2))
-typemap onTypeVar c (TyAll t1) = (TyAll (typemap onTypeVar (STypeVar c) t1))
+typemap onTypeVar c (TyAll t1) = (TyAll (typemap onTypeVar (S c) t1))
 typemap onTypeVar c (TyBase) = (TyBase)
 
 termSubstituteHelp sub c (TmVar var) = if (var == c) then (termshiftplus c sub) else (TmVar var)
@@ -65,20 +61,17 @@ typeSubstituteHelp sub c (TyVar var) = if (var == c) then (typeshiftplus c sub)
 typeTypeSubstitute sub orig t = (typemap (typeSubstituteHelp sub) orig t)
 
 freeVariablesTerm c (TmVar var) = if (var >= c) then [(minus var c)] else []
-freeVariablesTerm c (TmAbs x t) = (nub (concat [(freeVariablesTerm (STermVar c) x),(freeVariablesType c t)]))
+freeVariablesTerm c (TmAbs x t) = (nub (concat [(freeVariablesTerm (S c) x),(freeVariablesType c t)]))
 freeVariablesTerm c (TmApp t1 t2) = (nub (concat [(freeVariablesTerm c t1),(freeVariablesTerm c t2)]))
 freeVariablesTerm c (TmTApp t1 t) = (nub (concat [(freeVariablesTerm c t1),(freeVariablesType c t)]))
-freeVariablesTerm c (TmTAbs t1) = (nub (concat [(freeVariablesTerm (STypeVar c) t1)]))
+freeVariablesTerm c (TmTAbs t1) = (nub (concat [(freeVariablesTerm (S c) t1)]))
 
 freeVariablesType c (TyVar var) = if (var >= c) then [(minus var c)] else []
 freeVariablesType c (TyArr t1 t2) = (nub (concat [(freeVariablesType c t1),(freeVariablesType c t2)]))
-freeVariablesType c (TyAll t1) = (nub (concat [(freeVariablesType (STypeVar c) t1)]))
+freeVariablesType c (TyAll t1) = (nub (concat [(freeVariablesType (S c) t1)]))
 freeVariablesType c (TyBase) = (nub (concat [[]]))
 instance Ord Variable where
   compare (Z) (Z) = (EQ)
   compare (Z) _ = (LT)
   compare _ (Z) = (GT)
-  compare (STermVar h1) (STermVar h2) = (compare h1 h2)
-  compare (STermVar h1) (STypeVar h2) = (error "differing namespace found in compare")
-  compare (STypeVar h1) (STermVar h2) = (error "differing namespace found in compare")
-  compare (STypeVar h1) (STypeVar h2) = (compare h1 h2)
+  compare (S h1) (S h2) = (compare h1 h2)

SystemF/SystemFImpl.hs

@@ -7,6 +7,11 @@ data Env
              Env
   deriving (Show, Eq)
 
+nth :: Env -> Variable -> Maybe Env
+nth env Z = Just env
+nth (ETypeVar env) (S x) = nth env x
+nth (ETermVar _ env) (S x) = nth env x
+nth _ _ = Nothing
 
 isVal :: Term -> Bool
 isVal (TmAbs x t)              = True
@@ -16,10 +21,10 @@ isVal _ = False
 getTypeFromEnv :: Env -> Variable -> Either String Type
 getTypeFromEnv (ETermVar ty _) Z = return ty
 getTypeFromEnv _ Z = Left "wrong or no binding for term"
-getTypeFromEnv (ETermVar _ rest) (STermVar h) = getTypeFromEnv rest h
-getTypeFromEnv _ (STermVar h) = Left "wrong term binding"
-getTypeFromEnv (ETypeVar rest) (STypeVar h) = getTypeFromEnv rest h
-getTypeFromEnv _ (STypeVar h) = Left "No variable type"
+getTypeFromEnv (ETermVar _ rest) (S h) = getTypeFromEnv rest h
+getTypeFromEnv (ETypeVar rest) (S h) = getTypeFromEnv rest h
+getTypeFromEnv _ (S h) = Left "No variable type"
+
 --evaluation
 stepEval :: Term -> Maybe Term
 --function application
@@ -27,14 +32,14 @@ stepEval (TmApp (TmAbs t ty) t2)
   | isVal t2 =
     Just
       (termshiftminus
-         (STermVar Z)
-         (termTermSubstitute (termshiftplus (STermVar Z) t2) Z t))
+         (S Z)
+         (termTermSubstitute (termshiftplus (S Z) t2) Z t))
 --type application
 stepEval (TmTApp (TmTAbs t) ty) =
   Just
     (termshiftminus
-       (STypeVar Z)
-       (termTypeSubstitute (typeshiftplus (STypeVar Z) ty) Z t))
+       (S Z)
+       (termTypeSubstitute (typeshiftplus (S Z) ty) Z t))
 --R-CTXT
 stepEval (TmApp t1 t2)
   | isVal t1 = do
@@ -55,12 +60,23 @@ fullEval t = maybe t (fullEval) t2
   where
     t2 = stepEval t
 
+wellFormed :: Type -> Env -> Bool
+wellFormed (TyVar i) env       = case (nth env i) of
+  Nothing -> False
+  Just (ETermVar _ _) -> False
+  Just (ETypeVar _) -> True
+  Just Nil -> False
+wellFormed (TyArr ty1 ty2) env = wellFormed ty1 env && wellFormed ty2 env
+wellFormed (TyAll ty) env      = wellFormed ty (ETypeVar env)
+wellFormed (TyBase) env        = True
 
 typeOf :: Term -> Env -> Either String Type
 typeOf (TmVar nat) ctx = getTypeFromEnv ctx nat
-typeOf (TmAbs t ty) ctx = do
-  ty2 <- typeOf t (ETermVar ty ctx)
-  return (TyArr ty ty2)
+typeOf (TmAbs t ty) ctx =
+  if (wellFormed ty ctx) then do
+    ty2 <- typeOf t (ETermVar ty ctx)
+    return (TyArr ty ty2)
+  else Left (show ty ++ " is not well-formed")
 typeOf (TmApp t1 t2) ctx =
   case (typeOf t1 ctx) of
     Right (TyArr ty1 ty2) ->
@@ -72,15 +88,13 @@ typeOf (TmApp t1 t2) ctx =
         Left a -> Left a
     Left a -> Left a
     _ -> Left "arrow type expected"
-typeOf (TmTApp t ty) ctx =
-  case (typeOf t ctx) of
-    Right (TyAll ty2) ->
-      return
-        (typeshiftminus
-           (STypeVar Z)
-           (typeTypeSubstitute (typeshiftplus (STypeVar Z) ty) Z ty2))
-    Left a -> Left a
-    _ -> Left "not a type abstraction"
+typeOf (TmTApp (TmTAbs t) ty) ctx =
+  if (wellFormed ty ctx) then
+    typeOf
+      (termshiftminus
+        (S Z)
+        (termTypeSubstitute (typeshiftplus (S Z) ty) Z t)) ctx
+  else Left (show ty ++ " is not well-formed")
 typeOf (TmTAbs t) ctx = do
   ty <- typeOf t (ETypeVar ctx)
   return (TyAll ty)