module HM
( -- * Types
Type(..)
- , Term
+ , TypeScheme(..)
+ , Term(..)
+ , TypedTerm(..)
-- * Type inference
, algW
) where
+import Control.Monad.State
+
import HM.Term
import HM.Parser
type Substitution = TypeScheme -> TypeScheme
+type VarS a = State Int a
fresh :: TypeVarName
fresh = undefined
+--fresh = do
+-- n <- get
+-- "a" ++ show n
+
substitute :: TypeScheme -> TypeVarName -> TypeScheme -> TypeScheme
substitute = undefined
unify (TScheme (TypeVar a)) (TScheme (TypeVar b)) | a == b = Right id
unify a b = Left $ "cannot unify " ++ show a ++ " with " ++ show b
-algW :: HMTerm -> Either String TypeScheme
-algW (HMTerm (Var _) t) = Right t
-algW (HMTerm (Lambda x t) (TScheme p)) = do
- let v = TScheme (TypeVar fresh)
- np = substitute v x t
- unify p np
-algW (HMTerm (App u v) t) = do
- tu <- algW u
- tv <- algW v
- case tu of
- (TScheme (TypeFunction a b)) -> do
- unify a tv
- return b
- _ -> Left $ "cannot apply " ++ show tu ++ " to " ++ show tv
+algW :: TypedTerm -> Either String TypeScheme
+algW (TTerm (Var _) t) = Right t
+--algW (TTerm (Lam x t) (TScheme p)) = do
+-- let v = TScheme (TypeVar fresh)
+-- np = substitute v x t
+-- unify p np
+--algW (TTerm (App u v) t) = do
+-- tu <- algW u
+-- tv <- algW v
+-- case tu of
+-- (TScheme (TypeFunction a b)) -> do
+-- unify a tv
+-- return b
+-- _ -> Left $ "cannot apply " ++ show tu ++ " to " ++ show tv