a4-type-inference.hs

-- |
-- | CPSC 521 Tutorial: 06.04.2020
-- |
data TypeExpr v = Fun (TypeExpr v) (TypeExpr v)
                | Var String
                -- | Prod (LType v) (LType v)
                -- | List (LType v) (LType v)
                -- | Nat
                -- | Unit
                deriving (Show, Eq)

data TypeEquations v = TypeExists [v] [TypeEquations v]
                     | TypeEquation (TypeExpr v, TypeExpr v)

-- data Ctx v = Ctx { context :: [(String, LType v)], current :: v, counter :: v }
type Ctx v = ([(String, TypeExpr v)], v, v)
-- first v is the current type, second v is the counter
-- because v is enumerable, we can use it as a counter

data Lambda = LVar String
            | LAbs String Lambda
            | LApp Lambda Lambda
            | LFix Lambda
            deriving (Show, Eq)

buildTypeEquation
    :: Enum v => Lambda -> State (Ctx v) (Either (TypeEquations v) String)
buildTypeEquation t = case t of
    LVar v -> do
        (ctx, current, _) <- get
        case lookup v ctx of -- make sure that v has occured (occurence check)
            Just t -> return $ Left $ TypeEquation (Var current, Var t)
            Nothing ->
                return
                    $  Right "unknown variable: the var "
                    ++ v
                    ++ " doesn't occur in "
                    ++ show t
    LAbs s t -> do
        (ctx, current, count) <- get
        let (q, x, y) = (current, count, succ count)
        let next      = (succ . succ) count

        -- push (s, count) to context, current state is a fresh variable, increase counter()
        put ((s, x) : ctx, y, next)
        e <- buildTypeEquation t

        case e of
            Left e' -> do
                let left = Left $ TypeExists
                        [Var x, Var y]
                        [TypeEquation (Var q, Fun (Var x) (Var y)), e']
                return left
            Right err -> return $ Right err -- display better type error information (give context for something that went wrong)
    LApp t1 t2 -> do
        (ctx, q, z) <- get
        put (ctx, z, succ z)
        e1        <- buildTypeEquation t1

        (_, _, x) <- get
        put (ctx, x, succ x)
        e2 <- buildTypeEquation t2

        case (e1, e2) of
            (Left e1', Left e2') -> return $ Left $ TypeExists
                [Var x, Var z]
                [TypeEquation (Var z, Fun (Var x) (Var q)), e1', e2']

-- fix should be similar
    LFix t -> undefined