From: Tomas Musil <tomik.musil@gmail.com>
Date: Tue, 30 Dec 2014 16:45:05 +0000 (+0100)
Subject: start work on alg W
X-Git-Url: http://git.tomasm.cz/fp.git/commitdiff_plain/8116a4989a7f9664ff2b4d07c705937f1aae1915?ds=inline;hp=dbb3af7ea8341e87b254dc94a613aec837b676b8

start work on alg W
---

diff --git a/src/Lambda/Type.hs b/src/Lambda/Type.hs
new file mode 100644
index 0000000..9ffdae7
--- /dev/null
+++ b/src/Lambda/Type.hs
@@ -0,0 +1,52 @@
+-- |
+-- 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
+  
+
+