diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -18,6 +18,7 @@ - Whitespace insensitive syntax - Type annotations to support first-class modules and schema validation use cases - Built-in support for ints, double, bools, chars and lists +- Support for fixed-points (useful for dynamic binding), but without recursive records. ## Installation @@ -263,7 +264,7 @@ ## A data-exchange format with schemas -We could use Expresso as a lightweight data-exchange format (i.e. JSON with types). But how might be validate terms against a schema? +We could use Expresso as a lightweight data-exchange format (i.e. JSON with types). But how might we validate terms against a schema? A simple type annotation ` : ` , will not suffice for "schema validation". For example, consider this attempt at validating an integer against a schema that permits everything: diff --git a/expresso.cabal b/expresso.cabal --- a/expresso.cabal +++ b/expresso.cabal @@ -1,5 +1,5 @@ Name: expresso -Version: 0.1.2.0 +Version: 0.1.2.2 Cabal-Version: >= 1.10 License: BSD3 License-File: LICENSE diff --git a/src/Expresso/Eval.hs b/src/Expresso/Eval.hs --- a/src/Expresso/Eval.hs +++ b/src/Expresso/Eval.hs @@ -50,7 +50,6 @@ where import Control.Monad.Except -import Data.Foldable (foldrM) import Data.HashMap.Strict (HashMap) import Data.IORef import Data.Ord diff --git a/src/Expresso/Pretty.hs b/src/Expresso/Pretty.hs --- a/src/Expresso/Pretty.hs +++ b/src/Expresso/Pretty.hs @@ -24,7 +24,8 @@ import Data.String import Text.PrettyPrint.Leijen ( Doc, (<+>), (), angles, braces, brackets , comma, dot, dquotes, empty, hcat, hsep, indent - , int, integer, double, parens, space, text, string, vcat) + , int, integer, double, parens, space, text, string + , squotes, vcat) import qualified Text.PrettyPrint.Leijen as PP instance IsString Doc where diff --git a/src/Expresso/Type.hs b/src/Expresso/Type.hs --- a/src/Expresso/Type.hs +++ b/src/Expresso/Type.hs @@ -13,7 +13,6 @@ {-# LANGUAGE TupleSections #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} -{-# LANGUAGE TypeSynonymInstances #-} {-# LANGUAGE ViewPatterns #-} -- | @@ -35,10 +34,14 @@ import Data.Foldable (fold) import Data.IntMap (IntMap) import Data.Map (Map) +import Data.Maybe import Data.Set (Set) +import qualified Data.Graph as Graph +import qualified Data.List as L import qualified Data.Map as M -import qualified Data.IntMap as IM import qualified Data.Set as S +import qualified Data.Tree as Tree +import qualified Data.IntMap as IM import Text.Parsec (SourcePos) import Text.Parsec.Pos (newPos) @@ -155,19 +158,29 @@ deleteSynonym name (Synonyms m) = Synonyms $ M.delete name m --- | Checks for duplicate synonym names and free variables. +-- | Checks for duplicate synonym names, loops/cycles and free variables. insertSynonyms :: MonadError String m => [SynonymDecl] -> Synonyms -> m Synonyms -insertSynonyms ss (Synonyms m) = - Synonyms <$> foldM f m ss +insertSynonyms ss (Synonyms m) = do + m' <- foldM f m ss + case findLoops m' of + ([],[]) -> return $ Synonyms m' + (selfLoops,loops) -> + throwError . unlines $ + [ "Recursive synonym definitions are not supported: " <> loop + | loop <- selfLoops + ] ++ + [ "Mutually recursive synonym definitions are not supported: " <> L.intercalate "," nms + | nms <- loops + ] where f m syn | Just syn' <- M.lookup (synonymName syn) m -- check that it's not a benign re-import of the same synonym - , (fields syn /= fields syn') = + , fields syn /= fields syn' = throwError $ unwords [ "Duplicate synonyms with name" , "'" ++ synonymName syn ++ "'" @@ -190,6 +203,38 @@ -- strip positional annotations fields (SynonymDecl _ name vars body) = (name, vars, stripAnn body) + -- Find loops in the graphs (recursive synonyms are not allowed). + findLoops m = (selfLoops, loops) + where + -- Find self-loops + selfLoops = mapMaybe ((`M.lookup` vertexToName) . fst) + . filter (uncurry (==)) + $ edges + + -- We look for all the strongly connected components that + -- are not singleton lists. + loops = mapMaybe (mapM (`M.lookup` vertexToName)) + . filter ((>1) . length) + . map Tree.flatten + . Graph.scc + . Graph.buildG (0, M.size m) + $ edges + + edges = [ (v1, v2) -- edge + | (nm, v1) <- M.toList nameToVertex + , nm' <- maybe [] (S.toList . namesFromBody) $ M.lookup nm m + , Just v2 <- [M.lookup nm' nameToVertex] + ] + + vertexToName = M.fromList $ zip [0..] (M.keys m) + nameToVertex = M.fromList $ zip (M.keys m) [0..] + + namesFromBody = cata alg . stripAnn . synonymBody where + alg :: TypeF (Set Name) -> Set Name + alg (TSynonymF n ns) = S.insert n (S.unions ns) + alg t = fold t + + instance View TypeF Type where proj = left . unFix inj e = Fix (e :*: K dummyPos) @@ -245,13 +290,13 @@ instance Types Type where ftv = cata alg . stripAnn where - alg :: TypeF (Set TyVar) -> (Set TyVar) + alg :: TypeF (Set TyVar) -> Set TyVar alg (TForAllF vs t) = t S.\\ S.fromList vs alg (TVarF v) = S.singleton v alg e = fold e meta = cata alg . stripAnn where - alg :: TypeF (Set MetaTv) -> (Set MetaTv) + alg :: TypeF (Set MetaTv) -> Set MetaTv alg (TMetaVarF v) = S.singleton v alg e = fold e @@ -277,7 +322,7 @@ -- when quantifying an outer forall, we can avoid these inner ones. tyVarBndrs :: Type -> Set TyVar tyVarBndrs = cata alg . stripAnn where - alg :: TypeF (Set TyVar) -> (Set TyVar) + alg :: TypeF (Set TyVar) -> Set TyVar alg (TForAllF vs t) = t <> S.fromList vs alg (TFunF arg res) = arg <> res alg _ = S.empty @@ -289,15 +334,14 @@ -> Map Name Type -> Type alg (TForAllF vs f :*: K p) m = - let m' = foldr M.delete m (map tyvarName vs) + let m' = foldr (M.delete . tyvarName) m vs in Fix (TForAllF vs (f m') :*: K p) alg (TVarF v :*: K p) m = - case M.lookup (tyvarName v) m of - Nothing -> Fix (TVarF v :*: K p) - Just t -> t + fromMaybe (Fix (TVarF v :*: K p)) + $ M.lookup (tyvarName v) m alg e m = Fix $ fmap ($m) e - m = M.fromList $ (map tyvarName tvs) `zip` ts + m = M.fromList $ map tyvarName tvs `zip` ts newtype Subst = Subst { unSubst :: IntMap Type } deriving (Show) @@ -314,12 +358,12 @@ removeFromSubst :: [MetaTv] -> Subst -> Subst removeFromSubst vs (Subst m) = - Subst $ foldr IM.delete m (map metaUnique vs) + Subst $ foldr (IM.delete . metaUnique) m vs -- | apply s1 and then s2 -- NB: order is important composeSubst :: Subst -> Subst -> Subst -composeSubst s1 s2 = Subst $ (IM.map (apply s1) $ unSubst s2) `IM.union` unSubst s1 +composeSubst s1 s2 = Subst $ IM.map (apply s1) (unSubst s2) `IM.union` unSubst s1 instance Semigroup Subst where (<>) = composeSubst @@ -430,7 +474,9 @@ precType :: Type -> Precedence precType (TForAll _ _) = topPrec precType (TFun _ _) = arrPrec -precType (TSynonym _ _) = tcPrec +precType (TSynonym _ ts) + | null ts = atomicPrec + | otherwise = tcPrec precType _ = atomicPrec -- | Print with parens if precedence arg > precedence of type itself @@ -468,10 +514,14 @@ ppRowTail _ v = mempty <+> "|" <+> ppType v ppEntry (l, t) = text l <+> ":" <+> ppType t +ppRowLabels :: Type -> Doc +ppRowLabels row = + hcat $ map squotes (L.intersperse comma (map text . M.keys . rowToMap $ row)) + ppForAll :: ([TyVar], Type) -> Doc ppForAll (vars, t) | null vars = ppType' topPrec t - | otherwise = "forall" <+> (hsep $ map (ppType . TVar) vars) <> dot + | otherwise = "forall" <+> hsep (map (ppType . TVar) vars) <> dot <> (let cs = concatMap ppConstraint vars in if null cs then mempty else space <> (parensList cs <+> "=>")) <+> ppType' topPrec t diff --git a/src/Expresso/TypeCheck.hs b/src/Expresso/TypeCheck.hs --- a/src/Expresso/TypeCheck.hs +++ b/src/Expresso/TypeCheck.hs @@ -4,10 +4,7 @@ {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE PatternGuards #-} -{-# LANGUAGE TupleSections #-} {-# LANGUAGE TypeOperators #-} -{-# LANGUAGE TypeSynonymInstances #-} -{-# LANGUAGE ViewPatterns #-} {-# OPTIONS_GHC -fmax-pmcheck-iterations=10000000 #-} -- | @@ -78,8 +75,8 @@ -> Synonyms -> TIState -> (Either String a, TIState) -runTI t tEnv syns tState = - runState (runReaderT (runExceptT t) (TIEnv tEnv syns)) tState +runTI t tEnv syns = + runState (runReaderT (runExceptT t) (TIEnv tEnv syns)) -- | Initial state of the inference engine. initTIState :: TIState @@ -125,7 +122,7 @@ TypeEnv env <- asks tiTypeEnv case M.lookup name env of Just s -> return s - Nothing -> throwError $ show $ + Nothing -> throwError . show $ ppPos pos <+> ": unbound variable:" <+> text name extendEnv :: M.Map Name Sigma -> TI a -> TI a @@ -154,7 +151,7 @@ mkSubsts p mvs = zipWith mkSubst mvs (prefixBndrs L.\\ usedBndrs) where - prefixBndrs = [p] : [ (p:show i) | i <- [(1::Integer)..]] + prefixBndrs = [p] : [ p : show i | i <- [(1::Integer)..]] mkSubst mv name = (mv, TyVar Bound name p (metaConstraint mv)) @@ -241,10 +238,10 @@ ] unifyRow :: Type -> Type -> TI Subst -unifyRow row1@TRowExtend{} row2@TRowEmpty = throwError' $ - [ ppPos (getAnn row1) <+> ": unexpected row label(s)" - <+> hcat (L.intersperse comma (map text . M.keys . rowToMap $ row1)) - , "at" <+> ppPos (getAnn row2) +unifyRow row1@TRowExtend{} row2@TRowEmpty = throwError' + [ "Cannot unify the row at" <+> ppPos (getAnn row1) + , "with the row at" <+> ppPos (getAnn row2) + , "due to the row label(s)" <+> ppRowLabels row1 ] unifyRow row1@(TRowExtend label1 fieldTy1 rowTail1) row2@TRowExtend{} = do -- apply side-condition to ensure termination @@ -307,11 +304,11 @@ = case S.toList (ls `S.intersection` ls') of [] | Nothing <- mv -> return s1 | Just r1 <- mv -> do - let c = ls `S.union` (labelsFrom r1) + let c = ls `S.union` labelsFrom r1 r2 <- newMetaVar pos (CRow c) 'r' let s2 = r1 |-> r2 return $ s1 <> s2 - labels -> throwError $ show $ + labels -> throwError . show $ ppPos pos <+> ": repeated label(s):" <+> sepBy comma (map text labels) where @@ -324,14 +321,17 @@ rewriteRow :: Pos -> Pos -> Type -> Label -> TI (Type, Type, Subst) rewriteRow pos1 pos2 (Fix (TRowEmptyF :*: _)) newLabel = - throwError $ show $ - ppPos pos1 <+> ": label" <+> text newLabel <+> "cannot be inserted into row type introduced at" <+> ppPos pos2 + throwError . show $ + ppPos pos1 <+> ": label" + <+> text newLabel + <+> "cannot be inserted into row type introduced at" + <+> ppPos pos2 rewriteRow pos1 pos2 (Fix (TRowExtendF label fieldTy rowTail :*: K pos)) newLabel | newLabel == label = -- nothing to do return (fieldTy, rowTail, nullSubst) | TVar v <- rowTail, tyvarFlavour v == Skolem = - throwError $ show $ vcat $ + throwError . show $ vcat [ ppPos pos1 <+> ": Type not polymorphic enough:" , ppPos pos2 ] @@ -462,8 +462,9 @@ case apply s ty of TRecord r -> return $ rowToMap r _ -> - throwError $ show $ - ppPos pos <+> ": record wildcard cannot bind to type:" <+> ppType ty + throwError . show $ + ppPos pos <+> ": record wildcard cannot bind to type:" + <+> ppType ty subsCheck :: Pos -> Sigma -> Sigma -> TI ()