Add code for doing Hindley-Milner type inference, and a repl

This code was written by Stephen Diehl and Kwang Yul Seo, which they released
under an MIT license as the project poly_constraints:

    https://github.com/kseo/poly_constraints

The code is added to hnix right now as mainly a placeholder, and will need to
be modified before it can be used.

hnix.cabal

@@ -2,7 +2,7 @@
 --
 -- see: https://github.com/sol/hpack
 --
--- hash: 2c49222c1eda4bbca80475f682dd4cfaccf99ed3d4143ee2ad25f91171f21898
+-- hash: d8e569439f4d52d30cbcfda7126f2175566ff4b9550032b2b7f91eabacf8c04a
 
 name:           hnix
 version:        0.5.0
@@ -51,6 +51,10 @@ library
       Nix.StringOperations
       Nix.TH
       Nix.Thunk
+      Nix.Type.Assumption
+      Nix.Type.Env
+      Nix.Type.Infer
+      Nix.Type.Type
       Nix.Utils
       Nix.Value
       Nix.XML
@@ -101,6 +105,7 @@ library
 executable hnix
   main-is: Main.hs
   other-modules:
+      Repl
       Paths_hnix
   hs-source-dirs:
       main
@@ -118,6 +123,7 @@ executable hnix
     , hnix
     , mtl
     , optparse-applicative
+    , repline
     , serialise
     , template-haskell
     , text

main/Repl.hs

@@ -0,0 +1,180 @@
+{- This code was authored by:
+
+     Stephen Diehl
+     Kwang Yul Seo <kwangyul.seo@gmail.com>
+
+   It was made available under the MIT license. See the src/Nix/Type
+   directory for more details.
+-}
+
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE TypeSynonymInstances #-}
+
+{-# OPTIONS_GHC -Wno-unused-matches #-}
+{-# OPTIONS_GHC -Wno-unused-imports #-}
+
+module Repl where
+
+import           Nix.Type.Infer
+import qualified Nix.Type.Env as Env
+
+import qualified Data.Map as Map
+import           Data.Monoid
+import qualified Data.Text.Lazy as L
+import qualified Data.Text.Lazy.IO as L
+
+import           Control.Monad.Identity
+import           Control.Monad.State.Strict
+
+import           Data.List (isPrefixOf, foldl')
+import           Data.Text (unpack, pack)
+import qualified Data.Text as Text
+
+import           System.Exit
+import           System.Environment
+import           System.Console.Repline
+
+-------------------------------------------------------------------------------
+-- Types
+-------------------------------------------------------------------------------
+
+data TermEnv
+
+data IState = IState
+  { tyctx :: Env.Env  -- Type environment
+  , tmctx :: TermEnv  -- Value environment
+  }
+
+initState :: IState
+initState = IState Env.empty undefined
+
+type Repl a = HaskelineT (StateT IState IO) a
+hoistErr :: Show e => Either e a -> Repl a
+hoistErr (Right val) = return val
+hoistErr (Left err) = do
+  liftIO $ print err
+  abort
+
+-------------------------------------------------------------------------------
+-- Execution
+-------------------------------------------------------------------------------
+
+exec :: Bool -> L.Text -> Repl ()
+exec update source = do
+  -- Get the current interpreter state
+  st <- get
+
+  -- Parser ( returns AST )
+  -- mod <- hoistErr $ parseModule "<stdin>" source
+
+  -- Type Inference ( returns Typing Environment )
+  -- tyctx' <- hoistErr $ inferTop (tyctx st) mod
+
+  -- Create the new environment
+  -- let st' = st { tmctx = foldl' evalDef (tmctx st) mod
+  --              , tyctx = tyctx' <> tyctx st
+  --              }
+
+  -- Update the interpreter state
+  -- when update (put st')
+
+  -- If a value is entered, print it.
+  -- case lookup "it" mod of
+  --   Nothing -> return ()
+  --   Just ex -> do
+  --     let (val, _) = runEval (tmctx st') "it"  ex
+  --     showOutput (show val) st'
+
+  undefined
+
+showOutput :: String -> IState -> Repl ()
+showOutput arg st =
+  case Env.lookup "it" (tyctx st)  of
+    Just val -> liftIO $ putStrLn $ undefined -- ppsignature (arg, val)
+    Nothing -> return ()
+
+cmd :: String -> Repl ()
+cmd source = exec True (L.pack source)
+
+-------------------------------------------------------------------------------
+-- Commands
+-------------------------------------------------------------------------------
+
+-- :browse command
+browse :: [String] -> Repl ()
+browse _ = do
+  st <- get
+  undefined
+  -- liftIO $ mapM_ putStrLn $ ppenv (tyctx st)
+
+-- :load command
+load :: [String] -> Repl ()
+load args = do
+  contents <- liftIO $ L.readFile (unwords args)
+  exec True contents
+
+-- :type command
+typeof :: [String] -> Repl ()
+typeof args = do
+  st <- get
+  let arg = unwords args
+  case Env.lookup (pack arg) (tyctx st) of
+    Just val -> liftIO $ putStrLn $ undefined -- ppsignature (arg, val)
+    Nothing -> exec False (L.pack arg)
+
+-- :quit command
+quit :: a -> Repl ()
+quit _ = liftIO $ exitSuccess
+
+-------------------------------------------------------------------------------
+-- Interactive Shell
+-------------------------------------------------------------------------------
+
+-- Prefix tab completer
+defaultMatcher :: MonadIO m => [(String, CompletionFunc m)]
+defaultMatcher = [
+    (":load"  , fileCompleter)
+  --, (":type"  , values)
+  ]
+
+-- Default tab completer
+comp :: (Monad m, MonadState IState m) => WordCompleter m
+comp n = do
+  let cmds = [":load", ":type", ":browse", ":quit"]
+  Env.TypeEnv ctx <- gets tyctx
+  let defs = map unpack $ Map.keys ctx
+  return $ filter (isPrefixOf n) (cmds ++ defs)
+
+options :: [(String, [String] -> Repl ())]
+options = [
+    ("load"   , load)
+  , ("browse" , browse)
+  , ("quit"   , quit)
+  , ("type"   , Repl.typeof)
+  ]
+
+-------------------------------------------------------------------------------
+-- Entry Point
+-------------------------------------------------------------------------------
+
+completer :: CompleterStyle (StateT IState IO)
+completer = Prefix (wordCompleter comp) defaultMatcher
+
+shell :: Repl a -> IO ()
+shell pre = flip evalStateT initState
+     $ evalRepl "Poly> " cmd options completer pre
+
+-------------------------------------------------------------------------------
+-- Toplevel
+-------------------------------------------------------------------------------
+
+main :: IO ()
+main = do
+  args <- getArgs
+  case args of
+    []      -> shell (return ())
+    [fname] -> shell (load [fname])
+    ["test", fname] -> shell (load [fname] >> browse [] >> quit ())
+    _ -> putStrLn "invalid arguments"

package.yaml

@@ -67,6 +67,7 @@ executables:
     main: Main.hs
     dependencies:
       - hnix
+      - repline
 
 tests:
   hnix-tests:

src/Nix/Lint.hs

@@ -44,6 +44,7 @@ import           Nix.Expr
 import           Nix.Scope
 import           Nix.Stack
 import           Nix.Thunk
+-- import           Nix.Type.Infer
 import           Nix.Utils
 
 data TAtom

src/Nix/Type/Assumption.hs

@@ -0,0 +1,44 @@
+module Nix.Type.Assumption (
+  Assumption(..),
+  empty,
+  lookup,
+  remove,
+  extend,
+  keys,
+  merge,
+  mergeAssumptions,
+  singleton,
+) where
+
+import Prelude hiding (lookup)
+
+import Nix.Type.Type
+
+import Data.Foldable
+
+newtype Assumption = Assumption { assumptions :: [(Name, Type)] }
+  deriving (Eq, Show)
+
+empty :: Assumption
+empty = Assumption []
+
+extend :: Assumption -> (Name, Type) -> Assumption
+extend (Assumption a) (x, s) = Assumption ((x, s) : a)
+
+remove :: Assumption -> Name -> Assumption
+remove (Assumption a) var = Assumption (filter (\(n, _) -> n /= var) a)
+
+lookup :: Name -> Assumption -> [Type]
+lookup key (Assumption a) = map snd (filter (\(n, _) -> n == key) a)
+
+merge :: Assumption -> Assumption -> Assumption
+merge (Assumption a) (Assumption b) = Assumption (a ++ b)
+
+mergeAssumptions :: [Assumption] -> Assumption
+mergeAssumptions = foldl' merge empty
+
+singleton :: Name -> Type -> Assumption
+singleton x y = Assumption [(x, y)]
+
+keys :: Assumption -> [Name]
+keys (Assumption a) = map fst a

src/Nix/Type/Env.hs

@@ -0,0 +1,65 @@
+module Nix.Type.Env (
+  Env(..),
+  empty,
+  lookup,
+  remove,
+  extend,
+  extends,
+  merge,
+  mergeEnvs,
+  singleton,
+  keys,
+  fromList,
+  toList,
+) where
+
+import Prelude hiding (lookup)
+
+import Nix.Type.Type
+
+import Data.Foldable hiding (toList)
+import qualified Data.Map as Map
+
+-------------------------------------------------------------------------------
+-- Typing Environment
+-------------------------------------------------------------------------------
+
+newtype Env = TypeEnv { types :: Map.Map Name Scheme }
+  deriving (Eq, Show)
+
+empty :: Env
+empty = TypeEnv Map.empty
+
+extend :: Env -> (Name, Scheme) -> Env
+extend env (x, s) = env { types = Map.insert x s (types env) }
+
+remove :: Env -> Name -> Env
+remove (TypeEnv env) var = TypeEnv (Map.delete var env)
+
+extends :: Env -> [(Name, Scheme)] -> Env
+extends env xs = env { types = Map.union (Map.fromList xs) (types env) }
+
+lookup :: Name -> Env -> Maybe Scheme
+lookup key (TypeEnv tys) = Map.lookup key tys
+
+merge :: Env -> Env -> Env
+merge (TypeEnv a) (TypeEnv b) = TypeEnv (Map.union a b)
+
+mergeEnvs :: [Env] -> Env
+mergeEnvs = foldl' merge empty
+
+singleton :: Name -> Scheme -> Env
+singleton x y = TypeEnv (Map.singleton x y)
+
+keys :: Env -> [Name]
+keys (TypeEnv env) = Map.keys env
+
+fromList :: [(Name, Scheme)] -> Env
+fromList xs = TypeEnv (Map.fromList xs)
+
+toList :: Env -> [(Name, Scheme)]
+toList (TypeEnv env) = Map.toList env
+
+instance Monoid Env where
+  mempty = empty
+  mappend = merge

src/Nix/Type/Infer.hs

@@ -0,0 +1,328 @@
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE TypeSynonymInstances #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+
+{-# OPTIONS_GHC -Wno-name-shadowing #-}
+
+module Nix.Type.Infer (
+  Constraint(..),
+  TypeError(..),
+  Subst(..),
+  inferTop
+) where
+
+import           Nix.Atoms
+import           Nix.Expr.Types
+import qualified Nix.Type.Assumption as As
+import           Nix.Type.Env
+import qualified Nix.Type.Env as Env
+import           Nix.Type.Type
+
+import           Control.Monad.Except
+import           Control.Monad.State
+import           Control.Monad.Reader
+
+import           Data.Fix
+import           Data.List (delete, find, nub)
+import qualified Data.Map as Map
+import           Data.Maybe (fromJust)
+import qualified Data.Set as Set
+import           Data.Text (Text)
+
+-------------------------------------------------------------------------------
+-- Classes
+-------------------------------------------------------------------------------
+
+-- | Inference monad
+type Infer a = (ReaderT
+                  (Set.Set TVar)  -- Monomorphic set
+                  (StateT         -- Inference state
+                  InferState
+                  (Except         -- Inference errors
+                    TypeError))
+                  a)              -- Result
+
+-- | Inference state
+newtype InferState = InferState { count :: Int }
+
+-- | Initial inference state
+initInfer :: InferState
+initInfer = InferState { count = 0 }
+
+data Constraint = EqConst Type Type
+                | ExpInstConst Type Scheme
+                | ImpInstConst Type (Set.Set TVar) Type
+                deriving (Show, Eq, Ord)
+
+newtype Subst = Subst (Map.Map TVar Type)
+  deriving (Eq, Ord, Show, Monoid)
+
+
+class Substitutable a where
+  apply :: Subst -> a -> a
+
+instance Substitutable TVar where
+  apply (Subst s) a = tv
+    where t = TVar a
+          (TVar tv) = Map.findWithDefault t a s
+
+instance Substitutable Type where
+  apply _ (TCon a)       = TCon a
+  apply (Subst s) t@(TVar a) = Map.findWithDefault t a s
+  apply s (t1 `TArr` t2) = apply s t1 `TArr` apply s t2
+
+instance Substitutable Scheme where
+  apply (Subst s) (Forall as t)   = Forall as $ apply s' t
+                            where s' = Subst $ foldr Map.delete s as
+
+instance Substitutable Constraint where
+   apply s (EqConst t1 t2) = EqConst (apply s t1) (apply s t2)
+   apply s (ExpInstConst t sc) = ExpInstConst (apply s t) (apply s sc)
+   apply s (ImpInstConst t1 ms t2) = ImpInstConst (apply s t1) (apply s ms) (apply s t2)
+
+instance Substitutable a => Substitutable [a] where
+  apply = map . apply
+
+instance (Ord a, Substitutable a) => Substitutable (Set.Set a) where
+  apply = Set.map . apply
+
+
+class FreeTypeVars a where
+  ftv :: a -> Set.Set TVar
+
+instance FreeTypeVars Type where
+  ftv TCon{}         = Set.empty
+  ftv (TVar a)       = Set.singleton a
+  ftv (t1 `TArr` t2) = ftv t1 `Set.union` ftv t2
+
+instance FreeTypeVars TVar where
+  ftv = Set.singleton
+
+instance FreeTypeVars Scheme where
+  ftv (Forall as t) = ftv t `Set.difference` Set.fromList as
+
+instance FreeTypeVars a => FreeTypeVars [a] where
+  ftv   = foldr (Set.union . ftv) Set.empty
+
+instance (Ord a, FreeTypeVars a) => FreeTypeVars (Set.Set a) where
+  ftv   = foldr (Set.union . ftv) Set.empty
+
+
+class ActiveTypeVars a where
+  atv :: a -> Set.Set TVar
+
+instance ActiveTypeVars Constraint where
+  atv (EqConst t1 t2) = ftv t1 `Set.union` ftv t2
+  atv (ImpInstConst t1 ms t2) = ftv t1 `Set.union` (ftv ms `Set.intersection` ftv t2)
+  atv (ExpInstConst t s) = ftv t `Set.union` ftv s
+
+instance ActiveTypeVars a => ActiveTypeVars [a] where
+  atv = foldr (Set.union . atv) Set.empty
+
+
+data TypeError
+  = UnificationFail Type Type
+  | InfiniteType TVar Type
+  | UnboundVariable Text
+  | Ambigious [Constraint]
+  | UnificationMismatch [Type] [Type]
+
+-------------------------------------------------------------------------------
+-- Inference
+-------------------------------------------------------------------------------
+
+-- | Run the inference monad
+runInfer :: Infer a -> Either TypeError a
+runInfer m = runExcept $ evalStateT (runReaderT m Set.empty) initInfer
+
+inferType :: Env -> NExpr -> Infer (Subst, Type)
+inferType env ex = do
+  (as, cs, t) <- infer ex
+  let unbounds = Set.fromList (As.keys as) `Set.difference` Set.fromList (Env.keys env)
+  unless (Set.null unbounds) $ throwError $ UnboundVariable (Set.findMin unbounds)
+  let cs' = [ExpInstConst t s | (x, s) <- Env.toList env, t <- As.lookup x as]
+  subst <- solve (cs ++ cs')
+  return (subst, apply subst t)
+
+-- | Solve for the toplevel type of an expression in a given environment
+inferExpr :: Env -> NExpr -> Either TypeError Scheme
+inferExpr env ex = case runInfer (inferType env ex) of
+  Left err -> Left err
+  Right (subst, ty) -> Right $ closeOver $ apply subst ty
+
+-- | Canonicalize and return the polymorphic toplevel type.
+closeOver :: Type -> Scheme
+closeOver = normalize . generalize Set.empty
+
+extendMSet :: TVar -> Infer a -> Infer a
+extendMSet x = local (Set.insert x)
+
+letters :: [String]
+letters = [1..] >>= flip replicateM ['a'..'z']
+
+fresh :: Infer Type
+fresh = do
+    s <- get
+    put s{count = count s + 1}
+    return $ TVar $ TV (letters !! count s)
+
+instantiate ::  Scheme -> Infer Type
+instantiate (Forall as t) = do
+    as' <- mapM (const fresh) as
+    let s = Subst $ Map.fromList $ zip as as'
+    return $ apply s t
+
+generalize :: Set.Set TVar -> Type -> Scheme
+generalize free t  = Forall as t
+    where as = Set.toList $ ftv t `Set.difference` free
+
+ops :: NBinaryOp -> Type
+ops NPlus  = typeInt `TArr` (typeInt `TArr` typeInt)
+ops NMult  = typeInt `TArr` (typeInt `TArr` typeInt)
+ops NMinus = typeInt `TArr` (typeInt `TArr` typeInt)
+ops NEq    = typeInt `TArr` (typeInt `TArr` typeBool)
+ops _      = undefined
+
+infer :: NExpr -> Infer (As.Assumption, [Constraint], Type)
+infer = cata $ \case
+  NConstant (NInt _)  -> return (As.empty, [], typeInt)
+  NConstant (NBool _) -> return (As.empty, [], typeBool)
+
+  NSym x -> do
+    tv <- fresh
+    return (As.singleton x tv, [], tv)
+
+  NAbs _x e -> do
+    _tv@(TVar a) <- fresh
+    (_as, _cs, _t) <- extendMSet a e
+    undefined
+    -- return ( as `As.remove` x
+    --        , cs ++ [EqConst t' tv | t' <- As.lookup x as]
+    --        , tv `TArr` t
+    --        )
+
+  NLet _binds _body -> undefined
+
+  -- NLet x e1 e2 -> do
+  --   (as1, cs1, t1) <- infer e1
+  --   (as2, cs2, t2) <- infer e2
+  --   ms <- ask
+  --   return ( as1 `As.merge` as2 `As.remove` x
+  --          , cs1 ++ cs2 ++ [ImpInstConst t' ms t1 | t' <- As.lookup x as2]
+  --          , t2
+  --          )
+
+  -- Fix e -> do
+  --   (as, cs, t) <- infer e
+  --   tv <- fresh
+  --   return (as, cs ++ [EqConst (tv `TArr` tv) t], tv)
+
+  NBinary NApp e1 e2 -> do
+    (as1, cs1, t1) <- e1
+    (as2, cs2, t2) <- e2
+    tv <- fresh
+    return ( as1 `As.merge` as2
+           , cs1 ++ cs2 ++ [EqConst t1 (t2 `TArr` tv)]
+           , tv
+           )
+
+  NBinary op e1 e2 -> do
+    (as1, cs1, t1) <- e1
+    (as2, cs2, t2) <- e2
+    tv <- fresh
+    let u1 = t1 `TArr` (t2 `TArr` tv)
+        u2 = ops op
+    return (as1 `As.merge` as2, cs1 ++ cs2 ++ [EqConst u1 u2], tv)
+
+  NIf cond tr fl -> do
+    (as1, cs1, t1) <- cond
+    (as2, cs2, t2) <- tr
+    (as3, cs3, t3) <- fl
+    return ( as1 `As.merge` as2 `As.merge` as3
+           , cs1 ++ cs2 ++ cs3 ++ [EqConst t1 typeBool, EqConst t2 t3]
+           , t2
+           )
+
+  _ -> undefined
+
+inferTop :: Env -> [(Text, NExpr)] -> Either TypeError Env
+inferTop env [] = Right env
+inferTop env ((name, ex):xs) = case inferExpr env ex of
+  Left err -> Left err
+  Right ty -> inferTop (extend env (name, ty)) xs
+
+normalize :: Scheme -> Scheme
+normalize (Forall _ body) = Forall (map snd ord) (normtype body)
+  where
+    ord = zip (nub $ fv body) (map TV letters)
+
+    fv (TVar a)   = [a]
+    fv (TArr a b) = fv a ++ fv b
+    fv (TCon _)    = []
+
+    normtype (TArr a b) = TArr (normtype a) (normtype b)
+    normtype (TCon a)   = TCon a
+    normtype (TVar a)   =
+      case Prelude.lookup a ord of
+        Just x -> TVar x
+        Nothing -> error "type variable not in signature"
+
+-------------------------------------------------------------------------------
+-- Constraint Solver
+-------------------------------------------------------------------------------
+
+-- | The empty substitution
+emptySubst :: Subst
+emptySubst = mempty
+
+-- | Compose substitutions
+compose :: Subst -> Subst -> Subst
+(Subst s1) `compose` (Subst s2) = Subst $ Map.map (apply (Subst s1)) s2 `Map.union` s1
+
+unifyMany :: [Type] -> [Type] -> Infer Subst
+unifyMany [] [] = return emptySubst
+unifyMany (t1 : ts1) (t2 : ts2) =
+  do su1 <- unifies t1 t2
+     su2 <- unifyMany (apply su1 ts1) (apply su1 ts2)
+     return (su2 `compose` su1)
+unifyMany t1 t2 = throwError $ UnificationMismatch t1 t2
+
+unifies :: Type -> Type -> Infer Subst
+unifies t1 t2 | t1 == t2 = return emptySubst
+unifies (TVar v) t = v `bind` t
+unifies t (TVar v) = v `bind` t
+unifies (TArr t1 t2) (TArr t3 t4) = unifyMany [t1, t2] [t3, t4]
+unifies t1 t2 = throwError $ UnificationFail t1 t2
+
+bind ::  TVar -> Type -> Infer Subst
+bind a t | t == TVar a     = return emptySubst
+         | occursCheck a t = throwError $ InfiniteType a t
+         | otherwise       = return (Subst $ Map.singleton a t)
+
+occursCheck ::  FreeTypeVars a => TVar -> a -> Bool
+occursCheck a t = a `Set.member` ftv t
+
+nextSolvable :: [Constraint] -> (Constraint, [Constraint])
+nextSolvable xs = fromJust (find solvable (chooseOne xs))
+  where
+    chooseOne xs = [(x, ys) | x <- xs, let ys = delete x xs]
+    solvable (EqConst{}, _) = True
+    solvable (ExpInstConst{}, _) = True
+    solvable (ImpInstConst _t1 ms t2, cs) =
+        Set.null ((ftv t2 `Set.difference` ms) `Set.intersection` atv cs)
+
+solve :: [Constraint] -> Infer Subst
+solve [] = return emptySubst
+solve cs = solve' (nextSolvable cs)
+
+solve' :: (Constraint, [Constraint]) -> Infer Subst
+solve' (EqConst t1 t2, cs) = do
+  su1 <- unifies t1 t2
+  su2 <- solve (apply su1 cs)
+  return (su2 `compose` su1)
+solve' (ImpInstConst t1 ms t2, cs) =
+  solve (ExpInstConst t1 (generalize ms t2) : cs)
+solve' (ExpInstConst t s, cs) = do
+  s' <- instantiate s
+  solve (EqConst t s' : cs)

src/Nix/Type/LICENSE

@@ -0,0 +1,19 @@
+Copyright (c) 2014-2015, Stephen Diehl
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to
+deal in the Software without restriction, including without limitation the
+rights to use, copy, modify, merge, publish, distribute, sublicense, and/or
+sell copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in
+all copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
+FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS
+IN THE SOFTWARE.

src/Nix/Type/README.md

@@ -0,0 +1,81 @@
+Poly
+====
+
+A simple ML dialect with definitions, let polymorphism and a fixpoint operator.
+Uses syntax directed HM type inference.
+
+To compile and run:
+
+```shell
+$ cabal run
+```
+
+Usage:
+
+```ocaml
+Poly> let i x = x;
+i : forall a. a -> a
+
+Poly> i 3
+3
+
+Poly> :type i
+i : forall a. a -> a
+
+Poly> :type let k x y = x;
+k : forall a b. a -> b -> a
+
+Poly> :type let s f g x = f x (g x)
+s : forall a b c. ((a -> b) -> c -> a) -> (a -> b) -> c -> b
+
+Poly> :type let on g f = \x y -> g (f x) (f y)
+on : forall a b c. (a -> a -> b) -> (c -> a) -> c -> c -> b
+
+Poly> :type let let_bound = i (i i) (i 3)
+let_bound : Int
+
+Poly> :type let compose f g = \x -> f (g x)
+compose : forall a b c. (a -> b) -> (c -> a) -> c -> b
+
+Poly> let rec factorial n = 
+  if (n == 0) 
+  then 1
+  else (n * (factorial (n-1)));
+```
+
+Notes
+=====
+
+Top level let declarations are syntactic sugar for nested lambda. For example: 
+
+```ocaml
+let add x y = x + y;
+```
+
+Is semantically equivalent to:
+
+```ocaml
+let add = \x -> \y -> x + y;
+```
+
+Top level Let-rec declarations are syntactic sugar for use of the ``fix``
+operator. For example:
+
+```ocaml
+let rec factorial n = if (n == 0) then 1 else (n * (factorial (n-1)));
+```
+Is semantically equivalent to:
+
+```ocaml
+let factorial = fix (\factorial n -> if (n == 0) then 1 else (n * (factorial (n-1))));
+```
+
+License
+=======
+
+Released under MIT license.
+
+Authors
+=======
+Stephen Diehl
+Kwang Yul Seo <kwangyul.seo@gmail.com>

src/Nix/Type/Type.hs

@@ -0,0 +1,21 @@
+module Nix.Type.Type where
+
+import Data.Text (Text)
+
+newtype TVar = TV String
+  deriving (Show, Eq, Ord)
+
+data Type
+  = TVar TVar
+  | TCon String
+  | TArr Type Type
+  deriving (Show, Eq, Ord)
+
+data Scheme = Forall [TVar] Type
+  deriving (Show, Eq, Ord)
+
+typeInt, typeBool :: Type
+typeInt  = TCon "Int"
+typeBool = TCon "Bool"
+
+type Name = Text