binder (empty) → 0.1
raw patch · 7 files changed
+743/−0 lines, 7 filesdep +basedep +binderdep +containers
Dependencies added: base, binder, containers, hspec, lens, text, transformers
Files
- CHANGELOG.md +7/−0
- LICENSE +20/−0
- binder.cabal +70/−0
- src/Data/Binder.hs +255/−0
- test/Binder1Spec.hs +147/−0
- test/Binder2Spec.hs +243/−0
- test/Spec.hs +1/−0
+ CHANGELOG.md view
@@ -0,0 +1,7 @@+# Revision history for binder++## version 0++### 0.1 -- 2023-10-04++Initial release.
+ LICENSE view
@@ -0,0 +1,20 @@+Copyright (c) 2023 Keito Kajitani++Permission is hereby granted, free of charge, to any person obtaining+a copy of this software and associated documentation files (the+"Software"), to deal in the Software without restriction, including+without limitation the rights to use, copy, modify, merge, publish,+distribute, sublicense, and/or sell copies of the Software, and to+permit persons to whom the Software is furnished to do so, subject to+the following conditions:++The above copyright notice and this permission notice shall be included+in all copies or substantial portions of the Software.++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,+EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.+IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY+CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT,+TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE+SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ binder.cabal view
@@ -0,0 +1,70 @@+cabal-version: 3.0+name: binder+version: 0.1+synopsis: Variable binding for abstract syntax tree+description:+ binder is purely functional implementation of Ocaml's+ <https://github.com/rlepigre/ocaml-bindlib bindlib>.+ It follows the style of higher-order abstract syntax,+ and offers the representation of abstract syntax tree.+license: MIT+license-file: LICENSE+author: Keito Kajitani <ijaketak@gmail.com>+maintainer: Keito Kajitani <ijaketak@gmail.com>+copyright: (c) 2023 Keito Kajitani+homepage: https://github.com/ijaketak/binder+category: Data+build-type: Simple+tested-with:+ GHC == 9.2.8+ , GHC == 9.4.7+ , GHC == 9.6.3+extra-doc-files: CHANGELOG.md+-- extra-source-files:++source-repository head+ type: git+ location: https://github.com/ijaketak/binder++source-repository this+ type: git+ location: https://github.com/ijaketak/binder+ tag: 0.1++common depends+ build-depends:+ containers < 0.8+ , text < 2.2+ , transformers < 0.7++common warnings+ ghc-options: -Wall++library+ import: depends, warnings+ exposed-modules:+ Data.Binder+ -- other-modules:+ -- other-extensions:+ build-depends:+ base < 4.19+ , lens < 5.3+ hs-source-dirs: src+ default-language: Haskell2010++test-suite binder-test+ import: depends, warnings+ default-language: Haskell2010+ other-modules:+ Binder1Spec+ , Binder2Spec+ -- other-extensions:+ type: exitcode-stdio-1.0+ hs-source-dirs: test+ main-is: Spec.hs+ build-depends:+ base < 4.19+ , binder+ , hspec < 2.12+ build-tool-depends:+ hspec-discover:hspec-discover < 2.12
+ src/Data/Binder.hs view
@@ -0,0 +1,255 @@+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}++{-|+Module : Data.Binder+Description : Variable binding for abstract syntax tree+Copyright : (c) 2023 Keito Kajitani+License : MIT+Maintainer : Keito Kajitani <ijaketak@gmail.com>++binder is purely functional implementation of Ocaml's bindlib.+It follows the style of higher-order abstract syntax,+and offers the representation of abstract syntax tree.+-}+module Data.Binder+-- * Preliminaries+ ( MonadNumbering(..)+-- * Variable and Box+ , Var+ , Box+ , MkFree(..)+-- ** Variable+ , var'Key+ , var'Name+ , var'Box+ , nameOf+ , boxVar+ , newVar+ , isClosed+ , occur+-- ** Box+ , unbox+ , box+ , apBox+ , boxApply+ , boxApply2+ , boxApply3+ , boxApply4+ , boxPair+ , boxTriple+ , boxT+-- * Variable binding+ , Binder+ , binder'Name+ , binder'Body+ , subst+ , buildBinder+ , bind+ , unbind+ , eqBinder+ , boxBinder+ ) where++import Control.Lens+import Data.Kind (Type)+import qualified Data.Map.Lazy as M+import Data.Maybe (fromJust)+import Data.Text (Text)+import Unsafe.Coerce++-- | Numbering monad.+class (Monad m, Ord (Numbering m)) => MonadNumbering m where+ type Numbering m :: Type+ numbering :: m (Numbering m)++-- | Representation of variable+-- for abstract syntax tree type @a@+-- with base numbering monad @m@.+data Var m a = Var+ { _var'Key :: !(Numbering m)+ , _var'Body :: VarBody m a+ }+data VarBody m a = VarBody+ { _varBody'Name :: Text+ , _varBody'Box :: Box m a+ }+-- | Representation of under-construction things+-- having type @a@ and containing variables.+data Box m a+ = Box'Closed a+ | Box'Env (EnvVar m) (Closure m a)++-- | Typeclass for free variable constructor.+class MkFree m a where+ mkFree :: Var m a -> a++data AnyVar m = forall a. MkFree m a => AnyVar (Var m a)+type EnvVar m = M.Map (Numbering m) (AnyVar m)+data AnyMkFree m = forall a. MkFree m a => AnyMkFree a+type EnvMkFree m = M.Map (Numbering m) (AnyMkFree m)+newtype Closure m a = Closure { unClosure :: (EnvMkFree m) -> a }++instance Functor (Closure m) where+ fmap f cla = Closure $ f . unClosure cla++instance Applicative (Closure m) where+ pure a = Closure $ const a+ clf <*> cla = Closure $ \env -> unClosure clf env $ unClosure cla env++instance MonadNumbering m => Eq (Var m a) where+ Var x _ == Var y _ = x == y++instance MonadNumbering m => Ord (Var m a) where+ Var x _ `compare` Var y _ = x `compare` y++$(makeLenses ''Var)+$(makeLenses ''VarBody)+++var'Name :: Lens' (Var m a) Text+var'Name = var'Body . varBody'Name+var'Box :: Lens' (Var m a) (Box m a)+var'Box = var'Body . varBody'Box++instance Show (Var m a) where+ showsPrec n x = showsPrec n $ x ^. var'Name+instance Show (VarBody m a) where+ showsPrec n x = showsPrec n $ x ^. varBody'Name+instance Show (AnyVar m) where+ showsPrec n (AnyVar x) = showsPrec n $ x ^. var'Name++-- | The name of variable.+nameOf :: Var m a -> Text+nameOf x = x ^. var'Name++-- | Smart constructor for 'Box'.+boxVar :: Var m a -> Box m a+boxVar x = x ^. var'Box++-- | Create a new variable with given name.+newVar :: forall m a. (MkFree m a, MonadNumbering m) => Text -> m (Var m a)+newVar name = do+ i <- numbering+ let x = let b = Box'Env+ (M.singleton i $ AnyVar x)+ (Closure $ \env ->+ let f (AnyMkFree y) = unsafeCoerce y+ in f $ fromJust $ M.lookup i env)+ in Var i $ VarBody name b+ return x+++-- | 'Box' is closed if it exposes no free variables.+isClosed :: Box m a -> Bool+isClosed Box'Closed{} = True+isClosed Box'Env{} = False++-- | Check if the variable occurs in the box.+occur :: MonadNumbering m => Var m a -> Box m b -> Bool+occur _ (Box'Closed _) = False+occur v (Box'Env vs _) = M.member (v ^. var'Key) vs+++instance Functor (Box m) where+ fmap f (Box'Closed a) = Box'Closed (f a)+ fmap f (Box'Env vs ta) = Box'Env vs (f <$> ta)++instance (MonadNumbering m) => Applicative (Box m) where+ pure = Box'Closed+ Box'Closed f <*> Box'Closed a = Box'Closed (f a)+ Box'Closed f <*> Box'Env va ta = Box'Env va (f <$> ta)+ Box'Env vf tf <*> Box'Closed a = Box'Env vf (appClosure tf a)+ where+ appClosure clf x = Closure $ \env -> unClosure clf env x+ Box'Env vf tf <*> Box'Env va ta = Box'Env (M.union vf va) (tf <*> ta)++-- | Pick out and complete the construction of @a@.+unbox :: forall m a. Box m a -> a+unbox (Box'Closed t) = t+unbox (Box'Env env cl) = unClosure cl $ f <$> env+ where+ f (AnyVar x) = AnyMkFree @m $ mkFree x++box :: MonadNumbering m => a -> Box m a+box = pure+apBox :: MonadNumbering m => Box m (a -> b) -> Box m a -> Box m b+apBox = (<*>)+boxApply :: (a -> b) -> Box m a -> Box m b+boxApply = fmap+boxApply2 :: MonadNumbering m => (a -> b -> c) -> Box m a -> Box m b -> Box m c+boxApply2 f ta tb = f <$> ta <*> tb+boxApply3 :: MonadNumbering m => (a -> b -> c -> d) -> Box m a -> Box m b -> Box m c -> Box m d+boxApply3 f ta tb tc = f <$> ta <*> tb <*> tc+boxApply4 :: MonadNumbering m => (a -> b -> c -> d -> e) -> Box m a -> Box m b -> Box m c -> Box m d -> Box m e+boxApply4 f ta tb tc td = f <$> ta <*> tb <*> tc <*> td+boxPair :: MonadNumbering m => Box m a -> Box m b -> Box m (a, b)+boxPair = boxApply2 (,)+boxTriple :: MonadNumbering m => Box m a -> Box m b -> Box m c -> Box m (a, b, c)+boxTriple = boxApply3 (,,)+boxT :: (MonadNumbering m, Traversable t) => t (Box m a) -> Box m (t a)+boxT = sequenceA+++-- | Variable binding.+-- Essentially, @Binder a b@ means @a -> b@.+data Binder a b = Binder+ { _binder'Name :: Text+ , _binder'Body :: a -> b+ }++$(makeLenses ''Binder)++-- | Variable substitution.+subst :: Binder a b -> a -> b+subst b = b ^. binder'Body++-- | unbinding+unbind :: (MkFree m a, MonadNumbering m) => Binder a b -> m (Var m a, b)+unbind b = do+ x <- newVar $ b ^. binder'Name+ return (x, subst b $ mkFree x)++unbind2 :: (MkFree m a, MonadNumbering m)+ => Binder a b1 -> Binder a b2 -> m (Var m a, b1, b2)+unbind2 b1 b2 = do+ x <- newVar $ b1 ^. binder'Name+ let v = mkFree x+ return (x, subst b1 v, subst b2 v)++-- | Check if two bindings are equal.+eqBinder :: (MkFree m a, MonadNumbering m)+ => (b -> b -> m Bool) -> Binder a b -> Binder a b -> m Bool+eqBinder eq f g = do+ (_, t, u) <- unbind2 f g+ eq t u+++-- | Smart constructor for 'Binder'.+buildBinder :: Var m a -> (a -> b) -> Binder a b+buildBinder x body = Binder (x ^. var'Name) body++-- | binding+bind :: (MkFree m a, MonadNumbering m)+ => Var m a -> Box m b -> Box m (Binder a b)+bind x (Box'Closed t) = Box'Closed $ buildBinder x $ const t+bind x (Box'Env vs t) =+ let vs' = M.delete (x ^. var'Key) vs in if length vs' == 0+ then Box'Closed $ buildBinder x $+ \arg -> unClosure t $ M.singleton (x ^. var'Key) (AnyMkFree arg)+ else Box'Env vs' $ Closure $+ \ms -> buildBinder x $+ \arg -> unClosure t $ M.insert (x ^. var'Key) (AnyMkFree arg) ms++boxBinder :: (MkFree m a, MonadNumbering m)+ => (b -> m (Box m b)) -> Binder a b -> m (Box m (Binder a b))+boxBinder f b = do+ (x, t) <- unbind b+ ft <- f t+ return $ bind x ft
+ test/Binder1Spec.hs view
@@ -0,0 +1,147 @@+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE TypeFamilies #-}++module Binder1Spec where++import Control.Monad.IO.Class (MonadIO)+import Control.Monad.Trans.State.Strict (evalStateT, get, modify, StateT)+import Data.Text (Text)+import GHC.Generics hiding (S)+import Prelude hiding (abs)+import Test.Hspec++import Data.Binder++newtype S a = S { runS :: StateT Int IO a }+ deriving+ ( Generic+ , Generic1+ , Functor+ , Applicative+ , Monad+ , MonadIO+ )++instance MonadNumbering S where+ type Numbering S = Int+ numbering = do+ i <- S $ get+ S $ modify succ+ return i++-- This example is stolen from the documentation of bindlib.+-- https://github.com/rlepigre/ocaml-bindlib/blob/master/lib/bindlib.mli++data Term+ = Term'Var (Var S Term)+ | Term'Abs (Binder Term Term)+ | Term'App Term Term++instance MkFree S Term where+ mkFree = Term'Var++var :: Var S Term -> Box S Term+var = boxVar+absRaw :: Box S (Binder Term Term) -> Box S Term+absRaw = fmap Term'Abs+abs :: Var S Term -> Box S Term -> Box S Term+abs x t = absRaw $ bind x t+app :: Box S Term -> Box S Term -> Box S Term+app t u = Term'App <$> t <*> u+boxTerm :: Term -> S (Box S Term)+boxTerm (Term'Var x) = return $ var x+boxTerm (Term'Abs b) = absRaw <$> boxBinder boxTerm b+boxTerm (Term'App t u) = app <$> boxTerm t <*> boxTerm u++eval :: Term -> Term+eval t@(Term'App f a) = case eval f of+ Term'Abs b -> eval (subst b a)+ _ -> t+eval t = t++size :: Term -> S Int+size (Term'Var _) = return 0+size (Term'Abs b) = do+ (_, t) <- unbind b+ i <- size t+ return $ succ i+size (Term'App t u) = do+ i <- size t+ j <- size u+ return $ succ $ i + j++showTerm :: Term -> S Text+showTerm (Term'Var x) = return $ nameOf x+showTerm (Term'Abs b) = do+ (x, t) <- unbind b+ sh <- showTerm t+ return $ "\\" <> nameOf x <> "." <> sh+showTerm (Term'App t u) = do+ sht <- showTerm t+ shu <- showTerm u+ return $ "(" <> sht <> ") (" <> shu <> ")"++termIdentity, termFst, termDelta, termOmega :: S Term+termIdentity = do+ x <- newVar "x"+ return $ unbox $ abs x $ var x+termFst = do+ x <- newVar "x"+ y <- newVar "y"+ return $ unbox $ abs x $ abs y $ var x+termDelta = do+ x <- newVar "x"+ return $ unbox $ abs x $ app (var x) (var x)+termOmega = do+ delta <- box <$> termDelta+ return $ unbox $ app delta delta++spec :: Spec+spec = do+ describe "termIdentity" $ do+ it "should be size 1" $ do+ let r = 1+ flip shouldReturn r $ flip evalStateT 0 $ runS $ do+ t <- termIdentity+ size t+ it "should be shown the intended text" $ do+ let r = "\\x.x"+ flip shouldReturn r $ flip evalStateT 0 $ runS $ do+ t <- termIdentity+ showTerm t+ describe "termFst" $ do+ it "should be size 2" $ do+ let r = 2+ flip shouldReturn r $ flip evalStateT 0 $ runS $ do+ t <- termFst+ size t+ it "should be shown the intended text" $ do+ let r = "\\x.\\y.x"+ flip shouldReturn r $ flip evalStateT 0 $ runS $ do+ t <- termFst+ showTerm t+ describe "termDelta" $ do+ it "should be size 2" $ do+ let r = 2+ flip shouldReturn r $ flip evalStateT 0 $ runS $ do+ t <- termDelta+ size t+ it "should be shown the intended text" $ do+ let r = "\\x.(x) (x)"+ flip shouldReturn r $ flip evalStateT 0 $ runS $ do+ t <- termDelta+ showTerm t+ describe "termOmega" $ do+ it "should be size 5" $ do+ let r = 5+ flip shouldReturn r $ flip evalStateT 0 $ runS $ do+ t <- termOmega+ size t+ it "should be shown the intended text" $ do+ let r = "(\\x.(x) (x)) (\\x.(x) (x))"+ flip shouldReturn r $ flip evalStateT 0 $ runS $ do+ t <- termOmega+ showTerm t
+ test/Binder2Spec.hs view
@@ -0,0 +1,243 @@+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE TypeFamilies #-}++module Binder2Spec where++import Control.Monad.IO.Class (MonadIO)+import Control.Monad.Trans.State.Strict (evalStateT, get, modify, StateT)+import qualified Data.Map.Lazy as M+import Data.Text (Text)+import GHC.Generics hiding (S)+import Test.Hspec++import Data.Binder++newtype S a = S { runS :: StateT Int IO a }+ deriving+ ( Generic+ , Generic1+ , Functor+ , Applicative+ , Monad+ , MonadIO+ )++instance MonadNumbering S where+ type Numbering S = Int+ numbering = do+ i <- S $ get+ S $ modify succ+ return i++-- This example is stolen from the paper+-- Abstract Representation of Binders in OCaml using the Bindlib Library.+-- https://cgi.cse.unsw.edu.au/~eptcs/paper.cgi?LFMTP2018.4++data Ty+ = Ty'Var (Var S Ty)+ | Ty'Arr Ty Ty+ | Ty'All (Binder Ty Ty)++data Te+ = Te'Var (Var S Te)+ | Te'Abs Ty (Binder Te Te)+ | Te'App Te Te+ | Te'Lam (Binder Ty Te)+ | Te'Spe Te Ty++instance MkFree S Ty where+ mkFree = Ty'Var+instance MkFree S Te where+ mkFree = Te'Var++ty'Var :: Var S Ty -> Box S Ty+ty'Var = boxVar+ty'Arr :: Box S Ty -> Box S Ty -> Box S Ty+ty'Arr a b = Ty'Arr <$> a <*> b+ty'AllRaw :: Box S (Binder Ty Ty) -> Box S Ty+ty'AllRaw = fmap Ty'All+ty'All :: Var S Ty -> Box S Ty -> Box S Ty+ty'All x t = ty'AllRaw $ bind x t++te'Var :: Var S Te -> Box S Te+te'Var = boxVar+te'AbsRaw :: Box S Ty -> Box S (Binder Te Te) -> Box S Te+te'AbsRaw a f = Te'Abs <$> a <*> f+te'Abs :: Box S Ty -> Var S Te -> Box S Te -> Box S Te+te'Abs a x t = te'AbsRaw a $ bind x t+te'App :: Box S Te -> Box S Te -> Box S Te+te'App t u = Te'App <$> t <*> u+te'LamRaw :: Box S (Binder Ty Te) -> Box S Te+te'LamRaw = fmap Te'Lam+te'Lam :: Var S Ty -> Box S Te -> Box S Te+te'Lam x t = te'LamRaw $ bind x t+te'Spe :: Box S Te -> Box S Ty -> Box S Te+te'Spe t a = Te'Spe <$> t <*> a++boxTy :: Ty -> S (Box S Ty)+boxTy (Ty'Var x) = return $ ty'Var x+boxTy (Ty'Arr a b) = ty'Arr <$> boxTy a <*> boxTy b+boxTy (Ty'All f) = ty'AllRaw <$> boxBinder boxTy f+boxTe :: Te -> S (Box S Te)+boxTe (Te'Var x) = return $ te'Var x+boxTe (Te'Abs a f) = te'AbsRaw <$> boxTy a <*> boxBinder boxTe f+boxTe (Te'App t u) = te'App <$> boxTe t <*> boxTe u+boxTe (Te'Lam f) = te'LamRaw <$> boxBinder boxTe f+boxTe (Te'Spe t a) = te'Spe <$> boxTe t <*> boxTy a++hnf :: Te -> Te+hnf (Te'App t u) = let v = hnf u in case hnf t of+ Te'Abs _ b -> hnf $ subst b v+ h -> Te'App h v+hnf (Te'Spe t a) = case hnf t of+ Te'Lam b -> hnf $ subst b a+ h -> Te'Spe h a+hnf t = t++nf :: Te -> S Te+nf (Te'Abs a f) = do+ (x, t) <- unbind f+ nt <- nf t+ bt <- boxTe nt+ return $ Te'Abs a $ unbox $ bind x bt+nf (Te'App t u) = do+ nt <- nf t+ nu <- nf u+ case nt of+ Te'Abs _ f -> nf $ subst f u+ _ -> return $ Te'App nt nu+nf (Te'Lam f) = do+ (x, t) <- unbind f+ nt <- nf t+ bt <- boxTe nt+ return $ Te'Lam $ unbox $ bind x bt+nf (Te'Spe t a) = do+ nt <- nf t+ case nt of+ Te'Lam f -> nf $ subst f a+ _ -> return $ Te'Spe nt a+nf t = return t++eqTy :: Ty -> Ty -> S Bool+eqTy (Ty'Var x1) (Ty'Var x2) = return $ x1 == x2+eqTy (Ty'Arr a1 b1) (Ty'Arr a2 b2) = do+ ca <- eqTy a1 a2+ cb <- eqTy b1 b2+ return $ ca && cb+eqTy (Ty'All f1) (Ty'All f2) = eqBinder eqTy f1 f2+eqTy _ _ = return False++type Ctxt = M.Map (Var S Te) Ty++infer :: Ctxt -> Te -> S (Maybe Ty)+infer ctxt (Te'Var x) = return $ M.lookup x ctxt+infer ctxt (Te'Abs a f) = do+ (x, t) <- unbind f+ mtyt <- infer (M.insert x a ctxt) t+ return $ Ty'Arr a <$> mtyt+infer ctxt (Te'App t u) = do+ mtyt <- infer ctxt t+ case mtyt of+ Just (Ty'Arr a b) -> do+ mtyu <- infer ctxt u+ case mtyu of+ Just tyu -> do+ e <- eqTy tyu a+ return $ if e then Just b else Nothing+ Nothing -> return Nothing+ _ -> return Nothing+infer ctxt (Te'Lam f) = do+ (x, t) <- unbind f+ mtyt <- infer ctxt t+ case mtyt of+ Just tyt -> do+ bt <- boxTy tyt+ return $ Just $ Ty'All $ unbox $ bind x bt+ Nothing -> return Nothing+infer ctxt (Te'Spe t a) = do+ mtyt <- infer ctxt t+ case mtyt of+ Just (Ty'All f) -> return $ Just $ subst f a+ _ -> return Nothing++check :: Ctxt -> Te -> Ty -> S Bool+check ctxt t a = do+ mtyt <- infer ctxt t+ case mtyt of+ Just tyt -> eqTy tyt a+ Nothing -> return False++showTy :: Ty -> S Text+showTy (Ty'Var x) = return $ nameOf x+showTy (Ty'Arr a b) = do+ sha <- showTy a+ shb <- showTy b+ return $ "(" <> sha <> ") => (" <> shb <> ")"+showTy (Ty'All f) = do+ (x, t) <- unbind f+ sh <- showTy t+ return $ "\\" <> nameOf x <> "." <> sh++showTe :: Te -> S Text+showTe (Te'Var x) = return $ nameOf x+showTe (Te'Abs a f) = do+ sha <- showTy a+ (x, t) <- unbind f+ sht <- showTe t+ return $ "\\l " <> nameOf x <> ":" <> sha <> "." <> sht+showTe (Te'App t u) = do+ sht <- showTe t+ shu <- showTe u+ return $ "(" <> sht <> ") (" <> shu <> ")"+showTe (Te'Lam f) = do+ (x, t) <- unbind f+ sh <- showTe t+ return $ "\\L " <> nameOf x <> "." <> sh+showTe (Te'Spe t a) = do+ sht <- showTe t+ sha <- showTy a+ return $ "(" <> sht <> ") (" <> sha <> ")"++type1, type2 :: S Ty+term1 :: S Te+type1 = do+ x <- newVar "X"+ y <- newVar "Y"+ return $ unbox $ ty'Arr (ty'Var x) (ty'Var y)+type2 = do+ x <- newVar "X"+ y <- newVar "Y"+ let arr = ty'Arr (ty'Var x) (ty'Var y)+ return $ unbox $ ty'All x $ ty'All y $ ty'Arr arr arr+term1 = do+ x <- newVar "X"+ y <- newVar "Y"+ f <- newVar "f"+ a <- newVar "a"+ let arr = ty'Arr (ty'Var x) (ty'Var y)+ return $ unbox $ te'Lam x $ te'Lam y $ te'Abs arr f $ te'Abs (ty'Var x) a $+ te'App (te'Var f) (te'Var a)++spec :: Spec+spec = do+ describe "type1" $ do+ it "should be shown the intended text" $ do+ let r = "(X) => (Y)"+ flip shouldReturn r $ flip evalStateT 0 $ runS $ do+ t <- type1+ showTy t+ describe "type2" $ do+ it "should be shown the intended text" $ do+ let r = "\\X.\\Y.((X) => (Y)) => ((X) => (Y))"+ flip shouldReturn r $ flip evalStateT 0 $ runS $ do+ t <- type2+ showTy t+ describe "term1" $ do+ it "should be shown the intended text" $ do+ let r = "\\L X.\\L Y.\\l f:(X) => (Y).\\l a:X.(f) (a)"+ flip shouldReturn r $ flip evalStateT 0 $ runS $ do+ t <- term1+ showTe t
+ test/Spec.hs view
@@ -0,0 +1,1 @@+{-# OPTIONS_GHC -F -pgmF hspec-discover #-}