diff --git a/hnix.cabal b/hnix.cabal index a77f01c..e88883f 100644 --- a/hnix.cabal +++ b/hnix.cabal @@ -2,7 +2,7 @@ -- -- see: https://github.com/sol/hpack -- --- hash: c645369523720ac4958529bc3855a8407d647e54309528d27f5e1f90e596bbee +-- hash: 07cd6a1b7913ff6635f99b4d896cdcbd096091580710fe2b350ebd5cedc52802 name: hnix version: 0.5.0 @@ -152,6 +152,7 @@ executable hnix , hnix , mtl , optparse-applicative + , pretty-show , repline , serialise , template-haskell diff --git a/main/Main.hs b/main/Main.hs index d1ec73f..37f3480 100644 --- a/main/Main.hs +++ b/main/Main.hs @@ -25,12 +25,15 @@ import Nix import Nix.Convert import qualified Nix.Eval as Eval import Nix.Lint +import qualified Nix.Type.Env as Env +import qualified Nix.Type.Infer as HM import Nix.Utils import Options.Applicative hiding (ParserResult(..)) import qualified Repl import System.FilePath import System.IO import Text.PrettyPrint.ANSI.Leijen hiding ((<$>)) +import qualified Text.Show.Pretty as PS main :: IO () main = do @@ -67,7 +70,13 @@ main = do else errorWithoutStackTrace) $ "Parse failed: " ++ show err Success expr -> do - when (check opts) $ + when (check opts) $ do + case HM.inferTop Env.empty [("it", stripAnnotation expr)] of + Left err -> + errorWithoutStackTrace $ "Type error: " ++ show err + Right ty -> + liftIO $ putStrLn $ "Type of expression: " ++ PS.ppShow ty + liftIO $ putStrLn $ runST $ runLintM opts . renderSymbolic =<< lint opts expr diff --git a/package.yaml b/package.yaml index aa6a239..b29d518 100644 --- a/package.yaml +++ b/package.yaml @@ -100,6 +100,7 @@ executables: dependencies: - hnix - aeson + - pretty-show - repline - haskeline diff --git a/src/Nix/Type/Infer.hs b/src/Nix/Type/Infer.hs index 42314e5..e11d7e5 100644 --- a/src/Nix/Type/Infer.hs +++ b/src/Nix/Type/Infer.hs @@ -1,7 +1,12 @@ +{-# LANGUAGE ExistentialQuantification #-} +{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE LambdaCase #-} -{-# LANGUAGE TypeSynonymInstances #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TypeSynonymInstances #-} {-# OPTIONS_GHC -Wno-name-shadowing #-} @@ -13,21 +18,34 @@ module Nix.Type.Infer ( ) where import Nix.Atoms +import Nix.Convert +import Nix.Eval (MonadEval(..)) +import qualified Nix.Eval as Eval import Nix.Expr.Types +import Nix.Expr.Types.Annotated +import Nix.Frames (Frame) +import Nix.Scope +import Nix.Thunk import qualified Nix.Type.Assumption as As import Nix.Type.Env import qualified Nix.Type.Env as Env import Nix.Type.Type +import Nix.Utils +import Control.Applicative +import Control.Arrow import Control.Monad.Except -import Control.Monad.State import Control.Monad.Reader +import Control.Monad.State import Data.Fix -import Data.List (delete, find, nub) +import Data.Foldable +import Data.List (delete, find, nub, intersect, (\\)) +import Data.Map (Map) import qualified Data.Map as Map import Data.Maybe (fromJust) import Data.Semigroup +import qualified Data.HashMap.Lazy as M import qualified Data.Set as Set import Data.Text (Text) @@ -36,13 +54,16 @@ import Data.Text (Text) ------------------------------------------------------------------------------- -- | Inference monad -type Infer a = (ReaderT - (Set.Set TVar) -- Monomorphic set - (StateT -- Inference state - InferState - (Except -- Inference errors - TypeError)) - a) -- Result +newtype Infer a = Infer + { getInfer :: + ReaderT (Set.Set TVar, Scopes Infer Judgment) -- Monomorphic set + (StateT InferState -- Inference state + (Except TypeError)) -- Inference errors + a -- Result + } + deriving (Functor, Applicative, Alternative, Monad, MonadPlus, MonadFix, + MonadReader (Set.Set TVar, Scopes Infer Judgment), + MonadState InferState, MonadError TypeError) -- | Inference state newtype InferState = InferState { count :: Int } @@ -51,15 +72,18 @@ newtype InferState = InferState { count :: Int } initInfer :: InferState initInfer = InferState { count = 0 } -data Constraint = EqConst Type Type - | ExpInstConst Type Scheme - | ImpInstConst Type (Set.Set TVar) Type - deriving (Show, Eq, Ord) +data Constraint + = EqConst Type Type + | EqConstOneOf Type [Type] + -- ^ The first type must unify with the second. For example, integer + -- could unify with integer, or a type variable. + | ExpInstConst Type Scheme + | ImpInstConst Type (Set.Set TVar) Type + deriving (Show, Eq, Ord) -newtype Subst = Subst (Map.Map TVar Type) +newtype Subst = Subst (Map TVar Type) deriving (Eq, Ord, Show, Semigroup, Monoid) - class Substitutable a where apply :: Subst -> a -> a @@ -69,17 +93,21 @@ instance Substitutable TVar where (TVar tv) = Map.findWithDefault t a s instance Substitutable Type where - apply _ (TCon a) = TCon a + apply _ (TCon a) = TCon a + apply s (TSet a) = TSet (M.map (apply s) a) + apply s (TSubSet a) = TSubSet (M.map (apply s) a) + apply s (TList a) = TList (map (apply s) a) apply (Subst s) t@(TVar a) = Map.findWithDefault t a s - apply s (t1 `TArr` t2) = apply s t1 `TArr` apply s t2 + 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 + 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 (EqConst t1 t2) = EqConst (apply s t1) (apply s t2) + apply s (EqConstOneOf t1 t2) = EqConstOneOf (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 @@ -95,6 +123,9 @@ class FreeTypeVars a where instance FreeTypeVars Type where ftv TCon{} = Set.empty ftv (TVar a) = Set.singleton a + ftv (TSet a) = Set.unions (map ftv (M.elems a)) + ftv (TSubSet a) = Set.unions (map ftv (M.elems a)) + ftv (TList a) = Set.unions (map ftv a) ftv (t1 `TArr` t2) = ftv t1 `Set.union` ftv t2 instance FreeTypeVars TVar where @@ -114,9 +145,10 @@ class ActiveTypeVars a where atv :: a -> Set.Set TVar instance ActiveTypeVars Constraint where - atv (EqConst t1 t2) = ftv t1 `Set.union` ftv t2 + atv (EqConst t1 t2) = ftv t1 `Set.union` ftv t2 + atv (EqConstOneOf 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 + atv (ExpInstConst t s) = ftv t `Set.union` ftv s instance ActiveTypeVars a => ActiveTypeVars [a] where atv = foldr (Set.union . atv) Set.empty @@ -128,6 +160,17 @@ data TypeError | UnboundVariable Text | Ambigious [Constraint] | UnificationMismatch [Type] [Type] + | forall s. Frame s => EvaluationError s + | InferenceAborted + +deriving instance Show TypeError + +instance Semigroup TypeError where + x <> _ = x + +instance Monoid TypeError where + mempty = InferenceAborted + mappend = (<>) ------------------------------------------------------------------------------- -- Inference @@ -135,11 +178,12 @@ data TypeError -- | Run the inference monad runInfer :: Infer a -> Either TypeError a -runInfer m = runExcept $ evalStateT (runReaderT m Set.empty) initInfer +runInfer m = + runExcept $ evalStateT (runReaderT (getInfer m) (Set.empty, emptyScopes)) initInfer inferType :: Env -> NExpr -> Infer (Subst, Type) inferType env ex = do - (as, cs, t) <- infer ex + Judgment 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] @@ -157,13 +201,13 @@ closeOver :: Type -> Scheme closeOver = normalize . generalize Set.empty extendMSet :: TVar -> Infer a -> Infer a -extendMSet x = local (Set.insert x) +extendMSet x = Infer . local (first (Set.insert x)) . getInfer letters :: [String] letters = [1..] >>= flip replicateM ['a'..'z'] fresh :: Infer Type -fresh = do +fresh = Infer $ do s <- get put s{count = count s + 1} return $ TVar $ TV (letters !! count s) @@ -178,74 +222,184 @@ 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 +unops :: Type -> NUnaryOp -> [Constraint] +unops u1 = \case + NNot -> [ EqConst u1 ( typeFun [typeBool, typeBool] ) ] + NNeg -> [ EqConstOneOf u1 [ typeFun [typeInt, typeInt] + , typeFun [typeFloat, typeFloat] ] ] -infer :: NExpr -> Infer (As.Assumption, [Constraint], Type) -infer = cata $ \case - NConstant (NInt _) -> return (As.empty, [], typeInt) - NConstant (NBool _) -> return (As.empty, [], typeBool) +binops :: Type -> NBinaryOp -> [Constraint] +binops u1 = \case + NApp -> [] -- this is handled separately - NSym x -> do - tv <- fresh - return (As.singleton x tv, [], tv) + -- Equality tells you nothing about the types, because any two types are + -- allowed. + NEq -> [] + NNEq -> [] - 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 - -- ) + NGt -> inequality + NGte -> inequality + NLt -> inequality + NLte -> inequality - NLet _binds _body -> undefined + NAnd -> [ EqConst u1 ( typeFun [typeBool, typeBool, typeBool]) ] + NOr -> [ EqConst u1 ( typeFun [typeBool, typeBool, typeBool]) ] + NImpl -> [ EqConst u1 ( typeFun [typeBool, typeBool, typeBool]) ] - -- 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 - -- ) + NConcat -> [ EqConstOneOf u1 [ typeFun [typeList, typeList, typeList] + , typeFun [typeList, typeNull, typeList] + , typeFun [typeNull, typeList, typeList] + ] ] - -- Fix e -> do - -- (as, cs, t) <- infer e - -- tv <- fresh - -- return (as, cs ++ [EqConst (tv `TArr` tv) t], tv) + NUpdate -> [ EqConstOneOf u1 [ typeFun [typeSet, typeSet, typeSet] + , typeFun [typeSet, typeNull, typeSet] + , typeFun [typeNull, typeSet, typeSet] + ] ] - 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 - ) + NPlus -> [ EqConstOneOf u1 [ typeFun [typeInt, typeInt, typeInt] + , typeFun [typeFloat, typeFloat, typeFloat] + , typeFun [typeInt, typeFloat, typeFloat] + , typeFun [typeFloat, typeInt, typeFloat] + , typeFun [typeString, typeString, typeString] + , typeFun [typePath, typePath, typePath] + , typeFun [typeString, typeString, typePath] + ] ] + NMinus -> arithmetic + NMult -> arithmetic + NDiv -> arithmetic + where + inequality = + [ EqConstOneOf u1 [ typeFun [typeInt, typeInt, typeBool] + , typeFun [typeFloat, typeFloat, typeBool] + , typeFun [typeInt, typeFloat, typeBool] + , typeFun [typeFloat, typeInt, typeBool] + ] ] - 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) + arithmetic = + [ EqConstOneOf u1 [ typeFun [typeInt, typeInt, typeInt] + , typeFun [typeFloat, typeFloat, typeFloat] + , typeFun [typeInt, typeFloat, typeFloat] + , typeFun [typeFloat, typeInt, typeFloat] + ] ] - 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 - ) +instance MonadThunk Judgment Judgment Infer where + thunk = id + force v f = f v + value = id - _ -> undefined +instance MonadEval Judgment Infer where + freeVariable var = do + tv <- fresh + return $ Judgment (As.singleton var tv) [] tv + + evaledSym _ = pure + + evalCurPos = + return $ Judgment As.empty [] $ TSet $ M.fromList + [ ("file", typePath) + , ("line", typeInt) + , ("col", typeInt) ] + + evalConstant c = return $ Judgment As.empty [] (go c) + where + go = \case + NInt _ -> typeInt + NFloat _ -> typeFloat + NBool _ -> typeBool + NNull -> typeNull + NUri _ -> typeUri + + evalString = const $ return $ Judgment As.empty [] typeString + evalLiteralPath = const $ return $ Judgment As.empty [] typePath + evalEnvPath = const $ return $ Judgment As.empty [] typePath + + evalUnary op (Judgment as1 cs1 t1) = do + tv <- fresh + return $ Judgment as1 (cs1 ++ unops (t1 `TArr` tv) op) tv + + evalBinary op (Judgment as1 cs1 t1) e2 = do + Judgment as2 cs2 t2 <- e2 + tv <- fresh + return $ Judgment + (as1 `As.merge` as2) + (cs1 ++ cs2 ++ binops (t1 `TArr` (t2 `TArr` tv)) op) + tv + + evalWith _scope _body = undefined-- pushWeakScope undefined body + + evalIf (Judgment as1 cs1 t1) t f = do + Judgment as2 cs2 t2 <- t + Judgment as3 cs3 t3 <- f + return $ Judgment + (as1 `As.merge` as2 `As.merge` as3) + (cs1 ++ cs2 ++ cs3 ++ [EqConst t1 typeBool, EqConst t2 t3]) + t2 + + evalAssert (Judgment as1 cs1 t1) body = do + Judgment as2 cs2 t2 <- body + return $ Judgment + (as1 `As.merge` as2) + (cs1 ++ cs2 ++ [EqConst t1 typeBool]) + t2 + + evalApp (Judgment as1 cs1 t1) e2 = do + Judgment as2 cs2 t2 <- e2 + tv <- fresh + return $ Judgment + (as1 `As.merge` as2) + (cs1 ++ cs2 ++ [EqConst t1 (t2 `TArr` tv)]) + tv + + evalAbs (Param x) e = do + tv@(TVar a) <- fresh + Judgment as cs t <- + extendMSet a (e (pure (Judgment (As.singleton x tv) [] tv))) + return $ Judgment + (as `As.remove` x) + (cs ++ [EqConst t' tv | t' <- As.lookup x as]) + (tv `TArr` t) + + evalAbs (ParamSet _x _variadic _mname) _e = undefined + + evalError = throwError . EvaluationError + +data Judgment = Judgment + { assumptions :: As.Assumption + , typeConstraints :: [Constraint] + , inferredType :: Type + } + deriving Show + +instance FromValue (Text, DList Text) Infer Judgment where + fromValueMay _ = return Nothing + fromValue _ = error "Unused" + +instance FromValue (AttrSet Judgment, AttrSet SourcePos) Infer Judgment where + -- jww (2018-04-30): How can we do this? TSet doesn't record enough information + fromValueMay (Judgment _ _ (TSet xs)) = + pure $ Just (M.mapWithKey (\k v -> Judgment (As.singleton k v) [] v) xs, M.empty) + fromValueMay _ = pure Nothing + fromValue = fromValueMay >=> \case + Just v -> pure v + Nothing -> pure (M.empty, M.empty) + +instance ToValue (AttrSet Judgment, AttrSet SourcePos) Infer Judgment where + toValue (xs, _) = pure $ Judgment + (foldr (As.merge . assumptions) As.empty xs) + (concatMap typeConstraints xs) + (TSet (M.map inferredType xs)) + +instance ToValue [Judgment] Infer Judgment where + toValue xs = pure $ Judgment + (foldr (As.merge . assumptions) As.empty xs) + (concatMap typeConstraints xs) + (TList (map inferredType xs)) + +instance ToValue Bool Infer Judgment where + toValue _ = pure $ Judgment As.empty [] typeBool + +infer :: NExpr -> Infer Judgment +infer = cata Eval.eval inferTop :: Env -> [(Text, NExpr)] -> Either TypeError Env inferTop env [] = Right env @@ -258,13 +412,19 @@ 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 (TVar a) = [a] + fv (TArr a b) = fv a ++ fv b fv (TCon _) = [] + fv (TSet a) = concatMap fv (M.elems a) + fv (TSubSet a) = concatMap fv (M.elems a) + fv (TList a) = concatMap fv a - normtype (TArr a b) = TArr (normtype a) (normtype b) - normtype (TCon a) = TCon a - normtype (TVar a) = + normtype (TArr a b) = TArr (normtype a) (normtype b) + normtype (TCon a) = TCon a + normtype (TSet a) = TSet (M.map normtype a) + normtype (TSubSet a) = TSubSet (M.map normtype a) + normtype (TList a) = TList (map normtype a) + normtype (TVar a) = case Prelude.lookup a ord of Just x -> TVar x Nothing -> error "type variable not in signature" @@ -293,6 +453,13 @@ 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 (TList _) (TList _) = return emptySubst +unifies (TSet b) (TSubSet s) + | M.keys b `intersect` M.keys s == M.keys s = return emptySubst +unifies (TSubSet s) (TSet b) + | M.keys b `intersect` M.keys s == M.keys s = return emptySubst +unifies (TSet s) (TSet b) + | null (M.keys b \\ M.keys s) = return emptySubst unifies (TArr t1 t2) (TArr t3 t4) = unifyMany [t1, t2] [t3, t4] unifies t1 t2 = throwError $ UnificationFail t1 t2 @@ -308,7 +475,8 @@ 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 (EqConst{}, _) = True + solvable (EqConstOneOf{}, _) = True solvable (ExpInstConst{}, _) = True solvable (ImpInstConst _t1 ms t2, cs) = Set.null ((ftv t2 `Set.difference` ms) `Set.intersection` atv cs) @@ -322,8 +490,21 @@ solve' (EqConst t1 t2, cs) = do su1 <- unifies t1 t2 su2 <- solve (apply su1 cs) return (su2 `compose` su1) + +solve' (EqConstOneOf t1 t2, cs) = do + -- jww (2018-04-30): Instead of picking the first that matches, collect all + -- that match into a 'TVariant [Type]' type, so that we can report that a + -- function like 'x: y: x + y' has type: forall a b. a one of integer, + -- float, string, b the same as a, or compatible, result is determined by + -- the finally decided type of the function (in this case, one of int, + -- float, string or path, based on the types of a and b). + su1 <- asum (map (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) diff --git a/src/Nix/Type/Type.hs b/src/Nix/Type/Type.hs index 6642332..839d48e 100644 --- a/src/Nix/Type/Type.hs +++ b/src/Nix/Type/Type.hs @@ -1,26 +1,41 @@ module Nix.Type.Type where -import Data.Text (Text) +import qualified Data.HashMap.Lazy as M +import Data.Text (Text) +import Nix.Utils newtype TVar = TV String deriving (Show, Eq, Ord) data Type - = TVar TVar -- type variable - | TCon String -- known type - | TArr Type Type -- type -> type + = TVar TVar -- type variable + | TCon String -- known type + | TSet (AttrSet Type) -- heterogenous map: { a = b; } + | TSubSet (AttrSet Type) -- subset of heterogenous map: { a = b; ... } + | TList [Type] -- heterogenous list + | TArr Type Type -- type -> type deriving (Show, Eq, Ord) data Scheme = Forall [TVar] Type -- forall a b. a -> b deriving (Show, Eq, Ord) -typeInt, typeFloat, typeBool, typePath, typeUri, typeNull :: Type -typeInt = TCon "Int" -typeFloat = TCon "Float" -typeBool = TCon "Bool" -typeString = TCon "String" -typePath = TCon "Path" -typeUri = TCon "URI" -typeNull = TCon "Null" +-- This models a set that unifies with any other set. +typeSet :: Type +typeSet = TSubSet M.empty + +typeList :: Type +typeList = TList [] + +typeFun :: [Type] -> Type +typeFun = foldr1 TArr + +typeInt, typeFloat, typeBool, typeString, typePath, typeUri, typeNull :: Type +typeInt = TCon "integer" +typeFloat = TCon "float" +typeBool = TCon "boolean" +typeString = TCon "string" +typePath = TCon "path" +typeUri = TCon "uri" +typeNull = TCon "null" type Name = Text