infernu-0.0.0.1: src/Infernu/Infer.hs
{-# LANGUAGE CPP #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TupleSections #-}
module Infernu.Infer
( runTypeInference
, test
, Pretty(..)
, pretty
, getAnnotations
, minifyVars
, TypeError
)
where
import Control.Monad (foldM, forM)
import qualified Data.Graph.Inductive as Graph
import Data.Map.Lazy (Map)
import qualified Data.Map.Lazy as Map
import Data.Maybe (mapMaybe)
import Data.Set (Set)
import qualified Data.Set as Set
import Prelude hiding (foldr, mapM, sequence)
import Data.List (intercalate)
import Infernu.Prelude
import qualified Infernu.Builtins.Operators as Operators
import Infernu.InferState
import Infernu.Lib (safeLookup)
import Infernu.Log
import Infernu.Pretty
import Infernu.Types
import Infernu.Unify (unify, unifyAll, unifyPending, unifyPredsL, unifyRowPropertyBiased, unifyl)
getQuantificands :: TypeScheme -> [TVarName]
getQuantificands (TScheme tvars _) = tvars
getAnnotations :: Exp a -> [a]
getAnnotations = foldr (:) []
----------------------------------------------------------------------
closeRowList :: TRowList Type -> TRowList Type
closeRowList (TRowProp n t rest) = TRowProp n t (closeRowList rest)
closeRowList (TRowEnd _) = TRowEnd Nothing
-- TODO: Handle TRowRec, by defining a new named type in which all row types within are closed (recursively).
-- | Replaces a top-level open row type with the closed equivalent.
-- >>> pretty $ closeRow (Fix $ TRow $ TRowProp "a" (schemeEmpty $ Fix $ TRow $ TRowProp "aa" (schemeEmpty $ Fix $ TBody TNumber) (TRowEnd (Just $ RowTVar 1))) (TRowEnd (Just $ RowTVar 2)))
-- "{a: {aa: Number, ..b}}"
-- >>> pretty $ closeRow (Fix $ TFunc [Fix $ TRow $ TRowProp "a" (schemeEmpty $ Fix $ TRow $ TRowProp "aa" (schemeEmpty $ Fix $ TBody TNumber) (TRowEnd Nothing)) (TRowEnd Nothing)] (Fix $ TBody TString))
-- "{a: {aa: Number}}.(() -> String)"
-- >>> pretty $ closeRow (Fix $ TFunc [Fix $ TRow $ TRowProp "a" (schemeEmpty $ Fix $ TRow $ TRowProp "a.a" (schemeEmpty $ Fix $ TBody TNumber) (TRowEnd (Just $ RowTVar 1))) (TRowEnd (Just $ RowTVar 2))] (Fix $ TBody TString))
-- "{a: {a.a: Number, ..b}, ..c}.(() -> String)"
closeRow :: Type -> Type
closeRow (Fix (TRow r)) = Fix . TRow $ closeRowList r
closeRow t = t
----------------------------------------------------------------------
-- For efficiency reasons, types list is returned in reverse order.
accumInfer :: TypeEnv -> [Exp Source] -> Infer [(QualType, Exp (Source, QualType))]
accumInfer env =
do traceLog ("accumInfer: env: " ++ pretty env)
foldM accumInfer' []
where accumInfer' types expr =
do (t, e) <- inferType env expr
return ((t,e):types)
inferType :: TypeEnv -> Exp Source -> Infer (QualType, Exp (Source, QualType))
inferType env expr = do
traceLog (">> " ++ pretty expr ++ " -- env: " ++ pretty env)
(t, e) <- inferType' env expr
unifyPending
s <- getMainSubst
st <- getState
traceLog (">> " ++ pretty expr ++ " -- inferred :: " ++ pretty (applySubst s t))
traceLog (" infer state: " ++ prettyTab 3 st)
return (applySubst s t, fmap (applySubst s) e)
inferType' :: TypeEnv -> Exp Source -> Infer (QualType, Exp (Source, QualType))
inferType' _ (ELit a lit) = do
let t = Fix $ TBody $ case lit of
LitNumber _ -> TNumber
LitBoolean _ -> TBoolean
LitString _ -> TString
LitRegex{} -> TRegex
LitUndefined -> TUndefined
LitNull -> TNull
return (qualEmpty t, ELit (a, qualEmpty t) lit)
inferType' env (EVar a n) =
do t <- instantiateVar a n env
return (t, EVar (a, t) n)
inferType' env (EAbs a argNames e2) =
do argTypes <- forM argNames (const $ Fix . TBody . TVar <$> fresh)
env' <- foldM (\e (n, t) -> addVarScheme e n $ schemeEmpty t) env $ zip argNames argTypes
(t1, e2') <- inferType env' e2
pred' <- unifyPredsL a $ qualPred t1
let t = TQual pred' $ Fix $ TFunc argTypes (qualType t1)
return (t, EAbs (a, t) argNames e2')
inferType' env (EApp a e1 eArgs) =
do tvar <- Fix . TBody . TVar <$> fresh
(t1, e1') <- inferType env e1
traceLog $ "EApp: Inferred type for func expr: " ++ pretty t1
argsTE <- accumInfer env eArgs
traceLog $ "EApp: Inferred types for func args: " ++ intercalate ", " (map pretty argsTE)
let rargsTE = reverse argsTE
tArgs = map fst rargsTE
eArgs' = map snd rargsTE
preds = concatMap qualPred $ t1:tArgs
unify a (qualType t1) (Fix $ TFunc (map qualType tArgs) tvar)
traceLog $ "Inferred preds: " ++ intercalate ", " (map pretty preds)
tvar' <- do pred' <- unifyPredsL a preds
tvarSubsted <- applyMainSubst tvar
return $ TQual pred' tvarSubsted
traceLog ("Inferred func application: " ++ pretty tvar')
return (tvar', EApp (a, tvar') e1' eArgs')
inferType' env (ENew a e1 eArgs) =
do (t1, e1') <- inferType env e1
argsTE <- accumInfer env eArgs
thisT <- Fix . TBody . TVar <$> fresh
resT <- Fix . TBody . TVar <$> fresh
let rargsTE = reverse argsTE
tArgs = thisT : map (qualType . fst) rargsTE
eArgs' = map snd rargsTE
preds = concatMap qualPred $ t1 : map fst argsTE
unify a (qualType t1) (Fix $ TFunc tArgs resT)
-- constrain 'this' to be a row type:
rowConstraintVar <- RowTVar <$> fresh
unify a (Fix . TRow . TRowEnd $ Just rowConstraintVar) thisT
-- close the row type
resolvedThisT <- applyMainSubst thisT -- otherwise closeRow will not do what we want.
unify a thisT (closeRow resolvedThisT)
-- TODO: If the function returns a row type, it should be the resulting type; other it should be 'thisT'
preds' <- unifyPredsL a preds
let thisT' = TQual preds' thisT
return (thisT', ENew (a, thisT') e1' eArgs')
inferType' env (ELet a n e1 e2) =
do recType <- Fix . TBody . TVar <$> fresh
recEnv <- addVarScheme env n $ schemeEmpty recType
(t1, e1') <- inferType recEnv e1
unify a (qualType t1) recType
t' <- generalize e1 env t1
env' <- addVarScheme env n t'
(t2, e2') <- inferType env' e2
preds' <- unifyPredsL a $ concatMap qualPred [t1, t2]
let resT = TQual preds' $ qualType t2
return (resT, ELet (a, resT) n e1' e2')
-- | Handling of mutable variable assignment.
-- | Prevent mutable variables from being polymorphic.
inferType' env expr@(EAssign a n expr1 expr2) =
do traceLog $ "EAssign: " ++ pretty expr
lvalueScheme <- getVarScheme a n env `failWithM` throwError a ("Unbound variable: " ++ show n ++ " in assignment " ++ pretty expr1)
traceLog $ "EAssign lvalueScheme: " ++ pretty lvalueScheme
lvalueT <- instantiate lvalueScheme
(rvalueT, expr1') <- inferType env expr1
unify a (qualType lvalueT) (qualType rvalueT)
(tRest, expr2') <- inferType env expr2
traceLog $ "EAssign lvalueT: " ++ pretty lvalueT
traceLog $ "EAssign Invoking unifyAllInstances on scheme: " ++ pretty lvalueScheme
instancePreds <- unifyAllInstances a $ getQuantificands lvalueScheme
preds <- unifyPredsL a $ concat $ (instancePreds:) $ map qualPred [lvalueT, rvalueT, tRest] -- TODO should update variable scheme
-- update the variable scheme, removing perhaps some quantified tvars
varId <- getVarId n env `failWith` throwError a ("Unbound variable: '" ++ show n ++ "'")
updatedScheme <- generalize expr1 env (schemeType lvalueScheme)
_ <- setVarScheme env n updatedScheme varId
--
let tRest' = TQual preds $ qualType tRest
return (tRest', EAssign (a, tRest') n expr1' expr2')
inferType' env (EPropAssign a objExpr n expr1 expr2) =
do (objT, objExpr') <- inferType env objExpr
(rvalueT, expr1') <- inferType env expr1
rowTailVar <- RowTVar <$> fresh
let rvalueScheme = schemeFromQual rvalueT -- generalize expr1 env rvalueT
rank0Unify = unify a (qualType objT) $ Fix . TRow $ TRowProp n rvalueScheme $ TRowEnd (Just rowTailVar)
case unFix (qualType objT) of
TRow trowList ->
case Map.lookup n . fst $ flattenRow trowList of
-- lvalue is known to be a property with some scheme
Just lvalueScheme ->
do generalizedRvalue <- generalize expr1 env rvalueT
unifyRowPropertyBiased a rank0Unify (lvalueScheme, generalizedRvalue)
Nothing -> rank0Unify
_ -> rank0Unify
(expr2T, expr2') <- inferType env expr2 -- TODO what about the pred
--traceLog "EPropAssign - applying unifyAllInstances"
--instancePred <- unifyAllInstances a [getRowTVar rowTailVar]
preds <- unifyPredsL a $ concatMap qualPred [objT, rvalueT, expr2T] -- TODO review
let tRes = TQual preds $ qualType expr2T
return (tRes, EPropAssign (a, tRes) objExpr' n expr1' expr2')
inferType' env (EIndexAssign a eArr eIdx expr1 expr2) =
do (tArr, eArr') <- inferType env eArr
elemTVarName <- fresh
arrTVarName <- fresh
idxTVarName <- fresh
let elemType = Fix . TBody . TVar $ elemTVarName
-- unify a (qualType tArr) $ Fix $ TCons TArray [elemType]
unify a (qualType tArr) $ Fix $ TBody $ TVar arrTVarName
(tId, eIdx') <- inferType env eIdx
unify a (qualType tId) $ Fix $ TBody $ TVar idxTVarName
(tExpr1, expr1') <- inferType env expr1
unify a (qualType tExpr1) elemType
-- TODO: BUG here, because elemTVarName never has any var instances due to the predicates usage here.
--traceLog "EIndexAssign - applying unifyAllInstances"
--instancePred <- unifyAllInstances a [elemTVarName]
(tExpr2, expr2') <- inferType env expr2
let curPred = indexAccessPred arrTVarName elemTVarName idxTVarName
preds <- unifyPredsL a $ concat $ ([curPred]:) $ map qualPred [tArr, tId, tExpr1, tExpr2] -- TODO review
let tRes = TQual preds $ qualType tExpr2
return (tRes , EIndexAssign (a, tRes) eArr' eIdx' expr1' expr2')
inferType' env (EArray a exprs) =
do tv <- Fix . TBody . TVar <$> fresh
te <- accumInfer env exprs
let types = map (qualType . fst) te
unifyl unify a $ zip (tv:types) types
let t = qualEmpty $ Fix $ TCons TArray [tv]
return (t, EArray (a,t) $ map snd te)
inferType' env (ETuple a exprs) =
do te <- accumInfer env exprs
let t = TQual (concatMap (qualPred . fst) te) $ Fix . TCons TTuple . reverse $ map (qualType . fst) te
return (t, ETuple (a,t) $ map snd te)
inferType' env (EStringMap a exprs') =
do let exprs = map snd exprs'
elemType <- Fix . TBody . TVar <$> fresh
te <- accumInfer env exprs
let types = map (qualType . fst) te
unifyAll a $ elemType:types
allPreds <- unifyPredsL a . concatMap qualPred $ map fst te
let t = TQual { qualPred = allPreds, qualType = Fix $ TCons TStringMap [elemType] }
return (t, EStringMap (a,t) $ zip (map fst exprs') (map snd te))
inferType' env (ERow a isOpen propExprs) =
do te <- accumInfer env $ map snd propExprs
endVar <- RowTVar <$> fresh
let propNamesTypes = zip propExprs (reverse $ map fst te)
rowEnd' = TRowEnd $ if isOpen then Just endVar else Nothing
accumRowProp' row ((propName, propExpr), propType) =
do ts <- generalize propExpr env propType
return $ TRowProp propName ts row
rowType <- qualEmpty . Fix . TRow <$> foldM accumRowProp' rowEnd' propNamesTypes
return (rowType, ERow (a,rowType) isOpen $ zip (map fst propExprs) (map snd te))
inferType' env (ECase a eTest eBranches) =
do (eType, eTest') <- inferType env eTest
infPatterns <- accumInfer env $ map (ELit a . fst) eBranches
let patternTypes = map (qualType . fst) infPatterns
unifyAll a $ (qualType eType):patternTypes
infBranches <- accumInfer env $ map snd eBranches
let branchTypes = map (qualType . fst) infBranches
unifyAll a branchTypes
allPreds <- unifyPredsL a . concatMap qualPred $ eType : (map fst infPatterns) ++ (map fst infBranches)
let tRes = TQual { qualPred = allPreds, qualType = qualType . fst $ head infBranches } -- TODO unsafe head
return (tRes, ECase (a, tRes) eTest' $ zip (map fst eBranches) (map snd infBranches))
inferType' env (EProp a eObj propName) =
do (tObj, eObj') <- inferType env eObj
rowVar <- RowTVar <$> fresh
propTypeScheme <- schemeEmpty . Fix . TBody . TVar <$> fresh
--case unFix (qualType tObj) of
-- TRow tRowList -> --TODO
-- _ -> schemeEmpty . Fix . TBody . TVar <$> fresh
unify a (Fix . TRow $ TRowProp propName propTypeScheme $ TRowEnd (Just rowVar)) (qualType tObj)
propType <- instantiate propTypeScheme
return (propType, EProp (a,propType) eObj' propName)
inferType' env (EIndex a eArr eIdx) =
do (tArr, eArr') <- inferType env eArr
elemTVarName <- fresh
arrTVarName <- fresh
idxTVarName <- fresh
unify a (qualType tArr) (Fix $ TBody $ TVar arrTVarName)
(tId, eIdx') <- inferType env eIdx
unify a (qualType tId) (Fix $ TBody $ TVar idxTVarName)
let elemType' = qualEmpty $ Fix $ TBody $ TVar elemTVarName
curPred = indexAccessPred arrTVarName elemTVarName idxTVarName
preds <- unifyPredsL a $ (curPred:) $ concatMap qualPred [tArr, tId] -- TODO review
let tRes = TQual preds $ qualType elemType'
return (tRes, EIndex (a, tRes) eArr' eIdx')
indexAccessPred :: TVarName -> TVarName -> TVarName -> TPred Type
indexAccessPred arrTVarName elemTVarName idxTVarName =
let --elemType = mkv elemTVarName
mkv = Fix . TBody . TVar
in
TPredIsIn (ClassName "Indexable") (Fix $ TCons TTuple
[ mkv arrTVarName
, mkv idxTVarName
, mkv elemTVarName
])
-- Fix $ TCons TArray [elemType])
-- , TPredIsIn "Index"
-- `mkAnd` TPredEq idxTVarName (Fix $ TBody TNumber))
-- `mkOr` (TPredEq arrTVarName (Fix $ TCons TStringMap [elemType])
-- `mkAnd` TPredEq idxTVarName (Fix $ TBody TString))
unifyAllInstances :: Source -> [TVarName] -> Infer [TPred Type]
unifyAllInstances a tvs = do
m <- getVarInstances
traceLog $ "unifyAllInstances: " ++ pretty a ++ " Unifying all instances of tvars: " ++ intercalate ", " (map pretty tvs)
let equivalenceSets = map Set.fromList $ filter (not . null) $ map (mapMaybe $ Graph.lab m) $ map (flip Graph.bfs m) tvs
unifyAll' equivs =
do let equivsL = Set.toList equivs
qequivsL = map qualType equivsL
traceLog $ "unifyAllInstances - equivalence:" ++ pretty qequivsL
unifyAll a qequivsL
return $ concatMap qualPred equivsL
pred' <- concat <$> mapM unifyAll' equivalenceSets
unifyPredsL a pred'
createEnv :: Map EVarName TypeScheme -> Infer (Map EVarName VarId)
createEnv builtins = foldM addVarScheme' Map.empty $ Map.toList builtins
where allTVars :: TypeScheme -> Set TVarName
allTVars (TScheme qvars t) = freeTypeVars t `Set.union` Set.fromList qvars
addVarScheme' :: Map EVarName VarId -> (EVarName, TypeScheme) -> Infer (Map EVarName VarId)
addVarScheme' m (name, tscheme) =
do allocNames <- forM (Set.toList $ allTVars tscheme)
$ \tvName -> (tvName,) <$> fresh
addVarScheme m name $ mapVarNames (safeLookup allocNames) tscheme
typeInference :: Map EVarName TypeScheme -> Exp Source -> Infer (Exp (Source, QualType))
typeInference builtins e =
do env <- createEnv builtins
(_t, e') <- inferType env e
return e'
----------------------------------------------------------------------
--
-- | Mutable variable being assigned incompatible types:
--
-- >>> let p = emptySource
-- >>> let fun args = EAbs p ("this":args)
-- >>> let var = EVar p
-- >>> let let' = ELet p
-- >>> let tuple = ETuple p
-- >>> let lit = ELit p
-- >>> let app a b = EApp p a [lit LitUndefined, b]
-- >>> let assign = EAssign p
-- >>> let array = EArray p
--
-- x is known to have type forall a. a -> a, and to have been used in a context requiring bool -> bool (e.g. `x True`)
--
-- we now try to assign x := \y -> 2
--
-- This should fail because it "collapses" x to be Number -> Number which is not compatible with bool -> bool
--
-- >>> test $ let' "x" (fun ["z"] (var "z")) (let' "y" (tuple [app (var "x") (lit (LitNumber 2)), app (var "x") (lit (LitBoolean True))]) (assign "x" (fun ["y"] (lit (LitNumber 0))) (tuple [var "x", var "y"])))
-- ":1:1*: Error: Could not unify: Number with Boolean"
--
-- The following should succeed because x is immutable and thus polymorphic:
--
-- >>> test $ let' "x" (fun ["z"] (var "z")) (let' "y" (tuple [app (var "x") (lit (LitNumber 2)), app (var "x") (lit (LitBoolean True))]) (tuple [var "x", var "y"]))
-- "(c.(d -> d), (Number, Boolean))"
--
-- The following should fail because x is mutable and therefore a monotype:
--
-- >>> test $ let' "x" (fun ["z"] (var "z")) (let' "y" (tuple [app (var "x") (lit (LitNumber 2)), app (var "x") (lit (LitBoolean True))]) (assign "x" (fun ["z1"] (var "z1")) (tuple [var "x", var "y"])))
-- ":1:1*: Error: Could not unify: Number with Boolean"
--
-- The following should also succeed because "x" is only ever used like this: (x True). The second assignment to x is: x := \z1 -> False, which is specific but matches the usage. Note that x's type is collapsed to: Boolean -> Boolean.
--
-- >>> test $ let' "x" (fun ["z"] (var "z")) (let' "y" (app (var "x") (lit (LitBoolean True))) (assign "x" (fun ["z1"] (lit (LitBoolean False))) (tuple [var "x", var "y"])))
-- "((Boolean -> Boolean), Boolean)"
--
-- | Tests a setter for x being called with something more specific than x's original definition:
-- >>> :{
-- >>> test $ let'
-- >>> "x" (fun ["a"] (var "a"))
-- >>> (let' "setX"
-- >>> (fun ["v"]
-- >>> (let'
-- >>> "_" (assign "x" (var "v") (var "x")) (lit (LitBoolean False))))
-- >>> (let'
-- >>> "_" (app (var "setX") (fun ["a"] (lit (LitString "a"))))
-- >>> (app (var "x") (lit (LitBoolean True)))))
-- >>> :}
-- ":1:1*: Error: Could not unify: String with Boolean"
--
-- >>> test $ tuple [lit (LitBoolean True), lit (LitNumber 2)]
-- "(Boolean, Number)"
--
-- >>> test $ let' "id" (fun ["x"] (var "x")) (assign "id" (fun ["y"] (var "y")) (var "id"))
-- "a.(b -> b)"
--
-- >>> test $ let' "id" (fun ["x"] (var "x")) (assign "id" (lit (LitBoolean True)) (var "id"))
-- ":1:1*: Error: Could not unify: a.(b -> b) with Boolean"
--
-- >>> test $ let' "x" (lit (LitBoolean True)) (assign "x" (lit (LitBoolean False)) (var "x"))
-- "Boolean"
--
-- >>> test $ let' "x" (lit (LitBoolean True)) (assign "x" (lit (LitNumber 3)) (var "x"))
-- ":1:1*: Error: Could not unify: Boolean with Number"
--
-- >>> test $ let' "x" (array [lit (LitBoolean True)]) (var "x")
-- "[Boolean]"
--
-- >>> test $ let' "x" (array [lit $ LitBoolean True, lit $ LitBoolean False]) (var "x")
-- "[Boolean]"
--
-- >>> test $ let' "x" (array []) (assign "x" (array []) (var "x"))
-- "[a]"
--
-- >>> test $ let' "x" (array [lit $ LitBoolean True, lit $ LitNumber 2]) (var "x")
-- ":1:1*: Error: Could not unify: Number with Boolean"
--
-- >>> test $ let' "id" (fun ["x"] (let' "y" (var "x") (var "y"))) (app (var "id") (var "id"))
-- "c.(d -> d)"
--
-- >>> test $ let' "id" (fun ["x"] (let' "y" (var "x") (var "y"))) (app (app (var "id") (var "id")) (lit (LitNumber 2)))
-- "Number"
--
-- >>> test $ let' "id" (fun ["x"] (app (var "x") (var "x"))) (var "id")
-- ":1:1*: Error: Occurs check failed: a in (a -> b)"
--
-- >>> test $ fun ["m"] (let' "y" (var "m") (let' "x" (app (var "y") (lit (LitBoolean True))) (var "x")))
-- "a.((Boolean -> b) -> b)"
--
-- >>> test $ app (lit (LitNumber 2)) (lit (LitNumber 2))
-- ":1:1*: Error: Could not unify: Number with (Number -> a)"
--
-- EAssign tests
-- >>> test $ let' "x" (fun ["y"] (lit (LitNumber 0))) (assign "x" (fun ["y"] (var "y")) (var "x"))
-- "a.(Number -> Number)"
--
-- >>> test $ let' "x" (fun ["y"] (var "y")) (assign "x" (fun ["y"] (lit (LitNumber 0))) (var "x"))
-- "a.(Number -> Number)"
--
-- >>> test $ let' "x" (fun ["y"] (var "y")) (tuple [app (var "x") (lit (LitNumber 2)), app (var "x") (lit (LitBoolean True))])
-- "(Number, Boolean)"
--
-- >>> test $ let' "x" (fun ["y"] (var "y")) (app (var "x") (var "x"))
-- "c.(d -> d)"
--
-- >>> test $ let' "x" (fun ["a"] (var "a")) (let' "getX" (fun ["v"] (var "x")) (let' "setX" (fun ["v"] (let' "_" (assign "x" (var "v") (var "x")) (lit (LitBoolean True)))) (let' "_" (app (var "setX") (fun ["a"] (lit (LitString "a")))) (var "getX"))))
-- "e.(f -> d.(String -> String))"
test :: Exp Source -> String
test e = case runTypeInference e of
Left err -> pretty err
Right expr -> pretty $ snd . head . getAnnotations . minifyVars $ expr
runTypeInference :: Exp Source -> Either TypeError (Exp (Source, QualType))
runTypeInference e = runInfer $ typeInference Operators.builtins e