bound-extras (empty) → 0

raw patch · 19 files changed

+1623/−0 lines, 19 filesdep +basedep +bifunctorsdep +boundsetup-changed

Dependencies added: base, bifunctors, bound, bound-extras, containers, deepseq, filepath, hashable, pretty, tasty, tasty-golden, text-short, transformers, utf8-string

Files

LICENSE +30/−0
Setup.hs +2/−0
bound-extras.cabal +95/−0
examples/BiSTLC.hs +329/−0
examples/Examples.hs +12/−0
examples/Pretty.hs +63/−0
examples/SystemF.hs +335/−0
examples/stlc-four-mult.txt +15/−0
examples/stlc-four-plus.txt +5/−0
examples/stlc-id.txt +3/−0
examples/stlc-not-tt.txt +3/−0
examples/sysf-0.txt +3/−0
examples/sysf-1.txt +6/−0
examples/sysf-2.txt +10/−0
examples/sysf-id.txt +3/−0
examples/sysf-suc.txt +7/−0
src/Bound/ScopeH.hs +330/−0
src/Bound/ScopeT.hs +316/−0
src/Control/Monad/Module.hs +56/−0

+ LICENSE view

@@ -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.

+ Setup.hs view

@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain

+ bound-extras.cabal view

@@ -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 <oleg.grenrus@iki.fi>+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

+ examples/BiSTLC.hs view

@@ -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

+ examples/Examples.hs view

@@ -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+    ]

+ examples/Pretty.hs view

@@ -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

+ examples/SystemF.hs view

@@ -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

+ examples/stlc-four-mult.txt view

@@ -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

+ examples/stlc-four-plus.txt view

@@ -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

+ examples/stlc-id.txt view

@@ -0,0 +1,3 @@+id : (-> Nat Nat)+id = (the (-> Nat Nat) (fn x x))+id = (the (-> Nat Nat) (fn x x))

+ examples/stlc-not-tt.txt view

@@ -0,0 +1,3 @@+not-tt : Bool+not-tt = ((the (-> Bool Bool) (fn x (if x #f #t))) #t)+not-tt = #f

+ examples/sysf-0.txt view

@@ -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)))

+ examples/sysf-1.txt view

@@ -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))))

+ examples/sysf-2.txt view

@@ -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)))))

+ examples/sysf-id.txt view

@@ -0,0 +1,3 @@+id : (-> a a)+id = (poly b (fn (the b x) x))+id = (poly b (fn (the b x) x))

+ examples/sysf-suc.txt view

@@ -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))))))

+ src/Bound/ScopeH.hs view

@@ -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 #-}

+ src/Bound/ScopeT.hs view

@@ -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

+ src/Control/Monad/Module.hs view

@@ -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+    (>>==) = (>>>=)