diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,30 @@ +Copyright (c) 2018, Oleg Grenrus + +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are met: + + * Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + + * Redistributions in binary form must reproduce the above + copyright notice, this list of conditions and the following + disclaimer in the documentation and/or other materials provided + with the distribution. + + * Neither the name of Oleg Grenrus nor the names of other + contributors may be used to endorse or promote products derived + from this software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT +OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, +SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT +LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, +DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY +THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT +(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE +OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/bound-extras.cabal b/bound-extras.cabal new file mode 100644 --- /dev/null +++ b/bound-extras.cabal @@ -0,0 +1,95 @@ +cabal-version: 2.2 +name: bound-extras +version: 0 + +synopsis: ScopeH and ScopeT extras for bound +category: Language, Compilers, Interpreters +description: + Provides more complex @Scope@ variants; @ScopeT@ and @ScopeH@: + . + @ + Scope b f a ~ ScopeT b IdentityT f a ~ ScopeH b f f a + ScopeT b t f a ~ ScopeH b (t f) f a + @ + . + 'ScopeH' probably should be preferred over 'ScopeT'. + Latter is left here for completeness. + . + Simple implementations of @ScopeH@ and @ScopeT@ would be similar + (sans type arguments) to @Bound.Scope.Simple@. + . + Look into @examples/@ directory for /System F/ and /Bidirectional STLC/ + implemented with a help of 'ScopeH'. + +license: BSD-3-Clause +license-file: LICENSE +copyright: (c) 2018 Oleg Grenrus + +author: Oleg Grenrus, Edward Kmett +maintainer: Oleg Grenrus +homepage: https://github.com/phadej/bound-extras +bug-reports: https://github.com/phadej/bound-extras/issues + +tested-with: + GHC ==8.0.2 + || ==8.2.2 + || ==8.4.3 + || ==8.6.1 + +extra-source-files: + examples/*.txt + +source-repository head + type: git + location: https://github.com/phadej/bound-extras + +library + default-language: Haskell2010 + hs-source-dirs: src + ghc-options: -Wall + + exposed-modules: + Bound.ScopeH + Bound.ScopeT + Control.Monad.Module + + build-depends: + -- GHC boot libraries + , base ^>=4.9.1.0 || ^>= 4.10.1.0 || ^>=4.11.1.0 + , deepseq ^>=1.4.2.0 + , transformers ^>=0.5.0.0 + + -- other deps + , bound ^>=2.0.1 + , hashable ^>=1.2.7.0 + + if !impl(ghc >= 8.2) + build-depends: + bifunctors ^>=5.5.3 + + +test-suite examples + type: exitcode-stdio-1.0 + main-is: Examples.hs + other-modules: + Pretty + BiSTLC + SystemF + + default-language: Haskell2010 + hs-source-dirs: examples + ghc-options: -Wall + + build-depends: base, bound, bound-extras + , containers ^>=0.5.7.1 + , filepath ^>=1.4.1.1 + , pretty ^>=1.1.3.3 + , tasty ^>=1.1.0.3 + , text-short ^>=0.1.2 + , tasty-golden ^>=2.3.2 + , transformers ^>=0.5.0.0 + , utf8-string ^>=1.0.1.1 + + if !impl(ghc >= 8.2) + build-depends: + bifunctors ^>=5.5.3 diff --git a/examples/BiSTLC.hs b/examples/BiSTLC.hs new file mode 100644 --- /dev/null +++ b/examples/BiSTLC.hs @@ -0,0 +1,329 @@ +{-# LANGUAGE DeriveFoldable #-} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE DeriveTraversable #-} +{-# LANGUAGE FunctionalDependencies #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE OverloadedStrings #-} +module BiSTLC (tests) where + +import Bound.ScopeH +import Control.Monad (ap) +import Control.Monad.Module +import Data.String (IsString (..)) +import System.FilePath ((-<.>), ()) +import Test.Tasty (TestTree, testGroup) +import Test.Tasty.Golden (goldenVsString) + +import qualified Data.ByteString.Lazy.UTF8 as UTF8 + +import Pretty + +------------------------------------------------------------------------------- +-- Types +------------------------------------------------------------------------------- + +-- | Types. +data Ty + = TBool + | TNat + | Ty :-> Ty + deriving Eq + +infixr 2 :-> + +------------------------------------------------------------------------------- +-- Infession +------------------------------------------------------------------------------- + +-- | Inferable terms +data Inf a + = V a + + -- term abstraction + | App (Inf a) (Chk a) + + -- annotated term + | Ann (Chk a) Ty + + -- Booleans + | TT + | FF + + -- Numbers + | Zero + | Succ (Chk a) + deriving (Functor, Foldable, Traversable) + +(.:) :: Chk a -> Ty -> Inf a +(.:) = Ann +infix 1 .: + +-- | Checkable terms +data Chk a + = Inf (Inf a) + | Lam (ScopeH () Chk Inf a) + + -- : Bool -> a -> a -> a + | If (Chk a) (Chk a) (Chk a) + + -- : a -> (a -> a) -> Nat -> a + | FoldNat (Chk a) (Chk a) (Chk a) + deriving (Functor, Foldable, Traversable) + +------------------------------------------------------------------------------- +-- Instances +------------------------------------------------------------------------------- + +instance IsString a => IsString (Inf a) where fromString = V . fromString +instance IsString a => IsString (Chk a) where fromString = Inf . fromString + +instance Applicative Inf where + pure = V + (<*>) = ap + +instance Monad Inf where + return = V + + V x >>= k = k x + Ann x t >>= k = Ann (x >>== k) t + App f x >>= k = App (f >>= k) (x >>== k) + + TT >>= _ = TT + FF >>= _ = FF + + Zero >>= _ = Zero + Succ n >>= k = Succ (n >>== k) + +instance Module Chk Inf where + Inf x >>== k = Inf (x >>= k) + Lam b >>== k = Lam (b >>== k) + If c t e >>== k = If (c >>== k) (t >>== k) (e >>== k) + FoldNat z s n >>== k = FoldNat (z >>== k) (s >>== k) (n >>== k) + +lam_ :: Eq a => a -> Chk a -> Chk a +lam_ x b = Lam (abstract1H x b) + +------------------------------------------------------------------------------- +-- Normal form +------------------------------------------------------------------------------- + +ann :: Chk a -> Ty -> Inf a +ann (Inf x) _ = x +ann x t = Ann x t + +annNf :: Chk a -> Ty -> Inf a +annNf x t = ann (nfChk x t) t + +nf :: Inf a -> Inf a +nf (V x) = V x +nf (Ann x t) = annNf x t +nf (App f x) = case nf f of + Ann (Lam f') (a :-> b) -> annNf (instantiate1H (ann x a) f') b + f' -> App f' x -- not normalising, because type unclear + +nf TT = TT +nf FF = FF + +nf Zero = Zero +nf (Succ n) = Succ (nfChk n TNat) + +nfChk :: Chk a -> Ty -> Chk a +nfChk (Lam x) (_ :-> b) = Lam (toScopeH $ flip nfChk b $ fromScopeH x) +nfChk (Lam x) _ = Lam x -- not simplifying +nfChk (Inf x) _ = case nf x of + Ann x' _ -> x' + x' -> Inf x' +nfChk (If c t e) ty = case nfChk c TBool of + Inf TT -> nfChk t ty + Inf FF -> nfChk e ty + c' -> If c' t e -- doesn't normalise branches +nfChk (FoldNat z s n) ty = case iter n' of + Just x -> nfChk x ty + Nothing -> FoldNat z s n' + where + iter (Inf Zero) = Just z + iter (Inf (Succ n'')) = (s' $$) <$> iter n'' + iter _ = Nothing + + n' = nfChk n TNat + s' = s .: ty :-> ty + +------------------------------------------------------------------------------- +-- Pretty +------------------------------------------------------------------------------- + +instance Pretty Ty where + ppr = return . pprTy + +pprTy :: Ty -> Doc +pprTy TNat = text "Nat" +pprTy TBool = text "Bool" +pprTy (a :-> b) = sexpr (text "->") $ map pprTy $ a : peelArr b + +instance Pretty a => Pretty (Inf a) where ppr x = traverse ppr x >>= pprInf +instance Pretty a => Pretty (Chk a) where ppr x = traverse ppr x >>= pprChk + +pprInf :: Inf Doc -> PrettyM Doc +pprInf (V x) = pure x +pprInf (App f x) = case peelApp f of + (f', xs) -> sexpr + <$> pprInf f' + <*> traverse pprChk (xs ++ [x]) +pprInf (Ann x t) = do + x' <- pprChk x + t' <- ppr t + return $ sexpr (text "the") [t', x'] + +pprInf TT = return (text "#t") +pprInf FF = return (text "#f") + +pprInf Zero = return (integer 0) +pprInf (Succ n) = case peelNat n of + Just n' -> return (integer (succ n')) + Nothing -> sexpr (text "S") . pure <$> pprChk n + +pprChk :: Chk Doc -> PrettyM Doc +pprChk (Inf i) = pprInf i +pprChk (Lam b) = do + n <- text <$> fresh "x" + b' <- pprChk (instantiate1H (V n) b) + return $ sexpr (text "fn") [ n, b' ] +pprChk (If c t e) = sexpr (text "if") <$> traverse pprChk [c, t, e] +pprChk (FoldNat z f n) = sexpr (text "fold-Nat") <$> traverse pprChk [z, f, n] + +-- We output +-- (0 1 2 3) +-- instead of +-- (((0 1) 2) 3) +-- small, but nice improvement! +peelApp :: Inf a -> (Inf a, [Chk a]) +peelApp (App a b) = (++ [b]) <$> peelApp a +peelApp e = (e, []) + +peelArr :: Ty -> [Ty] +peelArr (a :-> b) = a : peelArr b +peelArr x = [x] + +peelNat :: Chk a -> Maybe Integer +peelNat (Inf Zero) = Just 0 +peelNat (Inf (Succ n)) = succ <$> peelNat n +peelNat _ = Nothing + +------------------------------------------------------------------------------- +-- peelApp +------------------------------------------------------------------------------- + +infixl 2 $$ + +class SApp f g h | h -> f g where + ($$) :: f a -> g a -> h a + +instance SApp Inf Chk Inf where ($$) = App +instance SApp Inf Chk Chk where f $$ x = Inf (f $$ x) + +class SBool f where + tt :: f a + ff :: f a + +instance SBool Inf where + tt = TT + ff = FF + +instance SBool Chk where + tt = Inf tt + ff = Inf ff + +------------------------------------------------------------------------------- +-- Type-checking +------------------------------------------------------------------------------- + +infer :: (a -> Ty) -> Inf a -> Maybe Ty +infer f = infer' . fmap f + +-- No error reporting :) +infer' :: Inf Ty -> Maybe Ty +infer' (V a) = Just a +infer' (App f x) = do + f' <- infer' f + case f' of + a :-> b -> do + check' x a + Just b + _ -> Nothing +infer' (Ann x t) = do + check' x t + Just t + +infer' TT = Just TBool +infer' FF = Just TBool + +infer' Zero = Just TNat +infer' (Succ n) = do + check' n TNat + Just TNat + +check' :: Chk Ty -> Ty -> Maybe () +check' (Lam x) t = case t of + a :-> b -> check' (instantiate1H (V a) x) b + _ -> Nothing +check' (Inf x) t = do + t' <- infer' x + if t == t' + then Just () + else Nothing +check' (If c t e) ty = do + check' c TBool + check' t ty + check' e ty +check' (FoldNat z f n) ty = do + check' z ty + check' f (ty :-> ty) + check' n TNat + +------------------------------------------------------------------------------- +-- Examples +------------------------------------------------------------------------------- + +id_ :: Inf ShortText +id_ = lam_ "x" "x" .: TNat :-> TNat + +not_ :: Inf ShortText +not_ = lam_ "x" (If "x" ff tt) .: TBool :-> TBool + +two_ :: Inf ShortText +two_ = Succ (Inf (Succ (Inf Zero))) + +plus_ :: Inf ShortText +plus_ = term .: TNat :-> TNat :-> TNat where + term = lam_ "n" $ lam_ "m" $ FoldNat "m" s "n" + s = lam_ "k" $ Inf (Succ "k") + +mult_ :: Inf ShortText +mult_ = term .: TNat :-> TNat :-> TNat where + term = lam_ "n" $ lam_ "m" $ FoldNat (Inf Zero) (plus_ $$ "m") "n" + +demo :: String -> Inf ShortText -> [String] +demo name e = case infer (const TBool) e of + Nothing -> + [ name ++ " = " ++ pretty e + , "DOESN'T TYPECHECK" + ] + Just t -> + [ name ++ " : " ++ pretty t + , name ++ " = " ++ pretty e + , name ++ " = " ++ pretty (nf e) + ] + +tests :: TestTree +tests = testGroup "Bi-directional STLC" + [ demo' "id" id_ + , demo' "not-tt" $ not_ $$ tt + , demo' "four-plus" $ plus_ $$ Inf two_ $$ Inf two_ + , demo' "four-mult" $ mult_ $$ Inf two_ $$ Inf two_ + ] + where + demo' name e = goldenVsString name ("examples" name' -<.> "txt") + $ return $ UTF8.fromString $ unlines + $ demo name e + where + name' = "stlc-" ++ name diff --git a/examples/Examples.hs b/examples/Examples.hs new file mode 100644 --- /dev/null +++ b/examples/Examples.hs @@ -0,0 +1,12 @@ +module Main (main) where + +import qualified BiSTLC +import qualified SystemF + +import Test.Tasty (testGroup, defaultMain) + +main :: IO () +main = defaultMain $ testGroup "Examples" + [ BiSTLC.tests + , SystemF.tests + ] diff --git a/examples/Pretty.hs b/examples/Pretty.hs new file mode 100644 --- /dev/null +++ b/examples/Pretty.hs @@ -0,0 +1,63 @@ +module Pretty ( + Pretty (..), + pretty, + PrettyM, + ShortText, + Doc, + sexpr, + fresh, + PP.text, + PP.integer, + ) where + +import Control.Monad.Trans.State.Strict +import Data.Text.Short (ShortText) +import Data.Char (isDigit) + +import qualified Data.Text.Short as TS +import qualified Text.PrettyPrint as PP + +import qualified Data.Set as Set + +type S = Set.Set ShortText +type Doc = PP.Doc +type PrettyM = State S + +pretty :: Pretty a => a -> String +pretty x = PP.render (evalState (ppr x) Set.empty) + +markUsed :: ShortText -> State S () +markUsed t = modify' (Set.insert t) + +sexpr :: Doc -> [Doc] -> Doc +sexpr car cdr = PP.parens $ PP.hang car 2 $ PP.sep cdr + +fresh :: String -> PrettyM String +fresh s = state (pick names) + where + pick [] u = (s, u) -- shouldn't happen, names is infinite + pick (x : xs) u + | x' `Set.member` u = pick xs u + | otherwise = (x, Set.insert x' u) + where + x' = TS.pack x + + names = n : [ n ++ show m | m <- [d .. ] ] + + (ds, rn) = span isDigit (reverse s) + + n :: String + n = reverse rn + + d :: Int + d = case ds of + [] -> 0 + _ -> read (reverse ds) + +class Pretty a where + ppr :: a -> PrettyM Doc + +instance Pretty ShortText where + ppr t = do + markUsed t + return $ PP.text $ TS.unpack t diff --git a/examples/SystemF.hs b/examples/SystemF.hs new file mode 100644 --- /dev/null +++ b/examples/SystemF.hs @@ -0,0 +1,335 @@ +{-# LANGUAGE DeriveFoldable #-} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE DeriveTraversable #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE OverloadedStrings #-} +module SystemF (tests) where + +import Bound.Class ((>>>=)) +import Bound.Scope +import Bound.ScopeH +import Bound.Var (Var (..)) +import Control.Monad (ap) +import Control.Monad.Module +import Data.Bifoldable (Bifoldable (..)) +import Data.Bifunctor (Bifunctor (..)) +import Data.Bitraversable (Bitraversable (..), bifoldMapDefault, bimapDefault) +import Data.Functor.Classes (Eq1 (..), eq1) +import Data.String (IsString (..)) +import System.FilePath ((-<.>), ()) +import Test.Tasty (TestTree, testGroup) +import Test.Tasty.Golden (goldenVsString) + +import qualified Data.ByteString.Lazy.UTF8 as UTF8 + +import Pretty + +------------------------------------------------------------------------------- +-- Types +------------------------------------------------------------------------------- + +-- | Types. +-- +-- Noteworthy thing is the absence of any /application/. +-- 'TForall' abstract only over types, not type-constructors; +-- so we don't have type application either. +-- In short: everything is well-kinded by construction. +data Ty a + = TV a + | Ty a :-> Ty a + | TForall (Scope () Ty a) + deriving (Functor, Foldable, Traversable) + +infixr 1 :-> + +instance Applicative Ty where + pure = TV + (<*>) = ap + +instance Monad Ty where + return = TV + TV x >>= k = k x + (a :-> b) >>= k = (a >>= k) :-> (b >>= k) + TForall t >>= k = TForall (t >>>= k) + +instance Eq1 Ty where + liftEq eq (TV a) (TV a') = eq a a' + liftEq eq (a :-> b) (a' :-> b') = liftEq eq a a' && liftEq eq b b' + liftEq eq (TForall a) (TForall a') = liftEq eq a a' + + liftEq _ TV {} _ = False + liftEq _ (:->) {} _ = False + liftEq _ TForall {} _ = False + +instance Eq a => Eq (Ty a) where (==) = eq1 + +instance IsString a => IsString (Ty a) where + fromString = TV . fromString + +forall_ :: Eq a => a -> Ty a -> Ty a +forall_ n t = TForall (abstract1 n t) + +------------------------------------------------------------------------------- +-- Expression +------------------------------------------------------------------------------- + +data Expr b a + = V a + + -- term abstraction + | Lam (Ty b) (Scope () (Expr b) a) + | App (Expr b a) (Expr b a) + + -- type abstraction + | TyApp (Expr b a) (Ty b) + | Forall (ScopeH () (Expr' a) Ty b) + +instance IsString a => IsString (Expr b a) where + fromString = V . fromString + +{- +-- | In practice we should write Bitraversable instance, and use +-- 'bimapDefault' as Bifunctor implementation. +-- +-- That's an argument (not a good one) to omit 'bimapScope' from @bound@. +instance Bifunctor Expr where + bimap f g = go where + go (V x) = V (g x) + go (App a b) = App (go a) (go b) + go (TyApp a b) = TyApp (go a) (fmap f b) + go (Lam t b) = Lam (fmap f t) (bimapScope f g b) + go (Forall (ScopeH b)) = Forall $ ScopeH $ + bimap g (fmap (fmap f)) b +-} + +instance Bifunctor Expr where bimap = bimapDefault +instance Bifunctor Expr' where bimap = bimapDefault +instance Bifoldable Expr where bifoldMap = bifoldMapDefault +instance Bifoldable Expr' where bifoldMap = bifoldMapDefault + +instance Bitraversable Expr' where + bitraverse f g = fmap Expr' . bitraverse g f . unExpr' + +instance Bitraversable Expr where + bitraverse f g = go where + go (V x) = V <$> g x + go (App a b) = App <$> go a <*> go b + go (TyApp a b) = TyApp <$> go a <*> traverse f b + go (Lam t b) = Lam <$> traverse f t <*> bitraverseScope f g b + go (Forall s) = Forall <$> bitransverseScopeH (bitraverse g) traverse f s + +instance Functor (Expr b) where + fmap = second + +instance Applicative (Expr b) where + pure = V + (<*>) = ap + +instance Monad (Expr b) where + return = V + + V x >>= k = k x + App a b >>= k = App (a >>= k) (b >>= k) + Lam t b >>= k = Lam t (b >>>= k) + TyApp a b >>= k = TyApp (a >>= k) b + Forall b >>= k = Forall $ ScopeH $ overExpr' (>>= k') $ unscopeH b where + k' = first (F . TV) . k + +-- | @'Flip' 'Expr'@. +newtype Expr' a b = Expr' { unExpr' :: Expr b a } + +overExpr :: (Expr' a b -> Expr' a b') -> Expr b a -> Expr b' a +overExpr f = unExpr' . f . Expr' + +overExpr' :: (Expr b a -> Expr b' a') -> Expr' a b -> Expr' a' b' +overExpr' f = Expr' . f . unExpr' + +instance Functor (Expr' a) where + fmap f = overExpr' (first f) + +instance Module (Expr' c) Ty where + Expr' (V a) >>== _ = Expr' (V a) + + Expr' (Lam t s) >>== k = Expr' $ Lam (t >>= k) $ hoistScope (overExpr (>>== k)) s + Expr' (Forall s) >>== k = Expr' $ Forall $ s >>== k + + Expr' (App a b) >>== k = Expr' $ App + (unExpr' (Expr' a >>== k)) + (unExpr' (Expr' b >>== k)) + + Expr' (TyApp a b) >>== k = Expr' $ TyApp + (unExpr' (Expr' a >>== k)) + (b >>= k) + +tyLam_ :: Eq b => b -> Expr b a -> Expr b a +tyLam_ n e = Forall $ abstract1H n (Expr' e) + +lam_ :: Eq a => a -> Ty b -> Expr b a -> Expr b a +lam_ x t b = Lam t (abstract1 x b) + +------------------------------------------------------------------------------- +-- Normal form +------------------------------------------------------------------------------- + +tnf :: Ty b -> Ty b +tnf (TV x) = TV x +tnf (a :-> b) = tnf a :-> tnf b +tnf (TForall a) = TForall (toScope $ tnf $ fromScope a) + +nf :: Expr b a -> Expr b a +nf (V x) = V x +nf (Lam t b) = Lam (tnf t) (toScope $ nf $ fromScope b) +nf (App a b) = case nf a of + Lam _ a' -> nf $ instantiate1 b a' + a' -> App a' (nf b) +nf (Forall e) = Forall $ toScopeH $ overExpr' nf $ fromScopeH e +nf (TyApp a b) = case nf a of + Forall a' -> nf $ unExpr' $ instantiate1H b a' + a' -> TyApp a' (tnf b) + +------------------------------------------------------------------------------- +-- Pretty +------------------------------------------------------------------------------- + +instance Pretty a => Pretty (Ty a) where + ppr x = traverse ppr x >>= pprTy + +pprTy :: Ty Doc -> PrettyM Doc +pprTy (TV x) = return x +pprTy (a :-> b) = sexpr (text "->") <$> traverse pprTy [a, b] +pprTy (TForall s) = do + a <- text <$> fresh "a" + pprTy (instantiate1 (TV a) s) + +instance (Pretty a, Pretty b) => Pretty (Expr b a) where + ppr x = bitraverse ppr ppr x >>= pprExpr + +pprExpr :: Expr Doc Doc -> PrettyM Doc +pprExpr (V x) = return x +pprExpr (App a b) = pprApplications $ applications a ++ [Right b] +pprExpr (TyApp a b) = pprApplications $ applications a ++ [Left b] +pprExpr (Lam t b) = do + x <- text <$> fresh "x" + t' <- pprTy t + b' <- pprExpr $ instantiate1 (V x) b + return $ sexpr (text "fn") [ sexpr "the" [t', x], b'] +pprExpr (Forall b) = do + t <- text <$> fresh "b" + b' <- pprExpr $ unExpr' $ instantiate1H (TV t) b + return $ sexpr (text "poly") [ t , b'] + +pprApplications :: [Either (Ty Doc) (Expr Doc Doc)] -> PrettyM Doc +pprApplications [] = return $ text "()" +pprApplications (x : xs) = sexpr <$> pp x <*> traverse pp xs + where + pp = either pprTy pprExpr + +-- We output +-- (0 1 2 3) +-- instead of +-- (((0 1) 2) 3) +-- small, but nice improvement! +applications :: Expr a b -> [Either (Ty a) (Expr a b)] +applications (App a b) = applications a ++ [Right b] +applications (TyApp a b) = applications a ++ [Left b] +applications e = [Right e] + +------------------------------------------------------------------------------- +-- Applications +------------------------------------------------------------------------------- + +infixl 2 $$, @@ + +($$) :: Expr b a -> Expr b a -> Expr b a +($$) = App + +(@@) :: Expr b a -> Ty b -> Expr b a +(@@) = TyApp + +------------------------------------------------------------------------------- +-- Type-checking +------------------------------------------------------------------------------- + +-- | Type-check assuming that free variables have the similarly named type. +-- In systemf type and term namespaces are different! +check :: Eq a => Expr a a -> Maybe (Ty a) +check = check' . fmap TV + +-- No error reporting :) +check' :: Eq a => Expr a (Ty a) -> Maybe (Ty a) +check' (V a) = Just a +check' (App f x) = do + f' <- check' f + x' <- check' x + case f' of + a' :-> b' | a' == x' -> return b' + _ -> Nothing +check' (TyApp x t) = do + x' <- check' x + case x' of + TForall b -> return (instantiate1 t b) + _ -> Nothing +check' (Lam t b) = do + b' <- check' (instantiate1 (V t) b) + return (t :-> b') + +check' (Forall b) = do + let b' = unExpr' $ fromScopeH b + b'' <- check' (fmap (fmap F) b') + return $ TForall $ toScope b'' + +------------------------------------------------------------------------------- +-- Identity function +------------------------------------------------------------------------------- + +-- idType_ :: Ty ShortText +-- idType_ = forall_ "n" $ "n" :-> "n" + +id_ :: Expr ShortText ShortText +id_ = tyLam_ "a" $ lam_ "x" "a" "x" + +------------------------------------------------------------------------------- +-- Church numerals +------------------------------------------------------------------------------- + +natType :: Ty ShortText +natType = forall_ "a" $ ("a" :-> "a") :-> "a" :-> "a" + +zero :: Expr ShortText ShortText +zero = tyLam_ "a" $ lam_ "f" ("a" :-> "a") $ lam_ "z" "a" "z" + +-- sucType :: Ty ShortText +-- sucType = natType :-> natType + +suc :: Expr ShortText ShortText +suc + = lam_ "n" natType + $ tyLam_ "a" $ lam_ "f" ("a" :-> "a") $ lam_ "z" "a" + $ "n" @@ "a" $$ "f" $$ ("f" $$ "z") + +demo :: String -> Expr ShortText ShortText -> [String] +demo name e = case check e of + Nothing -> + [ name ++ " = " ++ pretty e + , "DOESN'T TYPECHECK" + ] + Just t -> + [ name ++ " : " ++ pretty t + , name ++ " = " ++ pretty e + , name ++ " = " ++ pretty (nf e) + ] + +tests :: TestTree +tests = testGroup "System F" + [ demo' "id" id_ + , demo' "0" zero + , demo' "suc" suc + , demo' "1" (suc $$ zero) + , demo' "2" (suc $$ (suc $$ zero)) + ] + where + demo' name e = goldenVsString name ("examples" name' -<.> "txt") + $ return $ UTF8.fromString $ unlines + $ demo name e + where + name' = "sysf-" ++ name diff --git a/examples/stlc-four-mult.txt b/examples/stlc-four-mult.txt new file mode 100644 --- /dev/null +++ b/examples/stlc-four-mult.txt @@ -0,0 +1,15 @@ +four-mult : Nat +four-mult = ((the + (-> Nat Nat Nat) + (fn + x + (fn + x0 + (fold-Nat + 0 + ((the + (-> Nat Nat Nat) (fn x1 (fn x2 (fold-Nat x2 (fn x3 (S x3)) x1)))) + x0) + x)))) + 2 2) +four-mult = 4 diff --git a/examples/stlc-four-plus.txt b/examples/stlc-four-plus.txt new file mode 100644 --- /dev/null +++ b/examples/stlc-four-plus.txt @@ -0,0 +1,5 @@ +four-plus : Nat +four-plus = ((the + (-> Nat Nat Nat) (fn x (fn x0 (fold-Nat x0 (fn x1 (S x1)) x)))) + 2 2) +four-plus = 4 diff --git a/examples/stlc-id.txt b/examples/stlc-id.txt new file mode 100644 --- /dev/null +++ b/examples/stlc-id.txt @@ -0,0 +1,3 @@ +id : (-> Nat Nat) +id = (the (-> Nat Nat) (fn x x)) +id = (the (-> Nat Nat) (fn x x)) diff --git a/examples/stlc-not-tt.txt b/examples/stlc-not-tt.txt new file mode 100644 --- /dev/null +++ b/examples/stlc-not-tt.txt @@ -0,0 +1,3 @@ +not-tt : Bool +not-tt = ((the (-> Bool Bool) (fn x (if x #f #t))) #t) +not-tt = #f diff --git a/examples/sysf-0.txt b/examples/sysf-0.txt new file mode 100644 --- /dev/null +++ b/examples/sysf-0.txt @@ -0,0 +1,3 @@ +0 : (-> (-> a a) (-> a a)) +0 = (poly b (fn (the (-> b b) x) (fn (the b x0) x0))) +0 = (poly b (fn (the (-> b b) x) (fn (the b x0) x0))) diff --git a/examples/sysf-1.txt b/examples/sysf-1.txt new file mode 100644 --- /dev/null +++ b/examples/sysf-1.txt @@ -0,0 +1,6 @@ +1 : (-> (-> a a) (-> a a)) +1 = ((fn + (the (-> (-> a a) (-> a a)) x) + (poly b (fn (the (-> b b) x0) (fn (the b x1) (x b x0 (x0 x1)))))) + (poly b0 (fn (the (-> b0 b0) x2) (fn (the b0 x3) x3)))) +1 = (poly b (fn (the (-> b b) x) (fn (the b x0) (x x0)))) diff --git a/examples/sysf-2.txt b/examples/sysf-2.txt new file mode 100644 --- /dev/null +++ b/examples/sysf-2.txt @@ -0,0 +1,10 @@ +2 : (-> (-> a a) (-> a a)) +2 = ((fn + (the (-> (-> a a) (-> a a)) x) + (poly b (fn (the (-> b b) x0) (fn (the b x1) (x b x0 (x0 x1)))))) + ((fn + (the (-> (-> a0 a0) (-> a0 a0)) x2) + (poly + b0 (fn (the (-> b0 b0) x3) (fn (the b0 x4) (x2 b0 x3 (x3 x4)))))) + (poly b1 (fn (the (-> b1 b1) x5) (fn (the b1 x6) x6))))) +2 = (poly b (fn (the (-> b b) x) (fn (the b x0) (x (x x0))))) diff --git a/examples/sysf-id.txt b/examples/sysf-id.txt new file mode 100644 --- /dev/null +++ b/examples/sysf-id.txt @@ -0,0 +1,3 @@ +id : (-> a a) +id = (poly b (fn (the b x) x)) +id = (poly b (fn (the b x) x)) diff --git a/examples/sysf-suc.txt b/examples/sysf-suc.txt new file mode 100644 --- /dev/null +++ b/examples/sysf-suc.txt @@ -0,0 +1,7 @@ +suc : (-> (-> (-> a a) (-> a a)) (-> (-> a0 a0) (-> a0 a0))) +suc = (fn + (the (-> (-> a a) (-> a a)) x) + (poly b (fn (the (-> b b) x0) (fn (the b x1) (x b x0 (x0 x1)))))) +suc = (fn + (the (-> (-> a a) (-> a a)) x) + (poly b (fn (the (-> b b) x0) (fn (the b x1) (x b x0 (x0 x1)))))) diff --git a/src/Bound/ScopeH.hs b/src/Bound/ScopeH.hs new file mode 100644 --- /dev/null +++ b/src/Bound/ScopeH.hs @@ -0,0 +1,330 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE UndecidableInstances #-} +-- | 'ScopeH' scope, which allows substitute 'f' into 'g' to get new 'g'. +-- +-- Compare following signatures: +-- +-- @ +-- 'instantiate1' :: ... => m a -> 'Scope' b m a -> m a +-- 'instantiate1H' :: ... => m a -> 'ScopeH' b f m a -> f a +-- @ +-- +-- 'ScopeH' variant allows to encode e.g. Hindley-Milner types, where +-- we diffentiate between @Poly@ and @Mono@-morphic types. +-- +-- @ +-- specialise :: Poly a -> Mono a -> Poly a +-- specialise (Forall p) m = 'instantiate1H' m p +-- specialise _ _ = error "ill-kinded" +-- @ +-- +-- Another applications are /bidirectional/ type-systems or representing +-- normal forms with /normal/ and /neutral/ terms, +-- aka /introduction/ and /elimination/ terms. +-- +-- Look into @examples/@ directory for /System F/ and /Bidirectional STLC/ +-- implemented with a help of 'ScopeH'. +-- +module Bound.ScopeH ( + ScopeH (..), + -- * Abstraction + abstractH, abstract1H, abstractHEither, + -- ** Name + abstractHName, abstract1HName, + -- * Instantiation + instantiateH, instantiate1H, instantiateHEither, + -- * Traditional de Bruijn + fromScopeH, + toScopeH, + -- * Bound variable manipulation + lowerScopeH, + convertFromScope, + splatH, + bindingsH, + mapBoundH, + mapScopeH, + foldMapBoundH, + foldMapScopeH, + traverseBoundH_, + traverseScopeH_, + traverseBoundH, + traverseScopeH, + bitraverseScopeH, + bitransverseScopeH, + ) where + +import Bound (Scope (..), Var (..)) +import Bound.Name (Name (..)) +import Control.DeepSeq (NFData (..)) +import Control.Monad.Module (Module (..)) +import Data.Bifoldable (bifoldMap, bitraverse_) +import Data.Bifunctor (bimap) +import Data.Bitraversable (Bitraversable (..)) +import Data.Foldable (traverse_) +import Data.Functor.Classes +import Data.Hashable (Hashable (..)) +import Data.Hashable.Lifted (Hashable1 (..), hashWithSalt1) + +-- | @'ScopeH' b f m a@ is a @f@ expression abstracted over @g@, +-- with bound variables in @b@, and free variables in @a@. +-- +-- @ +-- 'Scope' b f a ~ 'ScopeH' n f f a +-- 'ScopeT' b t f a ~ 'ScopeH' b (t f) f a +-- @ +-- +newtype ScopeH b f m a = ScopeH { unscopeH :: f (Var b (m a)) } + +instance (Functor f, Monad m) => Module (ScopeH b f m) m where + ScopeH s >>== k = ScopeH $ fmap (fmap (>>= k)) s + +------------------------------------------------------------------------------- +-- Instances +------------------------------------------------------------------------------- + +instance (Functor f, Functor m) => Functor (ScopeH b f m) where + fmap f (ScopeH a) = ScopeH $ fmap (fmap (fmap f)) a + +instance (Foldable f, Foldable m) => Foldable (ScopeH b f m) where + foldMap f (ScopeH a) = foldMap (foldMap (foldMap f)) a + foldr f z (ScopeH a) = foldr (flip (foldr (flip (foldr f)))) z a + +instance (Traversable f, Traversable m) => Traversable (ScopeH b f m) where + traverse f (ScopeH a) = ScopeH <$> traverse (traverse (traverse f)) a + +instance (Hashable b, Module f m, Hashable1 f, Hashable1 m) => Hashable1 (ScopeH b f m) where + liftHashWithSalt h s m = liftHashWithSalt (liftHashWithSalt h) s (fromScopeH m) + {-# INLINE liftHashWithSalt #-} + +instance (Hashable b, Module f m, Hashable1 f, Hashable1 m, Hashable a) => Hashable (ScopeH b f m a) where + hashWithSalt n m = hashWithSalt1 n (fromScopeH m) + {-# INLINE hashWithSalt #-} + +instance NFData (f (Var b (m a))) => NFData (ScopeH b f m a) where + rnf scope = rnf (unscopeH scope) + +instance (Module f m, Eq b, Eq1 f, Eq1 m, Eq a) => Eq (ScopeH b f m a) where (==) = eq1 +instance (Module f m, Ord b, Ord1 f, Ord1 m, Ord a) => Ord (ScopeH b f m a) where compare = compare1 +instance (Show b, Show1 f, Show1 m, Show a) => Show (ScopeH b f m a) where showsPrec = showsPrec1 +instance (Read b, Read1 f, Read1 m, Read a) => Read (ScopeH b f m a) where readsPrec = readsPrec1 + +------------------------------------------------------------------------------- +-- * transformers 0.5 Data.Functor.Classes +------------------------------------------------------------------------------- + +instance (Module f m, Eq b, Eq1 f, Eq1 m) => Eq1 (ScopeH b f m) where + liftEq f m n = liftEq (liftEq f) (fromScopeH m) (fromScopeH n) + +instance (Module f m, Ord b, Ord1 f, Ord1 m) => Ord1 (ScopeH b f m) where + liftCompare f m n = liftCompare (liftCompare f) (fromScopeH m) (fromScopeH n) + +instance (Show b, Show1 f, Show1 m) => Show1 (ScopeH b f m) where + liftShowsPrec sp sl d (ScopeH x) = showsUnaryWith + (liftShowsPrec (liftShowsPrec sp' sl') (liftShowList sp' sl')) + "ScopeH" d x + where + sp' = liftShowsPrec sp sl + sl' = liftShowList sp sl + +instance (Read b, Read1 f, Read1 m) => Read1 (ScopeH b f m) where + liftReadsPrec f g = readsData $ readsUnaryWith + (liftReadsPrec (liftReadsPrec f' g') (liftReadList f' g')) + "ScopeH" ScopeH + where + f' = liftReadsPrec f g + g' = liftReadList f g + +------------------------------------------------------------------------------- +-- Abstraction +------------------------------------------------------------------------------- + +-- | Capture some free variables in an expression to yield a 'ScopeH' with bound variables in @b@. +abstractH :: (Functor f, Monad m) => (a -> Maybe b) -> f a -> ScopeH b f m a +abstractH f e = ScopeH (fmap k e) where + k y = case f y of + Just z -> B z + Nothing -> F (return y) +{-# INLINE abstractH #-} + +-- | Abstract over a single variable. +abstract1H :: (Functor f, Monad m, Eq a) => a -> f a -> ScopeH () f m a +abstract1H a = abstractH (\b -> if a == b then Just () else Nothing) +{-# INLINE abstract1H #-} + +-- | Capture some free variables in an expression to yield a 'ScopeH' with bound variables in @b@. Optionally change the types of the remaining free variables. +abstractHEither :: (Functor f, Monad m) => (a -> Either b c) -> f a -> ScopeH b f m c +abstractHEither f e = ScopeH (fmap k e) where + k y = case f y of + Left z -> B z + Right y' -> F (return y') +{-# INLINE abstractHEither #-} + +------------------------------------------------------------------------------- +-- Abstraction with Name +------------------------------------------------------------------------------- + +-- | Abstraction, capturing named bound variables. +abstractHName :: (Functor f, Monad m) => (a -> Maybe b) -> f a -> ScopeH (Name a b) f m a +abstractHName f t = ScopeH (fmap k t) where + k a = case f a of + Just b -> B (Name a b) + Nothing -> F (return a) +{-# INLINE abstractHName #-} + +-- | Abstract over a single variable +abstract1HName :: (Functor f, Monad m, Eq a) => a -> f a -> ScopeH (Name a ()) f m a +abstract1HName a = abstractHName (\b -> if a == b then Just () else Nothing) +{-# INLINE abstract1HName #-} + +------------------------------------------------------------------------------- +-- Instantiation +------------------------------------------------------------------------------- + +-- | Enter a 'ScopeH', instantiating all bound variables +instantiateH :: Module f m => (b -> m a) -> ScopeH b f m a -> f a +instantiateH k (ScopeH e) = e >>== \v -> case v of + B b -> k b + F a -> a +{-# INLINE instantiateH #-} + +-- | Enter a 'ScopeH' that binds one variable, instantiating it +instantiate1H :: Module f m => m a -> ScopeH b f m a -> f a +instantiate1H e = instantiateH (const e) +{-# INLINE instantiate1H #-} + +-- | Enter a 'ScopeH', and instantiate all bound and free variables in one go. +instantiateHEither :: Module f m => (Either b a -> m c) -> ScopeH b f m a -> f c +instantiateHEither f (ScopeH e) = e >>== \v -> case v of + B b -> f (Left b) + F ea -> ea >>= f . Right +{-# INLINE instantiateHEither #-} + +------------------------------------------------------------------------------- +-- Traditional de Bruijn +------------------------------------------------------------------------------- + +-- | Convert to traditional de Bruijn. +fromScopeH :: Module f m => ScopeH b f m a -> f (Var b a) +fromScopeH (ScopeH s) = s >>== \v -> case v of + F e -> fmap F e + B b -> return (B b) + +-- | Convert from traditional de Bruijn to generalized de Bruijn indices. +toScopeH :: (Functor f, Monad m) => f (Var b a) -> ScopeH b f m a +toScopeH e = ScopeH (fmap (fmap return) e) + +-- | Convert to 'Scope'. +lowerScopeH + :: (Functor f, Functor f) + => (forall x. f x -> h x) + -> (forall x. m x -> h x) + -> ScopeH b f m a -> Scope b h a +lowerScopeH f m (ScopeH x) = Scope (f (fmap (fmap m) x)) + +convertFromScope :: Scope b f a -> ScopeH b f f a +convertFromScope (Scope x) = ScopeH x + +------------------------------------------------------------------------------- +-- Extras +------------------------------------------------------------------------------- + +-- | Perform substitution on both bound and free variables in a 'ScopeH'. +splatH :: Module f m => (a -> m c) -> (b -> m c) -> ScopeH b f m a -> f c +splatH f unbind (ScopeH e) = e >>== \v -> case v of + B b -> unbind b + F ea -> ea >>= f +{-# INLINE splatH #-} + +-- | Return a list of occurences of the variables bound by this 'ScopeH'. +bindingsH :: Foldable f => ScopeH b f m a -> [b] +bindingsH (ScopeH s) = foldr f [] s where + f (B v) vs = v : vs + f _ vs = vs +{-# INLINE bindingsH #-} + +-- | Perform a change of variables on bound variables. +mapBoundH :: Functor f => (b -> b') -> ScopeH b f m a -> ScopeH b' f m a +mapBoundH f (ScopeH s) = ScopeH (fmap f' s) where + f' (B b) = B (f b) + f' (F a) = F a +{-# INLINE mapBoundH #-} + +-- | Perform a change of variables, reassigning both bound and free variables. +mapScopeH + :: (Functor f, Functor m) + => (b -> d) -> (a -> c) + -> ScopeH b f m a -> ScopeH d f m c +mapScopeH f g (ScopeH s) = ScopeH $ fmap (bimap f (fmap g)) s +{-# INLINE mapScopeH #-} + +-- | Obtain a result by collecting information from bound variables +foldMapBoundH :: (Foldable f, Monoid r) => (b -> r) -> ScopeH b f m a -> r +foldMapBoundH f (ScopeH s) = foldMap f' s where + f' (B a) = f a + f' _ = mempty +{-# INLINE foldMapBoundH #-} + +-- | Obtain a result by collecting information from both bound and free +-- variables +foldMapScopeH + :: (Foldable f, Foldable m, Monoid r) + => (b -> r) -> (a -> r) + -> ScopeH b f m a -> r +foldMapScopeH f g (ScopeH s) = foldMap (bifoldMap f (foldMap g)) s +{-# INLINE foldMapScopeH #-} + +-- | 'traverse_' the bound variables in a 'Scope'. +traverseBoundH_ :: (Applicative g, Foldable f) => (b -> g d) -> ScopeH b f m a -> g () +traverseBoundH_ f (ScopeH s) = traverse_ f' s where + f' (B a) = () <$ f a + f' _ = pure () +{-# INLINE traverseBoundH_ #-} + +-- | 'traverse_' both the variables bound by this scope and any free variables. +traverseScopeH_ + :: (Applicative g, Foldable f, Foldable m) + => (b -> g d) -> (a -> g c) + -> ScopeH b f m a -> g () +traverseScopeH_ f g (ScopeH s) = traverse_ (bitraverse_ f (traverse_ g)) s +{-# INLINE traverseScopeH_ #-} + +-- | 'traverse' the bound variables in a 'Scope'. +traverseBoundH + :: (Applicative g, Traversable f) + => (b -> g c) -> ScopeH b f m a -> g (ScopeH c f m a) +traverseBoundH f (ScopeH s) = ScopeH <$> traverse f' s where + f' (B b) = B <$> f b + f' (F a) = pure (F a) +{-# INLINE traverseBoundH #-} + +-- | 'traverse' both bound and free variables +traverseScopeH + :: (Applicative g, Traversable f, Traversable m) + => (b -> g d) -> (a -> g c) + -> ScopeH b f m a -> g (ScopeH d f m c) +traverseScopeH f g (ScopeH s) = ScopeH <$> traverse (bitraverse f (traverse g)) s +{-# INLINE traverseScopeH #-} + +bitraverseScopeH + :: (Applicative g, Bitraversable f, Bitraversable m) + => (k -> g k') + -> (l -> g l') + -> (a -> g a') + -> ScopeH b (f k) (m l) a + -> g (ScopeH b (f k') (m l') a') +bitraverseScopeH k l = bitransverseScopeH (bitraverse k) (bitraverse l) +{-# INLINE bitraverseScopeH #-} + +bitransverseScopeH + :: Applicative g + => (forall x x'. (x -> g x') -> f x -> g (f' x')) -- ^ 'traverse'-like for @f@ + -> (forall x x'. (x -> g x') -> m x -> g (m' x')) -- ^ 'traverse'-like for @m@ + -> (a -> g a') + -> ScopeH b f m a + -> g (ScopeH b f' m' a') +bitransverseScopeH tauF tauM f = fmap ScopeH . tauF (traverse (tauM f)) . unscopeH +{-# INLINE bitransverseScopeH #-} diff --git a/src/Bound/ScopeT.hs b/src/Bound/ScopeT.hs new file mode 100644 --- /dev/null +++ b/src/Bound/ScopeT.hs @@ -0,0 +1,316 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE RankNTypes #-} +#if __GLASGOW_HASKELL__ >= 805 +{-# LANGUAGE QuantifiedConstraints #-} +#endif +-- For NFData instance +{-# LANGUAGE UndecidableInstances #-} +-- | 'ScopeT' scope, which allows substitute 'f' into 't f' to get new 't f'. +-- +-- Consider using 'Bound.ScopeH.ScopeH', it might be clearer. +module Bound.ScopeT ( + ScopeT (..), + (>>>>=), + -- * Abstraction + abstractT, abstract1T, abstractTEither, + -- ** Name + abstractTName, abstract1TName, + -- * Instantiation + instantiateT, instantiate1T, instantiateTEither, + -- * Traditional de Bruijn + fromScopeT, + toScopeT, + -- * Bound variable manipulation + lowerScopeT, + splatT, + bindingsT, + mapBoundT, + mapScopeT, + foldMapBoundT, + foldMapScopeT, + traverseBoundT_, + traverseScopeT_, + traverseBoundT, + traverseScopeT, + bitransverseScopeT, + ) where + +import Bound (Bound (..), Scope (..), Var (..)) +import Bound.Name (Name (..)) +import Control.DeepSeq (NFData (..)) +import Control.Monad.Module (Module (..)) +import Data.Bifoldable (bifoldMap, bitraverse_) +import Data.Bifunctor (bimap) +import Data.Bitraversable (Bitraversable (..)) +import Data.Foldable (traverse_) +import Data.Functor.Classes +import Data.Hashable (Hashable (..)) +import Data.Hashable.Lifted (Hashable1 (..), hashWithSalt1) + +-- | @'Scope' b f a@ is a @t f@ expression abstracted over @f@, +-- with bound variables in @b@, and free variables in @a@. +-- +-- @ +-- 'Scope' n f a ~ 'ScopeT' n 'IdentityT' f a +-- 'ScopeT' n t f a ~ t ('Scope' n f) a +-- @ +-- +newtype ScopeT b t f a = ScopeT { unscopeT :: t f (Var b (f a)) } + +------------------------------------------------------------------------------- +-- Instances +------------------------------------------------------------------------------- + +instance (Functor (t f), Functor f) => Functor (ScopeT b t f) where + fmap f (ScopeT a) = ScopeT $ fmap (fmap (fmap f)) a + +instance (Foldable (t f), Foldable f) => Foldable (ScopeT b t f) where + foldMap f (ScopeT a) = foldMap (foldMap (foldMap f)) a + foldr f z (ScopeT a) = foldr (flip (foldr (flip (foldr f)))) z a + +instance (Traversable (t f), Traversable f) => Traversable (ScopeT b t f) where + traverse f (ScopeT a) = ScopeT <$> traverse (traverse (traverse f)) a + +-- | We cannot write @'Bound' ('ScopeT' n t)@ pre-GHC-8.6 (without an auxiliary type class). +(>>>>=) :: (Monad f, Functor (t f)) => ScopeT b t f a -> (a -> f c) -> ScopeT b t f c +ScopeT m >>>>= k = ScopeT $ fmap (fmap (>>= k)) m +{-# INLINE (>>>>=) #-} + +#if __GLASGOW_HASKELL__ >= 805 +-- | @(>>>=) :: ... => 'ScopeT' n t f a -> (a -> f b) -> 'ScopeT' n t f b@ +instance (forall f. Functor f => Functor (t f)) => Bound (ScopeT n t) where + (>>>=) = (>>>>=) +#endif + +instance (Monad f, Functor (t f)) => Module (ScopeT b t f) f where + (>>==) = (>>>>=) + +instance (Hashable b, Bound t, Monad f, Hashable1 f, Hashable1 (t f)) => Hashable1 (ScopeT b t f) where + liftHashWithSalt h s m = liftHashWithSalt (liftHashWithSalt h) s (fromScopeT m) + {-# INLINE liftHashWithSalt #-} + +instance (Hashable b, Bound t, Monad f, Hashable1 f, Hashable1 (t f), Hashable a) => Hashable (ScopeT b t f a) where + hashWithSalt n m = hashWithSalt1 n (fromScopeT m) + {-# INLINE hashWithSalt #-} + +instance NFData (t f (Var b (f a))) => NFData (ScopeT b t f a) where + rnf scope = rnf (unscopeT scope) + +instance (Monad f, Bound t, Eq b, Eq1 (t f), Eq1 f, Eq a) => Eq (ScopeT b t f a) where (==) = eq1 +instance (Monad f, Bound t, Ord b, Ord1 (t f), Ord1 f, Ord a) => Ord (ScopeT b t f a) where compare = compare1 +instance (Show b, Show1 (t f), Show1 f, Show a) => Show (ScopeT b t f a) where showsPrec = showsPrec1 +instance (Read b, Read1 (t f), Read1 f, Read a) => Read (ScopeT b t f a) where readsPrec = readsPrec1 + +------------------------------------------------------------------------------- +-- * transformers 0.5 Data.Functor.Classes +------------------------------------------------------------------------------- + +instance (Monad f, Bound t, Eq b, Eq1 (t f), Eq1 f) => Eq1 (ScopeT b t f) where + liftEq f m n = liftEq (liftEq f) (fromScopeT m) (fromScopeT n) + +instance (Monad f, Bound t, Ord b, Ord1 (t f), Ord1 f) => Ord1 (ScopeT b t f) where + liftCompare f m n = liftCompare (liftCompare f) (fromScopeT m) (fromScopeT n) + +instance (Show b, Show1 (t f), Show1 f) => Show1 (ScopeT b t f) where + liftShowsPrec sp sl d (ScopeT x) = showsUnaryWith + (liftShowsPrec (liftShowsPrec sp' sl') (liftShowList sp' sl')) + "ScopeT" d x + where + sp' = liftShowsPrec sp sl + sl' = liftShowList sp sl + +instance (Read b, Read1 (t f), Read1 f) => Read1 (ScopeT b t f) where + liftReadsPrec f g = readsData $ readsUnaryWith + (liftReadsPrec (liftReadsPrec f' g') (liftReadList f' g')) + "ScopeT" ScopeT + where + f' = liftReadsPrec f g + g' = liftReadList f g + +------------------------------------------------------------------------------- +-- Abstraction +------------------------------------------------------------------------------- + +-- | Capture some free variables in an expression to yield a 'ScopeT' with bound variables in @b@. +abstractT :: (Functor (t f), Monad f) => (a -> Maybe b) -> t f a -> ScopeT b t f a +abstractT f e = ScopeT (fmap k e) where + k y = case f y of + Just z -> B z + Nothing -> F (return y) +{-# INLINE abstractT #-} + +-- | Abstract over a single variable. +-- +-- >>> abstract1T 'x' (MaybeT (Nothing : map Just "xyz")) +-- ScopeT (MaybeT [Nothing,Just (B ()),Just (F "y"),Just (F "z")]) +abstract1T :: (Functor (t f), Monad f, Eq a) => a -> t f a -> ScopeT () t f a +abstract1T a = abstractT (\b -> if a == b then Just () else Nothing) +{-# INLINE abstract1T #-} + +-- | Capture some free variables in an expression to yield a 'ScopeT' with bound variables in @b@. Optionally change the types of the remaining free variables. +abstractTEither :: (Functor (t f), Monad f) => (a -> Either b c) -> t f a -> ScopeT b t f c +abstractTEither f e = ScopeT (fmap k e) where + k y = case f y of + Left z -> B z + Right y' -> F (return y') +{-# INLINE abstractTEither #-} + +------------------------------------------------------------------------------- +-- Abstraction with Name +------------------------------------------------------------------------------- + +-- | Abstraction, capturing named bound variables. +abstractTName :: (Functor (t f), Monad f) => (a -> Maybe b) -> t f a -> ScopeT (Name a b) t f a +abstractTName f t = ScopeT (fmap k t) where + k a = case f a of + Just b -> B (Name a b) + Nothing -> F (return a) +{-# INLINE abstractTName #-} + +-- | Abstract over a single variable +abstract1TName :: (Functor (t f), Monad f, Eq a) => a -> t f a -> ScopeT (Name a ()) t f a +abstract1TName a = abstractTName (\b -> if a == b then Just () else Nothing) +{-# INLINE abstract1TName #-} + +------------------------------------------------------------------------------- +-- Instantiation +------------------------------------------------------------------------------- + +-- | Enter a 'ScopeT', instantiating all bound variables +instantiateT :: (Bound t, Monad f) => (b -> f a) -> ScopeT b t f a -> t f a +instantiateT k (ScopeT e) = e >>>= \v -> case v of + B b -> k b + F a -> a +{-# INLINE instantiateT #-} + +-- | Enter a 'ScopeT' that binds one variable, instantiating it +instantiate1T :: (Bound t, Monad f) => f a -> ScopeT b t f a -> t f a +instantiate1T e = instantiateT (const e) +{-# INLINE instantiate1T #-} + +-- | Enter a 'ScopeT', and instantiate all bound and free variables in one go. +instantiateTEither :: (Bound t, Monad f) => (Either b a -> f c) -> ScopeT b t f a -> t f c +instantiateTEither f (ScopeT e) = e >>>= \v -> case v of + B b -> f (Left b) + F ea -> ea >>= f . Right +{-# INLINE instantiateTEither #-} + +------------------------------------------------------------------------------- +-- Traditional de Bruijn +------------------------------------------------------------------------------- + +-- | Convert to traditional de Bruijn. +fromScopeT :: (Bound t, Monad f) => ScopeT b t f a -> t f (Var b a) +fromScopeT (ScopeT s) = s >>>= \v -> case v of + F e -> fmap F e + B b -> return (B b) + +-- | Convert from traditional de Bruijn to generalized de Bruijn indices. +toScopeT :: (Functor (t f), Monad f) => t f (Var b a) -> ScopeT b t f a +toScopeT e = ScopeT (fmap (fmap return) e) + +-- | Convert to 'Scope'. +lowerScopeT + :: (Functor (t f), Functor f) + => (forall x. t f x -> g x) + -> (forall x. f x -> g x) + -> ScopeT b t f a -> Scope b g a +lowerScopeT tf f (ScopeT x) = Scope (tf (fmap (fmap f) x)) + +------------------------------------------------------------------------------- +-- Extras +------------------------------------------------------------------------------- + +-- | Perform substitution on both bound and free variables in a 'ScopeT'. +splatT :: (Bound t, Monad f) => (a -> f c) -> (b -> f c) -> ScopeT b t f a -> t f c +splatT f unbind (ScopeT e) = e >>>= \v -> case v of + B b -> unbind b + F ea -> ea >>= f +{-# INLINE splatT #-} + +-- | Return a list of occurences of the variables bound by this 'ScopeT'. +bindingsT :: Foldable (t f) => ScopeT b t f a -> [b] +bindingsT (ScopeT s) = foldr f [] s where + f (B v) vs = v : vs + f _ vs = vs +{-# INLINE bindingsT #-} + +-- | Perform a change of variables on bound variables. +mapBoundT :: Functor (t f) => (b -> b') -> ScopeT b t f a -> ScopeT b' t f a +mapBoundT f (ScopeT s) = ScopeT (fmap f' s) where + f' (B b) = B (f b) + f' (F a) = F a +{-# INLINE mapBoundT #-} + +-- | Perform a change of variables, reassigning both bound and free variables. +mapScopeT + :: (Functor (t f), Functor f) + => (b -> d) -> (a -> c) + -> ScopeT b t f a -> ScopeT d t f c +mapScopeT f g (ScopeT s) = ScopeT $ fmap (bimap f (fmap g)) s +{-# INLINE mapScopeT #-} + +-- | Obtain a result by collecting information from bound variables +foldMapBoundT :: (Foldable (t f), Monoid r) => (b -> r) -> ScopeT b t f a -> r +foldMapBoundT f (ScopeT s) = foldMap f' s where + f' (B a) = f a + f' _ = mempty +{-# INLINE foldMapBoundT #-} + +-- | Obtain a result by collecting information from both bound and free +-- variables +foldMapScopeT + :: (Foldable f, Foldable (t f), Monoid r) + => (b -> r) -> (a -> r) + -> ScopeT b t f a -> r +foldMapScopeT f g (ScopeT s) = foldMap (bifoldMap f (foldMap g)) s +{-# INLINE foldMapScopeT #-} + +-- | 'traverse_' the bound variables in a 'Scope'. +traverseBoundT_ :: (Applicative g, Foldable (t f)) => (b -> g d) -> ScopeT b t f a -> g () +traverseBoundT_ f (ScopeT s) = traverse_ f' s where + f' (B a) = () <$ f a + f' _ = pure () +{-# INLINE traverseBoundT_ #-} + +-- | 'traverse_' both the variables bound by this scope and any free variables. +traverseScopeT_ + :: (Applicative g, Foldable f, Foldable (t f)) + => (b -> g d) -> (a -> g c) + -> ScopeT b t f a -> g () +traverseScopeT_ f g (ScopeT s) = traverse_ (bitraverse_ f (traverse_ g)) s +{-# INLINE traverseScopeT_ #-} + +-- | 'traverse' the bound variables in a 'Scope'. +traverseBoundT + :: (Applicative g, Traversable (t f)) + => (b -> g c) -> ScopeT b t f a -> g (ScopeT c t f a) +traverseBoundT f (ScopeT s) = ScopeT <$> traverse f' s where + f' (B b) = B <$> f b + f' (F a) = pure (F a) +{-# INLINE traverseBoundT #-} + +-- | 'traverse' both bound and free variables +traverseScopeT + :: (Applicative g, Traversable f, Traversable (t f)) + => (b -> g d) -> (a -> g c) + -> ScopeT b t f a -> g (ScopeT d t f c) +traverseScopeT f g (ScopeT s) = ScopeT <$> traverse (bitraverse f (traverse g)) s +{-# INLINE traverseScopeT #-} + +-- | If you are looking for 'bitraverseScopeT', this is the monster you need. +bitransverseScopeT + :: Applicative f + => (forall x x'. (x -> f x') -> t s x -> f (t' s' x')) -- ^ 'traverse'-like for @t@ + -> (forall x x'. (x -> f x') -> s x -> f (s' x')) -- ^ 'traverse'-like for @s@ + -> (a -> f a') + -> ScopeT b t s a + -> f (ScopeT b t' s' a') +bitransverseScopeT tauT tauS f = fmap ScopeT . tauT (traverse (tauS f)) . unscopeT +{-# INLINE bitransverseScopeT #-} + +-- $setup +-- >>> import Control.Monad.Trans.Maybe diff --git a/src/Control/Monad/Module.hs b/src/Control/Monad/Module.hs new file mode 100644 --- /dev/null +++ b/src/Control/Monad/Module.hs @@ -0,0 +1,56 @@ +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE MultiParamTypeClasses #-} +-- | Right monad 'Module' type-class. +-- +-- Most possible instances are omitted. +-- The primary use-case for 'Module' is to power 'Bound.ScopeH.ScopeH'. +module Control.Monad.Module where + +import Bound (Scope (..), (>>>=)) +import Control.Monad.Trans.Class (MonadTrans (..)) +import Data.Functor.Compose (Compose (..)) +import Data.Functor.Identity (Identity (..)) + +-- | @f@ is right @m@-module. (according to https://ncatlab.org/nlab/show/module+over+a+monad#modules definitions). +-- We have @'Compose' f m ~> f@ natural transformation. +-- +-- === Laws +-- +-- @ +-- fma '>>==' return = fma +-- fma '>>==' (f 'Control.Monad.>=>' g) = (fma '>>==' f) '>>==' g +-- @ +-- +-- === Properties +-- +-- For all @'Monad' m@ we can write associated @instance 'Module' m m where ('>>==') = ('>>=')@. +-- +-- 'mjoin' and '>>==' are equivalent in power: +-- +-- @ +-- fa '>>==' amb = 'mjoin' ('fmap' amb fa) +-- @ +class (Functor f, Monad m) => Module f m where + + -- | Called 'action'. + (>>==) :: f a -> (a -> m b) -> f b + +infixl 1 >>== + +-- | 'Module''s 'join' variant. +mjoin :: Module f m => f (m a) -> f a +mjoin fma = fma >>== id + +-- | @'Module' m (t m)@ action's implementation. +transAction :: (MonadTrans t, Monad m, Monad (t m)) => t m a -> (a -> m b) -> t m b +transAction tma amb = tma >>= lift . amb + +-- | @'Module' m ('Compose' f m)@ action's implementation. +composeAction :: (Functor f, Monad m) => Compose f m a -> (a -> m b) -> Compose f m b +composeAction (Compose fma) amb = Compose (fmap (>>= amb) fma) + +instance Monad m => Module m Identity where + fa >>== k = fmap (runIdentity . k) fa + +instance Monad m => Module (Scope b m) m where + (>>==) = (>>>=)