gistfile1.txt

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE StandaloneDeriving #-}

import qualified Data.Map as Map
import Control.Monad.State
import Control.Monad.Except
import Data.Monoid

type Var = String

data Expr
  = Var Var
  | App Expr Expr
  | Lam Var Expr
  | Let Var Expr Expr
  | Lit Lit
  | If Expr Expr Expr
  | Fix Expr
  | Op Binop Expr Expr
  deriving (Show, Eq, Ord)

data Lit
  = LInt Integer
  | LBool Bool
  deriving (Show, Eq, Ord)

data Binop = Add | Sub | Mul | Eql
  deriving (Eq, Ord, Show)

data Program = Program [Decl] Expr deriving Eq

type Decl = (String, Expr)

newtype TVar = TV String
  deriving (Show, Eq, Ord)

data Type
  = TVar TVar
  | TCon String
  | TArr Type Type
  deriving (Show, Eq, Ord)

typeInt, typeBool :: Type
typeInt  = TCon "Int"
typeBool = TCon "Bool"

data Scheme = Forall [TVar] Type deriving (Show,Eq,Ord)
newtype TypeEnv = TypeEnv (Map.Map Var Scheme) deriving Semigroup

deriving instance Show TypeEnv
deriving instance Monoid TypeEnv


extend :: TypeEnv -> (Var, Scheme) -> TypeEnv
extend (TypeEnv env) (x, s) = TypeEnv $ Map.insert x s env

testExtend = show (extend env ("x",Forall [] typeBool))
               where env =  TypeEnv (Map.singleton ("f") (Forall [TV "a"] (TArr (TVar $ TV "a") typeInt)))



data Unique = Unique { count :: Int }

data TypeError
  = UnificationFail Type Type
  | InfiniteType TVar Type
  | UnboundVariable String
  a
type Infer = ExceptT TypeError (State Unique)
type Subst = Map.Map TVar Type

main :: IO ()
main = print (testExtend)