expresso 0.1.2.0 → 0.1.2.2
raw patch · 6 files changed
+92/−40 lines, 6 filesPVP ok
version bump matches the API change (PVP)
API changes (from Hackage documentation)
Files
- README.md +2/−1
- expresso.cabal +1/−1
- src/Expresso/Eval.hs +0/−1
- src/Expresso/Pretty.hs +2/−1
- src/Expresso/Type.hs +68/−18
- src/Expresso/TypeCheck.hs +19/−18
README.md view
@@ -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 `<term> : <type>` , will not suffice for "schema validation". For example, consider this attempt at validating an integer against a schema that permits everything:
expresso.cabal view
@@ -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
src/Expresso/Eval.hs view
@@ -50,7 +50,6 @@ where import Control.Monad.Except-import Data.Foldable (foldrM) import Data.HashMap.Strict (HashMap) import Data.IORef import Data.Ord
src/Expresso/Pretty.hs view
@@ -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
src/Expresso/Type.hs view
@@ -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
src/Expresso/TypeCheck.hs view
@@ -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 ()