bound-extras 0.0.1 → 0.0.2

raw patch · 18 files changed

+933/−14 lines, 18 filesdep +adjunctionsdep ~basedep ~bifunctorsdep ~deepseqPVP ok

version bump matches the API change (PVP)

Dependencies added: adjunctions

Dependency ranges changed: base, bifunctors, deepseq, hashable, tasty, transformers

API changes (from Hackage documentation)

Files

• CHANGELOG.md +4/−0
• bound-extras.cabal +15/−8
• examples/Adjunctions.hs +13/−0
• examples/BiSTLC.hs +3/−0
• examples/BiSTLC2.hs +417/−0
• examples/BiSTLC3.hs +398/−0
• examples/Examples.hs +4/−0
• examples/Pretty.hs +5/−1
• examples/stlc-2-app-delta.txt +3/−0
• examples/stlc-2-arr-beta.txt +3/−0
• examples/stlc-2-pair-beta.txt +3/−0
• examples/stlc-2-redundant-case.txt +3/−0
• examples/stlc-2-sum-beta.txt +3/−0
• examples/stlc-3-arr-beta.txt +3/−0
• examples/stlc-3-pair-beta.txt +3/−0
• src/Bound/ScopeH.hs +21/−4
• src/Bound/ScopeT.hs +22/−1
• src/Control/Monad/Module.hs +10/−0

@@ -1,3 +1,7 @@+# 0.0.2++- Add `LiftedModule` allowing to lift into 'ScopeH'.+ # 0.0.1  - Relax 

@@ -1,6 +1,6 @@ cabal-version:      2.2 name:               bound-extras-version:            0.0.1+version:            0.0.2 synopsis:           ScopeH and ScopeT extras for bound category:           Language, Compilers, Interpreters description:@@ -27,9 +27,13 @@ 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.4 || ==8.6.5 || ==8.8.1-extra-source-files: CHANGELOG.md examples/*.txt+tested-with:+  GHC ==8.0.2 || ==8.2.2 || ==8.4.4 || ==8.6.5 || ==8.8.4 || ==8.10.4 || ==9.0.1 || ==9.2.1 +extra-source-files:+  CHANGELOG.md+  examples/*.txt+ source-repository head   type:     git   location: https://github.com/phadej/bound-extras@@ -45,14 +49,13 @@    -- GHC boot libraries   build-depends:-    , base          ^>=4.9.1.0 || ^>=4.10.1.0 || ^>=4.11.1.0 || ^>=4.12.0.0+    , base          ^>=4.9.1.0 || ^>=4.10.1.0 || ^>=4.11.1.0 || ^>=4.12.0.0 || ^>=4.13.0.0 || ^>=4.14.0.0 || ^>=4.15.0.0 || ^>=4.16.0.0     , deepseq       ^>=1.4.2.0-    , hashable      ^>=1.2.7.0+    , hashable      ^>=1.2.7.0 || ^>=1.3.0.0 || ^>=1.4.0.1     , transformers  ^>=0.5.0.0    -- other deps-  build-depends:-    , bound         ^>=2.0.1+  build-depends:    bound ^>=2.0.1    if !impl(ghc >=8.2)     build-depends: bifunctors ^>=5.5.3@@ -61,7 +64,10 @@   type:             exitcode-stdio-1.0   main-is:          Examples.hs   other-modules:+    Adjunctions     BiSTLC+    BiSTLC2+    BiSTLC3     Pretty     SystemF @@ -69,13 +75,14 @@   hs-source-dirs:   examples   ghc-options:      -Wall   build-depends:+    , adjunctions   ^>=4.4     , base     , bound     , bound-extras     , containers    ^>=0.5.7.1 || ^>=0.6.0.1     , filepath      ^>=1.4.1.1     , pretty        ^>=1.1.3.3-    , tasty         >=1.1.0.3 && <1.3+    , tasty         >=1.1.0.3 && <1.5     , tasty-golden  ^>=2.3.2     , text-short    ^>=0.1.2     , transformers  ^>=0.5.0.0

@@ -0,0 +1,13 @@+module Adjunctions where++import Data.Functor.Adjunction (Adjunction (..))++-- Defining 'mjoin' for monad arising from adjunction is easy:+-- every @r f@ is right module of @u f@.+mjoinAdj :: (Functor r, Adjunction f u) => r (f (u (f a))) -> r (f a)+mjoinAdj = fmap counit++-- However 'LiftedModule' is trickier, here we need +-- to know more.+mliftAdj :: (Functor r, Adjunction f u) => u (f a) -> r (f a)+mliftAdj = error "we need to know about r, f and u"

@@ -100,6 +100,9 @@     If c t e      >>== k = If (c >>== k) (t >>== k) (e >>== k)     FoldNat z s n >>== k = FoldNat (z >>== k) (s >>== k) (n >>== k) +instance LiftedModule Chk Inf where+    mlift = Inf+ lam_ :: Eq a => a -> Chk a -> Chk a lam_ x b = Lam (abstract1H x b) 

@@ -0,0 +1,417 @@+{-# LANGUAGE DeriveFoldable         #-}+{-# LANGUAGE DeriveFunctor          #-}+{-# LANGUAGE DeriveTraversable      #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE GADTs                  #-}+{-# LANGUAGE MultiParamTypeClasses  #-}+{-# LANGUAGE OverloadedStrings      #-}+module BiSTLC2 (tests) where++import Bound.ScopeH+import Bound.Var            (Var (..), unvar)+import Control.Monad        (ap)+import Control.Monad.Module+import Data.Bifunctor       (first)+import Data.String          (IsString (..))+import Data.Void            (Void)+import System.FilePath      ((-<.>), (</>))+import Test.Tasty           (TestTree, testGroup)+import Test.Tasty.Golden    (goldenVsString)++import qualified Data.ByteString.Lazy.UTF8 as UTF8+import qualified Data.Text.Short           as TS++import Pretty++-------------------------------------------------------------------------------+-- Types+-------------------------------------------------------------------------------++-- | Types.+data Ty+    = Ty ShortText+    | TUnit+    | Ty :+: Ty+    | Ty :*: Ty+    | Ty :-> Ty+  deriving Eq++infixr 2 :->+infix 4 :*:+infix 3 :+:++instance IsString Ty where+    fromString = Ty . fromString++-------------------------------------------------------------------------------+-- Infession+-------------------------------------------------------------------------------++-- | Inferable terms+data Inf ty a+    -- Variable+    = V a++    -- :-> Elimination+    | App (Inf ty a) (Chk ty a)++    -- :*: Elimination-1+    | Fst (Inf ty a)++    -- :*: Elimination-2+    | Snd (Inf ty a)++    -- annotated term+    | Ann (Chk ty a) ty+  deriving (Functor, Foldable, Traversable)++(.:) :: Chk ty a -> ty -> Inf ty a+(.:) = Ann+infix 1 .:++-- | Checkable terms+data Chk ty a+    -- Converted term+    = Inf (Inf ty a)++    -- :-> Introduction+    | Lam (ScopeH () (Chk ty) (Inf ty) a)++    -- :*: Introduction+    | Pair (Chk ty a) (Chk ty a)++    -- :+: Introduction-1+    | Inl (Chk ty a)++    -- :+: Introduction-2+    | Inr (Chk ty a)++    -- :+: Elimination+    | Case (Inf ty a) (ScopeH () (Chk ty) (Inf ty) a) (ScopeH () (Chk ty) (Inf ty) a)++  deriving (Functor, Foldable, Traversable)++-------------------------------------------------------------------------------+-- Instances+-------------------------------------------------------------------------------++instance IsString a => IsString (Inf ty a) where fromString = V . fromString+instance IsString a => IsString (Chk ty a) where fromString = Inf . fromString++instance Applicative (Inf ty) where+    pure = V+    (<*>) = ap++instance Monad (Inf ty) 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)+    Fst x    >>= k = Fst (x >>= k)+    Snd x    >>= k = Snd (x >>= k)++instance ty ~ ty' => Module (Chk ty) (Inf ty') where+    Inf x         >>== k = Inf (x >>= k)+    Lam b         >>== k = Lam (b >>== k)+    Pair x y      >>== k = Pair (x >>== k) (y >>== k)+    Inl x         >>== k = Inl (x >>== k)+    Inr y         >>== k = Inr (y >>== k)+    Case e c1 c2  >>== k = Case (e >>= k) (c1 >>== k) (c2 >>== k)++instance ty ~ ty' => LiftedModule (Chk ty) (Inf ty') where+    mlift = Inf++lam_ :: Eq a => a -> Chk ty a -> Chk ty a+lam_ x b = Lam (abstract1H x b)++case_ :: Eq a => Inf ty a -> a -> Chk ty a -> a -> Chk ty a -> Chk ty a+case_ e x c1 y c2 = Case e (abstract1H x c1) (abstract1H y c2)++-------------------------------------------------------------------------------+-- Pretty+-------------------------------------------------------------------------------++instance Pretty Ty where+    ppr = return . pprTy++pprTy :: Ty -> Doc+pprTy (Ty t)    = text (TS.unpack t)+pprTy TUnit     = text "Unit"+pprTy (a :*: b) = sexpr (text "prod") [pprTy a, pprTy b]+pprTy (a :+: b) = sexpr (text "sum") [pprTy a, pprTy b]+pprTy (a :-> b) = sexpr (text "->") $ map pprTy $ a : peelArr b++instance (Pretty a, Pretty ty) => Pretty (Inf ty a) where ppr x = traverse ppr x >>= pprInf+instance (Pretty a, Pretty ty) => Pretty (Chk ty a) where ppr x = traverse ppr x >>= pprChk++pprInf :: Pretty ty => Inf ty 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 (Fst x)  = do+    x' <- pprInf x+    return $ sexpr (text "fst") [x']+pprInf (Snd x)  = do+    x' <- pprInf x+    return $ sexpr (text "snd") [x']++pprChk :: Pretty ty => Chk ty 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 (Pair x y) = do+    x' <- pprChk x    +    y' <- pprChk y+    return $ sexpr (text "pair") [x', y']+pprChk (Inl x)  = do+    x' <- pprChk x+    return $ sexpr (text "inl") [x']+pprChk (Inr x)  = do+    x' <- pprChk x+    return $ sexpr (text "inr") [x']+pprChk (Case e c1 c2) = do+    e' <- pprInf e+    n1 <- text <$> fresh "x"+    n2 <- text <$> fresh "y"+    c1' <- pprChk (instantiate1H (V n1) c1)+    c2' <- pprChk (instantiate1H (V n2) c2)+    return $ sexpr (text "case+") [e', n1, c1', n2, c2']++-- We output+--   (0 1 2 3)+-- instead of+--   (((0 1) 2) 3)+-- small, but nice improvement!+peelApp :: Inf ty a -> (Inf ty a, [Chk ty a])+peelApp (App a b)   = (++ [b]) <$> peelApp a+peelApp e           = (e, [])++peelArr :: Ty -> [Ty]+peelArr (a :-> b) = a : peelArr b+peelArr x         = [x]++-------------------------------------------------------------------------------+-- peelApp+-------------------------------------------------------------------------------++infixl 2 $$++class SApp f g h | h -> f g where+    ($$) :: f a -> g a -> h a++instance SApp (Inf ty) (Chk ty) (Inf ty) where ($$) = App+instance SApp (Inf ty) (Chk ty) (Chk ty) where f $$ x = Inf (f $$ x)++-------------------------------------------------------------------------------+-- Normal form+-------------------------------------------------------------------------------++nfApp :: Chk ty a -> Chk ty a -> Maybe (Chk ty a)+nfApp (Inf f) x = Just $ Inf (App f x)+nfApp (Lam b) x        = chkBind (fromScopeH b) (unvar (const x) (Inf . V))+nfApp Pair {} _        = Nothing+nfApp Inl {}  _        = Nothing+nfApp Inr {}  _        = Nothing+nfApp (Case e c1 c2) x = do+    let x' = fmap F x+    c1' <- nfApp (fromScopeH c1) x'+    c2' <- nfApp (fromScopeH c2) x'+    Just $ Case e (toScopeH c1') (toScopeH c2')++nfFst :: Chk ty b -> Maybe (Chk ty b)+nfFst (Inf x)        = Just $ Inf (Fst x)+nfFst (Pair x _)     = Just x+nfFst Lam {}         = Nothing+nfFst Inl {}         = Nothing+nfFst Inr {}         = Nothing+nfFst (Case e c1 c2) = do+    c1' <- nfFst (fromScopeH c1)+    c2' <- nfFst (fromScopeH c2)+    Just $ Case e (toScopeH c1') (toScopeH c2')++nfSnd :: Chk ty b -> Maybe (Chk ty b)+nfSnd (Inf x)        = Just $ Inf (Snd x)+nfSnd (Pair x _)     = Just x+nfSnd Lam {}         = Nothing+nfSnd Inl {}         = Nothing+nfSnd Inr {}         = Nothing+nfSnd (Case e c1 c2) = do+    c1' <- nfSnd (fromScopeH c1)+    c2' <- nfSnd (fromScopeH c2)+    Just $ Case e (toScopeH c1') (toScopeH c2')++nfCase :: Chk ty a -> Chk ty (Var () a) -> Chk ty (Var () a) -> Maybe (Chk ty a)+nfCase (Inf e)        c1 c2 = Just $ Case e (toScopeH c1) (toScopeH c2)+nfCase (Inl x)        c1 _  = chkBind c1 (unvar (const x) (Inf . V))+nfCase (Inr y)        _  c2 = chkBind c2 (unvar (const y) (Inf . V))+nfCase Lam {}         _  _  = Nothing+nfCase Pair {}        _  _  = Nothing+nfCase (Case e d1 d2) c1 c2 = do+    let mkCase c = nfCase c (fmap F $ fromScopeH d1) (fmap F $ fromScopeH d2)+    c1' <- mkCase c1+    c2' <- mkCase c2+    Just $ Case e (toScopeH c1') (toScopeH c2') ++infBind :: Inf ty a -> (a -> Chk ty b) -> Maybe (Chk ty b)+infBind (Ann x _) k = chkBind x k+infBind (V x)     k = Just $ k x+infBind (App f x) k = do +    f' <- infBind f k+    x' <- chkBind x k+    nfApp f' x'+infBind (Fst x)   k = do+    x' <- infBind x k+    nfFst x'+infBind (Snd x)   k = do+    x' <- infBind x k+    nfSnd x'++chkBind :: Chk ty a -> (a -> Chk ty b) -> Maybe (Chk ty b)+chkBind (Inf a) k = infBind a k+chkBind (Lam b) k = do+    b' <- chkBind (fromScopeH b) (unvar (Inf . V . B) (fmap F . k))+    return $ Lam $ toScopeH b'+chkBind (Pair x y) k = do+    x' <- chkBind x k+    y' <- chkBind y k+    return $ Pair x' y'+chkBind (Inl x) k = do+    x' <- chkBind x k+    return $ Inl x'+chkBind (Inr y) k = do+    y' <- chkBind y k+    return $ Inl y'+chkBind (Case e c1 c2) k = do+    e' <- infBind e k+    c1' <- chkBind (fromScopeH c1) (unvar (Inf . V . B) (fmap F . k))+    c2' <- chkBind (fromScopeH c2) (unvar (Inf . V . B) (fmap F . k))+    nfCase e' c1' c2'++-------------------------------------------------------------------------------+-- Type-checking+-------------------------------------------------------------------------------++infer :: (a -> Ty) -> Inf Ty a -> Maybe (Chk Void a, Ty)+infer f = infer' . fmap (\x -> (x, f x))++-- No error reporting :)+infer' :: Inf Ty (a, Ty) -> Maybe (Chk Void a, Ty)+infer' (V (a, at)) = Just (Inf (V a), at)+infer' (Ann x t) = do+    x' <- check' x t+    Just (x', t)+infer' (App f x) = do+    (f', ft) <- infer' f+    case ft of+        a :-> b -> do+            x' <- check' x a+            t <- nfApp f' x'+            return (t, b)+        _       -> Nothing+infer' (Fst x) = do+    (x', xt) <- infer' x+    case xt of+        (a :*: _) -> do+            t <- nfFst x'+            return (t, a)+        _ -> Nothing+infer' (Snd x) = do+    (x', xt) <- infer' x+    case xt of+        (_ :*: b) -> do+            t <- nfSnd x'+            return (t, b)+        _ -> Nothing++check' :: Chk Ty (a, Ty) -> Ty -> Maybe (Chk Void a)+check' (Lam x) t = case t of+    a :-> b -> do+        let xx = fmap (unvar (\n -> (B n, a)) (first F)) $ fromScopeH x+        xx' <- check' xx b+        return $ Lam (toScopeH xx')+    _ -> Nothing+check' (Inf x) t = do+    (x', xt) <- infer' x+    if t == xt+    then Just x'+    else Nothing+check' (Pair x y) t = case t of+    a :*: b -> do+        x' <- check' x a+        y' <- check' y b+        return (Pair x' y')+    _ -> Nothing+check' (Inl x) t = case t of+    a :+: _ -> do+        x' <- check' x a+        return (Inl x')+    _ -> Nothing+check' (Inr y) t = case t of+    _ :+: b -> do+        y' <- check' y b+        return (Inl y')+    _ -> Nothing+check' (Case e c1 c2) t = do+    (e', et) <- infer' e+    case et of+        a :+: b -> do+            let cc1 = fmap (unvar (\n -> (B n, a)) (first F)) $ fromScopeH c1+            let cc2 = fmap (unvar (\n -> (B n, b)) (first F)) $ fromScopeH c2+            cc1' <- check' cc1 t+            cc2' <- check' cc2 t+            nfCase e' cc1' cc2'+        _ -> Nothing++-------------------------------------------------------------------------------+-- Examples+-------------------------------------------------------------------------------++demo :: String -> Inf Ty ShortText -> [String]+demo name e = case infer ctx e of+    Nothing ->+        [ name ++ " = " ++ pretty e+        , "DOESN'T TYPECHECK"+        ]+    Just (nf, t) ->+        [ name ++ " : " ++ pretty t+        , name ++ " = " ++ pretty e+        , name ++ " = " ++ pretty nf+        ]+  where+    ctx "f"   = "A" :-> "B"+    ctx "a"   = "A"+    ctx "b"   = "B"+    ctx "c" = "C"+    ctx "a2c" = "A" :-> "C"+    ctx "b2c" = "B" :-> "C"+    ctx "aorb" = "A" :+: "B"+    ctx "ac2d" = "A" :-> "C" :-> "D"+    ctx "bc2d" = "B" :-> "C" :-> "D"+    ctx "aa2b" = "A" :-> "A" :-> "B"+    ctx _     = TUnit++tests :: TestTree+tests = testGroup "Bi-directional STLC 2"+    [ demo' "arr-beta"  $ (lam_ "x" ("f" $$ "x") .: "A" :-> "B") $$ "a"+    , demo' "pair-beta" $ Fst (Pair "a" "b" .: "A" :*: "B")+    , demo' "sum-beta"  $ case_ (Inl "a" .: "A" :+: "B") "x" ("a2c" $$ "x") "y" ("b2c" $$ "y") .: "C"+    , demo' "app-delta" $ (case_ "aorb" "x" ("ac2d" $$"x") "y" ("bc2d" $$ "y") .: "C" :-> "D") $$ "c"+    , demo' "redundant-case" $+        (case_ "aorb" "x" (case_ "aorb" "u" ("aa2b" $$ "x" $$ "u") "v" "v") "y" "y".: "B")+    ]+  where+    demo' name e = goldenVsString name ("examples" </> name' -<.> "txt")+        $ return $ UTF8.fromString $ unlines+        $ demo name e+      where+        name' = "stlc-2-" ++ name+

@@ -0,0 +1,398 @@+{-# LANGUAGE DeriveFoldable         #-}+{-# LANGUAGE DeriveFunctor          #-}+{-# LANGUAGE DeriveTraversable      #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE GADTs                  #-}+{-# LANGUAGE MultiParamTypeClasses  #-}+{-# LANGUAGE OverloadedStrings      #-}+module BiSTLC3 (tests) where++import Bound.ScopeH+import Bound.Var            (Var (..), unvar)+import Control.Monad        (ap)+import Control.Monad.Module+import Data.Bifunctor       (first)+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 qualified Data.Text.Short           as TS++import Pretty++-------------------------------------------------------------------------------+-- Types+-------------------------------------------------------------------------------++-- | Types.+data Ty+    = Ty ShortText+    | TUnit+    | Ty :*: Ty+    | Ty :-> Ty+  deriving Eq++infixr 2 :->+infix 4 :*:++instance IsString Ty where+    fromString = Ty . fromString++-------------------------------------------------------------------------------+-- Elimession+-------------------------------------------------------------------------------++-- | Elimerable terms+data Elim a+    -- Variable+    = Var a++    -- :-> Elimination+    | App (Elim a) (Term a)++    -- :*: Elimination-1+    | Fst (Elim a)++    -- :*: Elimination-2+    | Snd (Elim a)++    -- annotated term+    | Ann (Term a) Ty+  deriving (Functor, Foldable, Traversable)++(.:) :: Term a -> Ty -> Elim a+(.:) = Ann+infix 1 .:++-- | Checkable terms+data Term a+    -- Converted term+    = Emb (Elim a)++    -- :-> Introduction+    | Lam (ScopeH () Term Elim a)++    -- :*: Introduction+    | Mul (Term a) (Term a)++  deriving (Functor, Foldable, Traversable)++-------------------------------------------------------------------------------+-- Instances+-------------------------------------------------------------------------------++instance IsString a => IsString (Elim a) where fromString = Var . fromString+instance IsString a => IsString (Term a) where fromString = Emb . fromString++instance Applicative Elim where+    pure = Var+    (<*>) = ap++instance Monad Elim where+    return = Var++    Var x      >>= k = k x+    Ann x t  >>= k = Ann (x >>== k) t+    App f x  >>= k = App (f >>= k) (x >>== k)+    Fst x    >>= k = Fst (x >>= k)+    Snd x    >>= k = Snd (x >>= k)++instance Module Term Elim where+    Emb x    >>== k = Emb (x >>= k)+    Lam b    >>== k = Lam (b >>== k)+    Mul x y  >>== k = Mul (x >>== k) (y >>== k)++instance LiftedModule Term Elim where+    mlift = Emb++lam_ :: Eq a => a -> Term a -> Term a+lam_ x b = Lam (abstract1H x b)++-------------------------------------------------------------------------------+-- Pretty+-------------------------------------------------------------------------------++instance Pretty Ty where+    ppr = return . pprTy++pprTy :: Ty -> Doc+pprTy (Ty t)    = text (TS.unpack t)+pprTy TUnit     = text "Unit"+pprTy (a :*: b) = sexpr (text "prod") [pprTy a, pprTy b]+pprTy (a :-> b) = sexpr (text "->") $ map pprTy $ a : peelArr b++instance Pretty a => Pretty (Elim a) where ppr x = traverse ppr x >>= pprElim+instance Pretty a => Pretty (Term a) where ppr x = traverse ppr x >>= pprTerm++pprElim :: Elim Doc -> PrettyM Doc+pprElim (Var x) = pure x+pprElim (App f x) = case peelApp f of+    (f', xs) -> sexpr+        <$> pprElim f'+        <*> traverse pprTerm (xs ++ [x])+pprElim (Ann x t) = do+    x' <- pprTerm x+    t' <- ppr t+    return $ sexpr (text "the") [t', x']+pprElim (Fst x)  = do+    x' <- pprElim x+    return $ sexpr (text "fst") [x']+pprElim (Snd x)  = do+    x' <- pprElim x+    return $ sexpr (text "snd") [x']++pprTerm :: Term Doc -> PrettyM  Doc+pprTerm (Emb e) = pprElim e+pprTerm (Lam b) = do+    n <- text <$> fresh "x"+    b' <- pprTerm (instantiate1H (Var n) b)+    return $ sexpr (text "fn") [ n, b' ]+pprTerm (Mul x y) = do+    x' <- pprTerm x    +    y' <- pprTerm y+    return $ sexpr (text "pair") [x', y']++-- We output+--   (0 1 2 3)+-- instead of+--   (((0 1) 2) 3)+-- small, but nice improvement!+peelApp :: Elim a -> (Elim a, [Term a])+peelApp (App a b)   = (++ [b]) <$> peelApp a+peelApp e           = (e, [])++peelArr :: Ty -> [Ty]+peelArr (a :-> b) = a : peelArr b+peelArr x         = [x]++-------------------------------------------------------------------------------+-- peelApp+-------------------------------------------------------------------------------++infixl 2 $$++class SApp f g h | h -> f g where+    ($$) :: f a -> g a -> h a++instance SApp Elim Term Elim where ($$) = App+instance SApp Elim Term Term where f $$ x = Emb (f $$ x)++-------------------------------------------------------------------------------+-- Normal form+-------------------------------------------------------------------------------++data NFElim a+    = NFElimNeu (UNeut a)+    | NFElimAnn (NFTerm a) Ty+  deriving (Functor, Foldable, Traversable)++data NFTerm a+    = NFEmb (UNeut a)+    | NFLam (ScopeH () NFTerm NFElim a)+    | NFMul (NFTerm a) (NFTerm a)+  deriving (Functor, Foldable, Traversable)++-- | Upsilon neutral eliminations+data UNeut a+    = NFVar a+    | NFApp (BNeut a) (NFTerm a)+    | NFFst (BNeut a)+    | NFSnd (BNeut a)+    | NFEvalPanic+  deriving (Functor, Foldable, Traversable)++-- | Beta neutral eliminations+data BNeut a+    = BNeutNeu (UNeut a)+    | BNeutAnnEmb (UNeut a) Ty+  deriving (Functor, Foldable, Traversable)++nfVar :: a -> NFElim a+nfVar = NFElimNeu . NFVar++nfApp :: NFElim a -> NFTerm a -> NFElim a+nfApp (NFElimNeu f)                   s =+    NFElimNeu (NFApp (BNeutNeu f) s)+nfApp (NFElimAnn (NFLam t) (a :-> b)) s =+    NFElimAnn (instantiate1H (NFElimAnn s a) t) b+nfApp (NFElimAnn (NFEmb u) ty) s =+    NFElimNeu (NFApp (BNeutAnnEmb u ty) s)+nfApp _ _ = NFElimNeu NFEvalPanic++nfFst :: NFElim a -> NFElim a+nfFst (NFElimNeu e) =+    NFElimNeu (NFFst (BNeutNeu e))+nfFst (NFElimAnn (NFMul t _) (a :*: _)) =+    NFElimAnn t a+nfFst (NFElimAnn (NFEmb u) ty) =+    NFElimNeu (NFFst (BNeutAnnEmb u ty))+nfFst _ = NFElimNeu NFEvalPanic++nfSnd :: NFElim a -> NFElim a+nfSnd (NFElimNeu e) =+    NFElimNeu (NFSnd (BNeutNeu e))+nfSnd (NFElimAnn (NFMul _ s) (_ :*: b)) =+    NFElimAnn s b+nfSnd (NFElimAnn (NFEmb u) ty) =+    NFElimNeu (NFSnd (BNeutAnnEmb u ty))+nfSnd _ = NFElimNeu NFEvalPanic++nfAnn :: NFTerm a -> Ty -> NFElim a+nfAnn = NFElimAnn++nfEmb :: NFElim a -> NFTerm a+nfEmb (NFElimNeu u) = NFEmb u+nfEmb (NFElimAnn t _) = t -- upsilon-reduction++instance Applicative NFElim where+    pure = nfVar+    (<*>) = ap++instance Monad NFElim where+    return = nfVar++    NFElimNeu e   >>= k = substU e k+    NFElimAnn t a >>= k = NFElimAnn (t >>== k) a++substU :: UNeut a -> (a -> NFElim b) -> NFElim b+substU (NFVar x)   k = k x+substU (NFApp f s) k = nfApp (substB f k) (s >>== k)+substU (NFFst e)   k = nfFst (substB e k)+substU (NFSnd e)   k = nfSnd (substB e k)+substU NFEvalPanic _ = NFElimNeu NFEvalPanic++substB :: BNeut a -> (a -> NFElim b) -> NFElim b+substB (BNeutNeu e)       k = substU e k+substB (BNeutAnnEmb e ty) k = nfAnn (nfEmb (substU e k)) ty++instance Module NFTerm NFElim where+    NFEmb u   >>== k = nfEmb (substU u k)+    NFLam b   >>== k = NFLam (b >>== k)+    NFMul t s >>== k = NFMul (t >>== k) (s >>== k)++-------------------------------------------------------------------------------+-- From normal forms to terms+-------------------------------------------------------------------------------++class ToTerm t where toTerm :: t a -> Term a+class ToElim t where toElim :: t a -> Elim a++instance ToTerm Term where toTerm = id+instance ToElim Elim where toElim = id++instance ToElim NFElim where+    toElim (NFElimNeu e)   = toElim e+    toElim (NFElimAnn t a) = Ann (toTerm t) a++instance ToElim BNeut where+    toElim (BNeutNeu e)       = toElim e+    toElim (BNeutAnnEmb e ty) = Ann (Emb (toElim e)) ty++instance ToElim UNeut where+    toElim (NFVar a)   = Var a+    toElim (NFApp f s) = App (toElim f) (toTerm s)+    toElim (NFFst e)   = Fst (toElim e)+    toElim (NFSnd e)   = Snd (toElim e)+    toElim NFEvalPanic = error "eval panic"++instance ToTerm NFTerm where+    toTerm (NFEmb e)   = Emb (toElim e)+    toTerm (NFLam t)   = Lam (toScopeH (toTerm (fromScopeH t)))+    toTerm (NFMul t s) = Mul (toTerm t) (toTerm s)+++-------------------------------------------------------------------------------+-- Type-checking+-------------------------------------------------------------------------------++-- infer and check return evaluated values as well.++infer :: (a -> Ty) -> Elim a -> Maybe (NFElim a, Ty)+infer f = infer' . fmap (\x -> (x, f x))++-- No error reporting :)+infer' :: Elim (a, Ty) -> Maybe (NFElim a, Ty)+infer' (Var (a, at)) = Just (nfVar a, at)+infer' (Ann x t) = do+    x' <- check' x t+    Just (nfAnn x' t, t)+infer' (App f x) = do+    (f', ft) <- infer' f+    case ft of+        a :-> b -> do+            x' <- check' x a+            return (nfApp f' x', b)+        _       -> Nothing+infer' (Fst x) = do+    (x', xt) <- infer' x+    case xt of+        (a :*: _) -> do+            return (nfFst x', a)+        _ -> Nothing+infer' (Snd x) = do+    (x', xt) <- infer' x+    case xt of+        (_ :*: b) -> do+            return (nfSnd x', b)+        _ -> Nothing++check' :: Term (a, Ty) -> Ty -> Maybe (NFTerm a)+check' (Lam x) t = case t of+    a :-> b -> do+        let xx = fmap (unvar (\n -> (B n, a)) (first F)) $ fromScopeH x+        xx' <- check' xx b+        return $ NFLam (toScopeH xx')+    _ -> Nothing+check' (Emb x) t = do+    (x', xt) <- infer' x+    if t == xt+    then Just (nfEmb x')+    else Nothing+check' (Mul x y) t = case t of+    a :*: b -> do+        x' <- check' x a+        y' <- check' y b+        return (NFMul x' y')+    _ -> Nothing++-------------------------------------------------------------------------------+-- Examples+-------------------------------------------------------------------------------++demo :: String -> Elim ShortText -> [String]+demo name e = case infer ctx e of+    Nothing ->+        [ name ++ " = " ++ pretty e+        , "DOESN'T TYPECHECK"+        ]+    Just (nf, t) ->+        [ name ++ " : " ++ pretty t+        , name ++ " = " ++ pretty e+        , name ++ " = " ++ pretty (toElim nf)+        ]+  where+    ctx "f"   = "A" :-> "B"+    ctx "a"   = "A"+    ctx "b"   = "B"+    ctx "c" = "C"+    ctx "a2c" = "A" :-> "C"+    ctx "b2c" = "B" :-> "C"+    ctx "ac2d" = "A" :-> "C" :-> "D"+    ctx "bc2d" = "B" :-> "C" :-> "D"+    ctx "aa2b" = "A" :-> "A" :-> "B"+    ctx _     = TUnit++tests :: TestTree+tests = testGroup "Bi-directional STLC 3"+    [ demo' "arr-beta"  $ (lam_ "x" ("f" $$ "x") .: "A" :-> "B") $$ "a"+    , demo' "pair-beta" $ Fst (Mul "a" "b" .: "A" :*: "B")+    ]+  where+    demo' name e = goldenVsString name ("examples" </> name' -<.> "txt")+        $ return $ UTF8.fromString $ unlines+        $ demo name e+      where+        name' = "stlc-3-" ++ name+

@@ -1,6 +1,8 @@ module Main (main) where  import qualified BiSTLC+import qualified BiSTLC2+import qualified BiSTLC3 import qualified SystemF  import Test.Tasty           (testGroup, defaultMain)@@ -8,5 +10,7 @@ main :: IO () main = defaultMain $ testGroup "Examples"     [ BiSTLC.tests+    , BiSTLC2.tests+    , BiSTLC3.tests     , SystemF.tests     ]

@@ -11,8 +11,9 @@     ) where  import Control.Monad.Trans.State.Strict+import Data.Char                        (isDigit) import Data.Text.Short                  (ShortText)-import Data.Char (isDigit)+import Data.Void                        (Void, absurd)  import qualified Data.Text.Short  as TS import qualified Text.PrettyPrint as PP@@ -61,3 +62,6 @@     ppr t = do         markUsed t         return $ PP.text $ TS.unpack t++instance Pretty Void where+    ppr = absurd

@@ -0,0 +1,3 @@+app-delta : D+app-delta = ((the (-> C D) (case+ aorb x (ac2d x) y (bc2d y))) c)+app-delta = (case+ aorb x (ac2d x c) y (bc2d y c))

@@ -0,0 +1,3 @@+arr-beta : B+arr-beta = ((the (-> A B) (fn x (f x))) a)+arr-beta = (f a)

@@ -0,0 +1,3 @@+pair-beta : A+pair-beta = (fst (the (prod A B) (pair a b)))+pair-beta = a

@@ -0,0 +1,3 @@+redundant-case : B+redundant-case = (the B (case+ aorb x (case+ aorb x0 (aa2b x x0) y0 y0) y y))+redundant-case = (case+ aorb x (case+ aorb x0 (aa2b x x0) y0 y0) y y)

@@ -0,0 +1,3 @@+sum-beta : C+sum-beta = (the C (case+ (the (sum A B) (inl a)) x (a2c x) y (b2c y)))+sum-beta = (a2c a)

@@ -0,0 +1,3 @@+arr-beta : B+arr-beta = ((the (-> A B) (fn x (f x))) a)+arr-beta = (the B (f a))

@@ -0,0 +1,3 @@+pair-beta : A+pair-beta = (fst (the (prod A B) (pair a b)))+pair-beta = (the A a)

@@ -3,6 +3,7 @@ {-# LANGUAGE FlexibleInstances     #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE RankNTypes            #-}+{-# LANGUAGE ScopedTypeVariables   #-} {-# LANGUAGE UndecidableInstances  #-} -- | 'ScopeH' scope, which allows substitute 'f' into 'g' to get new 'g'. --@@ -17,7 +18,7 @@ -- we diffentiate between @Poly@ and @Mono@-morphic types. -- -- @--- specialise :: Poly a -> Mono a -> Poly a +-- specialise :: Poly a -> Mono a -> Poly a -- specialise (Forall p) m = 'instantiate1H' m p -- specialise _          _ = error "ill-kinded" -- @@@ -25,7 +26,7 @@ -- 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'. --@@ -37,6 +38,8 @@     abstractHName, abstract1HName,     -- * Instantiation     instantiateH, instantiate1H, instantiateHEither,+    -- * Lifting+    liftScopeH,     -- * Traditional de Bruijn     fromScopeH,     toScopeH,@@ -60,7 +63,7 @@ import Bound                (Scope (..), Var (..)) import Bound.Name           (Name (..)) import Control.DeepSeq      (NFData (..))-import Control.Monad.Module (Module (..))+import Control.Monad.Module (Module (..), LiftedModule (..)) import Data.Bifoldable      (bifoldMap, bitraverse_) import Data.Bifunctor       (bimap) import Data.Bitraversable   (Bitraversable (..))@@ -82,6 +85,9 @@ instance (Functor f, Monad m) => Module (ScopeH b f m) m where     ScopeH s >>== k = ScopeH $ fmap (fmap (>>= k)) s +instance LiftedModule f m => LiftedModule (ScopeH b f m) m where+    mlift = liftScopeH+ ------------------------------------------------------------------------------- -- Instances -------------------------------------------------------------------------------@@ -199,9 +205,20 @@ -- | 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)+    B b  -> f (Left b)     F ea -> ea >>= f . Right {-# INLINE instantiateHEither #-}++-------------------------------------------------------------------------------+-- Lifting+-------------------------------------------------------------------------------++-- |+--+-- @since 0.0.2+liftScopeH:: forall f m a b. LiftedModule f m => m a -> ScopeH b f m a+liftScopeH m = ScopeH (mlift (return (F m) :: m (Var b (m a))))+{-# INLINE liftScopeH #-}  ------------------------------------------------------------------------------- -- Traditional de Bruijn

@@ -20,6 +20,8 @@     abstractTName, abstract1TName,     -- * Instantiation     instantiateT, instantiate1T, instantiateTEither,+    -- * Lifting+    liftScopeT,     -- * Traditional de Bruijn     fromScopeT,     toScopeT,@@ -41,7 +43,7 @@ import Bound                (Bound (..), Scope (..), Var (..)) import Bound.Name           (Name (..)) import Control.DeepSeq      (NFData (..))-import Control.Monad.Module (Module (..))+import Control.Monad.Module (Module (..), LiftedModule (..)) import Data.Bifoldable      (bifoldMap, bitraverse_) import Data.Bifunctor       (bimap) import Data.Bitraversable   (Bitraversable (..))@@ -88,6 +90,14 @@ instance (Monad f, Functor (t f)) => Module (ScopeT b t f) f where     (>>==) = (>>>>=) +instance (Monad f, Monad (t f)) => LiftedModule (ScopeT b t f) f where+    mlift = liftScopeT++-- we can define this, as we need Monad (t m).+-- QuantifiedConstraint for transformers would solve that.+-- instance MonadTrans (ScopeT b t) where+--     lift = mlift+ 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 #-}@@ -197,6 +207,17 @@     B b -> f (Left b)     F ea -> ea >>= f . Right {-# INLINE instantiateTEither #-}++-------------------------------------------------------------------------------+-- Lifting+-------------------------------------------------------------------------------++-- |+--+-- @since 0.0.2+liftScopeT:: forall t f a b. (Monad (t f)) => f a -> ScopeT b t f a+liftScopeT = ScopeT . return . F+{-# INLINE liftScopeT #-}  ------------------------------------------------------------------------------- -- Traditional de Bruijn

@@ -54,3 +54,13 @@  instance Monad m => Module (Scope b m) m where     (>>==) = (>>>=)++-- | An extension of 'Module' allowing to lift @m a@ info @f a@.+-- As we have @'Monad' m@, this allows to have a pseudo-return for @f@:+-- @point . return :: a -> f a@+--+-- /Note:/ for @f = t m@ for some @'MonadTrans' t@ @'mlift' = 'lift'@.+--+-- @since 0.0.2+class Module f m => LiftedModule f m where+    mlift :: m a -> f a