--- /dev/null
+-- |
+-- Module : Lambda.Type
+-- Copyright : Tomáš Musil 2014
+-- License : BSD-3
+--
+-- Maintainer : tomik.musil@gmail.com
+-- Stability : experimental
+--
+-- Data types for Hindley-Milner types.
+
+
+module Lambda.Type
+ ( -- * Types
+ Type(..)
+ ) where
+
+import Lambda.Term
+
+type TypeVarName = String
+type TypeName = String
+
+data Type = Primitive TypeName | TypeVar TypeVarName | TypeFunction Type Type deriving (Show)
+data TypeScheme = TScheme Type | TSForAll TypeVarName TypeScheme deriving (Show)
+
+data HMTerm = HMTerm Term TypeScheme | HMLet VarName HMTerm HMTerm TypeScheme
+
+fresh :: TypeVarName
+fresh = undefined
+
+substitute :: TypeScheme -> TypeVarName -> TypeScheme -> TypeScheme
+substitute = undefined
+
+unify :: TypeScheme -> TypeScheme -> Either String TypeScheme
+unify = undefined
+
+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
+ return $ 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
+
+
+