unbound-generics 0.3.1 → 0.3.2

raw patch · 11 files changed

+1836/−28 lines, 11 filesdep +ansi-wl-pprintdep +exceptionsdep +semigroupsdep ~criteriondep ~deepseqdep ~deepseq-genericsPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies added: ansi-wl-pprint, exceptions, semigroups, unix

Dependency ranges changed: criterion, deepseq, deepseq-generics

API changes (from Hackage documentation)

Files

• Changelog.md +13/−0
• README.md +4/−1
• benchmarks/BenchLam.hs +8/−1
• examples/CanonicalLF.lhs +535/−0
• examples/Nanevski.lhs +1149/−0
• examples/Prof.hs +42/−0
• src/Unbound/Generics/LocallyNameless/Alpha.hs +26/−12
• src/Unbound/Generics/LocallyNameless/Fresh.hs +13/−1
• src/Unbound/Generics/LocallyNameless/LFresh.hs +13/−1
• src/Unbound/Generics/PermM.hs +9/−3
• unbound-generics.cabal +24/−9

@@ -1,3 +1,16 @@+# NEXT++# 0.3.2++* Bump `deepseq >= 1.4.0.0` remove benchmark dependency on `deepseq-generics`+* Tested with GHC 8.4.1+* Tested with GHC 8.2.2+* Compile with `-Wcompat`+* Add `Semigroup` instances for all types that were previously `Monoid` instances+* Added more examples to the [examples/ directory](https://github.com/lambdageek/unbound-generics/tree/master/examples)+* Added "exceptions" dependency and `MonadThrow`, `MonadCatch`, `MonadMask` instances for `FreshMT` and `LFreshMT`.+  Thanks Alex McKenna.+ # 0.3.1  * Tested with GHC 8.0.1

@@ -14,8 +14,11 @@  This is a reimplementation of (parts of) [unbound](http://hackage.haskell.org/package/unbound) but using [GHC generics](http://www.haskell.org/ghc/docs/latest/html/libraries/base-4.7.0.1/GHC-Generics.html) instead of [RepLib](https://hackage.haskell.org/package/RepLib). -## Example+## Examples +Some examples are in the `examples/` directory in the source.  And also at [unbound-generics on GitHub Pages](https://lambdageek.github.io/unbound-generics)++### Example: Untyped lambda calculus interpreter Here is how you would implement call by value evaluation for the untyped lambda calculus:  ```haskell

@@ -1,5 +1,5 @@ -- | Untyped lambda calc for benchmarking-{-# LANGUAGE DeriveGeneric, DeriveDataTypeable #-}+{-# LANGUAGE DeriveGeneric, DeriveDataTypeable, CPP #-} module BenchLam where  import Control.Applicative@@ -10,7 +10,10 @@ import Data.Typeable (Typeable)  import Control.DeepSeq (NFData(..), deepseq)+#if MIN_VERSION_deepseq (1,4,0)+#else import Control.DeepSeq.Generics (genericRnf)+#endif import Criterion (Benchmark, env, bench, nf)  import Unbound.Generics.LocallyNameless@@ -24,7 +27,11 @@     deriving (Show, Generic, Typeable)  instance Alpha Term+#if MIN_VERSION_deepseq (1,4,0)+instance NFData Term+#else instance NFData Term where rnf = genericRnf+#endif   -- | lambda abstract over all the given vars

@@ -0,0 +1,535 @@+% Canonical LF using unbound-generics+% Aleksey Kliger+% June 2016++Canonical LF+============++This is a representation of [LF](http://www.twelf.org/) in which all terms are+automatically in *canonical form*.  The key idea is to segregate the type families+and the terms into *atomic* and *normal* forms where the term variables only stand+for atomic terms, and not arbitrary ones.  Then, a substitution procedure is defined+that takes terms in normal form and performs a substitution for a variable while+simultaneously normalizing any redices that occur.++> {-# LANGUAGE DeriveGeneric, StandaloneDeriving, DeriveDataTypeable,+>     ViewPatterns, RankNTypes, FlexibleContexts, FlexibleInstances,+>     FunctionalDependencies, TypeFamilies+>   #-}+> module CanonicalLF where+> import Unbound.Generics.LocallyNameless+> import GHC.Generics (Generic)+> import Data.Typeable (Typeable)+> import qualified Data.Map as M+> import Control.Monad.Reader+> import Control.Monad.Except+> import Data.Functor.Identity+> import Control.Applicative (Const(..))++Syntax+------++An LF signature introduces type family atoms and constant terms.++> data Signature = NilS+>   | SnocAtom (Rebind Signature (Atm, Embed Kind))+>   | SnocConst (Rebind Signature (Cnst, Embed Type))+>   deriving (Show, Generic, Typeable)++The type families are classified by kinds and may either be plain+types, or pi-kinds for families of types indexed by a term+variable.++> data Kind = TypeK | PiK (Bind (Var, Embed Type) Kind)+>   deriving (Show, Generic, Typeable)++The atomic type families are either type familiy atoms applied to zero+or more terms in normal form.++> type Atm = Name P+> data P = AtmP Atm | AppP P Term+>   deriving (Show, Generic, Typeable)++Type families in normal form are either atomic type families or dependent product+types indexed by a term variable of normal type.++> data Type = PT P | PiT (Bind (Var, Embed Type) Type)+>   deriving (Show, Generic, Typeable)++The atomic terms are either variables or constants applied to zero or+more terms in normal form.++> type Cnst = Name R+> type Var = Name R+> data R = VarR Var | ConstR Cnst | AppR R Term+>   deriving (Show, Generic, Typeable)++A term in normal form is either an atomic term or a lambda abstraction+that binds a term variable.++> data Term = RM R | LamM (Bind Var Term)+>   deriving (Show, Generic, Typeable)++When typechecking kinds, types or terms, new term variables may come+into scope. They are collected in contexts.++> data Context = NilC+>              | Snoc (Rebind Context (Var, Embed Type))+>              deriving (Show, Generic, Typeable)++All the syntactic objects are equivalent upto renaming of bound variables.++> instance Alpha Signature+> instance Alpha Kind+> instance Alpha P+> instance Alpha Type+> instance Alpha R+> instance Alpha Term+> instance Alpha Context++The metatheory of Canonical LF uses simple types to prove the+termination of hereditary substitution (defined below).  But they+aren't needed in the implementation.  (Although it would be+interesting to lift them to Haskell kinds and index the terms by the+simple types to disallow some malformed terms.)++> data SimpleType = AtmS Atm | ArrS SimpleType SimpleType+>   deriving (Show, Generic, Typeable)+>+> instance Alpha SimpleType++Hereditary Substitution+-----------------------++Variables in Canonical LF stand for atomic terms, but we will need to+subtitute terms for them.  If we used ordinary capture-avoiding+substitution, such substitution would produce redices, which we are+precisely what we don't want.  However redices will potentially only+occur when the variable for which we're substituting occurs at the+head of an atomic term.++> isHeadVarR :: Var -> R -> Bool+> isHeadVarR x (VarR y) = x == y+> isHeadVarR _ (ConstR _) = False+> isHeadVarR x (AppR r _) = isHeadVarR x r++Just using a boolean to decide if the variable is at the head of an+atomic term is fine, but we can actually partition an atomic term into+its head variable or constant together with a spine of applications.++> data Spine a = NilSp a | AppSp (Spine a) Term+> data Head = VarH Var | ConstH Cnst++If the variable for which we'll be substituting is at the head we only+really care about the spine.  Otherwise we have some other variable,+or perhaps a constant at the head.++> headSpine :: Var -> R -> Either (Spine Head) (Spine ())+> headSpine x (VarR y) | x == y    = Right (NilSp ())+>                      | otherwise = Left (NilSp (VarH y))+> headSpine _ (ConstR c)           = Left (NilSp (ConstH c))+> headSpine x (AppR r m)           = case headSpine x r of+>   Left s -> Left (AppSp s m)+>   Right s -> Right (AppSp s m)++Substitution in a kind just carries out substitution in the types.+Likewise substutition in normal type families.++> substKind :: Fresh m => Term -> Var -> Kind -> m Kind+> substKind _ _ TypeK = return TypeK+> substKind m x (PiK bnd) = do+>   ((y, unembed -> a), k) <- unbind bnd+>   a' <- substType m x a+>   k' <- substKind m x k+>   return $ PiK $ bind (y, embed a') k'+>+> substType :: Fresh m => Term -> Var -> Type -> m Type+> substType m x (PT p) = do+>   p' <- substP m x p+>   return (PT p')+> substType m x (PiT bnd) = do+>   ((y, unembed -> a), b) <- unbind bnd+>   a' <- substType m x a+>   b' <- substType m x b+>   return $ PiT $ bind (y, embed a') b'++Atomic type family application substitutes a term for a variable in the (normal) index terms.++> substP :: Fresh m => Term -> Var -> P -> m P+> substP _ _ (AtmP a) = return (AtmP a)+> substP m x (AppP p n) = do+>   p' <- substP m x p+>   n' <- substTerm m x n+>   return (AppP p' n')++Normal term substitution goes under a lambda (freshness is ensured by+the library) and into the atomic term.++> substTerm :: Fresh m => Term -> Var -> Term -> m Term+> substTerm m x (RM r) = substR m x r+> substTerm m x (LamM bnd) = do+>   (y, n) <- unbind bnd+>   n' <- substTerm m x n+>   return $ LamM $ bind y n'++To substitute in an atomic term we separate the head and the spine and+proceed according to whether the variable at the head is the one we+are substituting for.++> substR :: Fresh m => Term -> Var -> R -> m Term+> substR m x r =+>   case headSpine x r of+>     Left rsp -> RM <$> substRRsp m x rsp+>     Right msp -> substMsp m x msp++If there is another variable or a constant at the head, we will get+some kind of atomic term out since the head is unchanged and we only+substitute into the index terms.++> substRRsp :: Fresh m => Term -> Var -> Spine Head -> m R+> substRRsp _ _ (NilSp h) = return (headR h)+> substRRsp m x (AppSp sp n) = do+>   n' <- substTerm m x n+>   r <- substRRsp m x sp+>   return $ AppR r n'+>+> headR :: Head -> R+> headR (VarH y) = VarR y+> headR (ConstH c) = ConstR c++When the variable we care about is at the head, we apply the+substitution to the rest of the spine to get a normal term (which, by+the metatheory will turn out to be some kind of a lambda), apply the+substitution to the index, and then carry out a new substitution of+the new index for the variable bound by the lambda to the body of the+lambda.  This last step is the heredetary part of heredetary+substitution.  The metatheory guarantees that this process will+terminate.  (Because the simple type of the body of the lambda is+smaller than the simple type of the original term).++> substMsp :: Fresh m => Term -> Var -> Spine () -> m Term+> substMsp m _ (NilSp ()) = return m+> substMsp m x (AppSp s n) = do+>   o_ <- substMsp m x s+>   n' <- substTerm m x n+>   case o_ of+>     LamM bnd -> do+>       (y, o) <- unbind bnd+>       substTerm n' y o+>     _ -> error "can't happen"++Typechecking+============++We typecheck in an environment that maps type family atoms, term+costants and variables to their respective kinds and types.++> data Env = Env { _envAtm :: M.Map Atm Kind,+>                  _envConst :: M.Map Cnst Type,+>                  _envCtx :: M.Map Var Type }++> emptyEnv :: Env+> emptyEnv = Env M.empty M.empty M.empty++Some lenses to work with the environment++> envAtm :: Lens' Env (M.Map Atm Kind)+> envAtm afb s = fmap (\atms -> s { _envAtm = atms }) $ afb (_envAtm s)+>+> envCtx :: Lens' Env (M.Map Var Type)+> envCtx afb s = fmap (\ctx -> s { _envCtx = ctx } ) $ afb (_envCtx s)+>+> envConst :: Lens' Env (M.Map Cnst Type)+> envConst afb s = fmap (\sig -> s { _envConst = sig} ) $ afb (_envConst s)++And some combinators to perform lookups.++> lookupOver :: (MonadReader e m, MonadError String m) => Getting p e p -> String -> (p -> Maybe c) -> m c+> lookupOver l s f = do+>   mk <- views l f+>   case mk of+>     Nothing -> throwError $ "unbound " ++ s+>     Just c -> return c+>+> lookupAtom :: (MonadReader Env m, MonadError String m) => Atm -> m Kind+> lookupAtom = lookupOver envAtm "atom" . M.lookup +>+> lookupVar :: (MonadReader Env m, MonadError String m) => Var -> m Type+> lookupVar = lookupOver envCtx "variable" . M.lookup+>+> lookupConst :: (MonadReader Env m, MonadError String m) => Cnst -> m Type+> lookupConst = lookupOver envConst "constant" . M.lookup++To check a signature we check the kind or type classifying the atom or+constant and then continue in an environment extended with the new+binding.++> withSigOk :: (Fresh m, MonadReader Env m, MonadError String m) => Signature -> m r -> m r+> withSigOk NilS kont = kont+> withSigOk (SnocAtom (unrebind -> (s, (a, unembed -> k)))) kont =+>   withSigOk s $ do+>   local (set envCtx M.empty) $ wfk k+>   local (over envAtm (M.insert a k)) kont+> withSigOk (SnocConst (unrebind -> (s, (c, unembed -> a)))) kont =+>   withSigOk s $ do+>   local (set envCtx M.empty) $ wfType a+>   local (over envConst (M.insert c a)) kont++Kind and normal type formation is unsurprising.  Note that PT is only+well-formed when the atomic type family is fully applied and is of+base kind.++> wfk :: (Fresh m, MonadReader Env m, MonadError String m) => Kind -> m ()+> wfk TypeK = return ()+> wfk (PiK bnd) = do+>   ((x, unembed -> t), k) <- unbind bnd+>   wfType t+>   local (over envCtx (M.insert x t)) $ wfk k+>+> wfType :: (Fresh m, MonadReader Env m, MonadError String m) => Type -> m ()+> wfType (PT p) = do+>   k <- inferP p+>   case k of+>     TypeK -> return ()+>     _ -> throwError "expected a type"+> wfType (PiT bnd) = do+>   ((x, unembed -> a), b) <- unbind bnd+>   wfType a+>   local (over envCtx (M.insert x a)) $ wfType b++For atomic type families we infer their kinds.  For atoms we read the+kind off from the environment.  For applications we infer the kind of+the type family (which had better be a pi kind), and then check that+the term argument has the expected type and then return the resulting+kind where we (heredeterily) substitute the term for the index+variable.++> inferP :: (Fresh m, MonadReader Env m, MonadError String m) => P -> m Kind+> inferP (AtmP atm) = lookupAtom atm+> inferP (AppP p m) = do+>   k <- inferP p+>   case k of+>     TypeK -> throwError "expected a pi kind"+>     PiK bnd -> do+>       ((x, unembed -> a), k') <- unbind bnd+>       checkTerm m a+>       substKind m x k'++To check that a term in normal form has the expected normal type, we+check that its either a lambda of pi type, or an atomic term of atomic+type.  The latter ensures that terms are in eta long form by requiring+all variables and constants to be fully applied.++We infer the type of an atomic term (which had better be atomic) and+then check that it is alpha-equivalent to the given atomic type.+Because the calculus is constructed to only allow terms in normal+form, alpha equivalence suffices and we don't have to do any+normalization.  (We paid that price in heredetary substitution.)++> checkTerm :: (Fresh m, MonadReader Env m, MonadError String m) => Term -> Type -> m ()+> checkTerm (LamM bnd) (PiT bnd') = do+>   mmatch <- unbind2 bnd bnd'+>   case mmatch of+>     Just (x, m, (_, unembed -> a), b) -> do+>       wfType a+>       local (over envCtx (M.insert x a)) $ checkTerm m b+>     Nothing -> throwError "did not match"+> checkTerm (RM r) (PT p) = do+>   t <- inferTerm r+>   case t of+>     (PT p') | p `aeq` p' -> return ()+>     _ -> throwError "atomic term doesn't have the expected atomic type."+> checkTerm (LamM {}) _ = throwError "lambda with no-PI type"+> checkTerm (RM {}) _ = throwError "atomic term with non-atomic type"++To infer the type of a term, we lookup variables and constants in the+environment.  For applications we ensure that the head has some kind+of pi type and then check the index against the argument type, and+then return the result type with the argument substituted for the+index variable.++> inferTerm :: (Fresh m, MonadReader Env m, MonadError String m) => R -> m Type+> inferTerm (VarR x) = lookupVar x+> inferTerm (ConstR c) = lookupConst c+> inferTerm (AppR r m) = do+>   p_ <- inferTerm r+>   case p_ of+>     PiT bnd -> do+>       ((x, unembed -> a), b) <- unbind bnd+>       checkTerm m a+>       substType m x b+>     PT {} -> throwError "expected a function in application position"++Smart Constructors+==================++This section defines a little DSL for writing Canonical LF terms in+Haskell.  It's a higher-order encoding that uses haskell variable+binding to represent LF binding constructs.++We use a higher-kinded repr parameter to allow for different sorts of+interpretations for this DSL.  Although in this example we only build+one using the Syn newtype to wrap a fresh-name monad computation that+just builds a term in our original AST, above.++> class TermSyntax repr r n | r -> n, n -> r where+>   lam :: String -> ((repr r) -> (repr n)) -> (repr n)+>   app :: repr r -> repr n -> repr r+>   rm :: repr r -> repr n+>+> newtype Syn m a = Syn { unSyn :: m a } +>+> instance Fresh m => TermSyntax (Syn m) R Term where+>   lam hint f = Syn $ do+>     x <- fresh (s2n hint)+>     m <- unSyn $ f (Syn $ return $ VarR x)+>     return $ LamM (bind x m)+>   app r n = Syn (AppR <$> unSyn r <*> unSyn n)+>   rm r = Syn (RM <$> unSyn r)++> class  TypeSyntax repr p a | a -> p, p -> a where+>   type TermInType repr a :: *+>   type RInType repr a :: *+>   piT :: String -> repr a -> (repr (RInType repr a) -> repr a) -> repr a+>   arrT :: repr a -> repr a -> repr a+>   arrT a b = piT "_" a (const b)+>   appP :: repr p -> repr (TermInType repr a) -> repr p+>   pt :: repr p -> repr a++> instance Fresh m => TypeSyntax (Syn m) P Type where+>   type TermInType (Syn m) Type = Term+>   type RInType (Syn m) Type = R+>   piT hint sa f = Syn $ do+>     x <- fresh (s2n hint)+>     b <- unSyn $ f (Syn $ return $ VarR x)+>     a <- unSyn sa+>     return $ PiT $ bind (x, embed a) b+>   appP p m = Syn (AppP <$> unSyn p <*> unSyn m)+>   pt p = Syn (PT <$> unSyn p)++> class KindSyntax repr k where+>   type TypeInKind repr k :: *+>   type RInKind repr k :: *+>   typeK :: repr k+>   piK :: String -> repr (TypeInKind repr k) -> (repr (RInKind repr k) -> repr k) -> repr k+>   arrK :: repr (TypeInKind repr k) -> repr k -> repr k+>   arrK a k = piK "_" a (const k)++> instance Fresh m => KindSyntax (Syn m) Kind where+>   type TypeInKind (Syn m) Kind = Type+>   type RInKind (Syn m) Kind = R+>   typeK = Syn $ return TypeK+>   piK hint sa sk = Syn $ do+>     x <- fresh (s2n hint)+>     a <- unSyn sa+>     k <- unSyn $ sk (Syn $ return $ VarR x)+>     return $ PiK $ bind (x, embed a) k++> class SignatureSyntax repr sig p r | sig -> p r where+>   type KindInSig repr sig :: *+>   type TypeInSig repr sig :: *+>   letAtom :: String -> repr (KindInSig repr sig) -> (repr p -> repr sig) -> repr sig+>   letConstant :: String -> repr (TypeInSig repr sig) -> (repr r -> repr sig) -> repr sig+>   endSig :: repr sig+>+> instance Fresh m => SignatureSyntax (Syn m) (Signature -> Signature) P R where+>   type KindInSig (Syn m) (Signature -> Signature) = Kind+>   type TypeInSig (Syn m) (Signature -> Signature) = Type+>+>   letAtom hint sk kont = Syn $ do+>     a <- fresh (s2n hint)+>     k <- unSyn sk+>     f <- unSyn $ kont $ Syn $ return $ AtmP a+>     return $ \sig -> f (SnocAtom $ rebind sig (a, embed k))+>+>   letConstant hinst st kont = Syn $ do+>     c <- fresh (s2n hinst)+>     t <- unSyn st+>     f <- unSyn $ kont $ Syn $ return $ ConstR c+>     return $ \sig -> f (SnocConst $ rebind sig (c, embed t))+>+>   endSig = Syn $ return id++> infixr 6 `arrT`, `arrK`+> infixl 6 `appP`, `app`++Example+-------++An LF signature fragment for first-order logic.++> example1 :: Fresh m => Syn m (Signature -> Signature)+> example1 =+>   letAtom "o" typeK $ \o ->+>   letConstant "tt" (pt o) $ \tt ->+>   letConstant "ff" (pt o) $ \ff ->+>   letConstant "not" (pt o `arrT` pt o) $ \not ->+>   letConstant "and" (pt o `arrT` pt o `arrT` pt o) $ \and ->+>   letAtom "nd" (pt o `arrK` typeK) $ \nd ->+>   letConstant "tti" (pt (nd `appP` rm tt)) $ \tti ->+>   letConstant "ffe" (piT "a" (pt o) $ \a ->+>                        pt (nd `appP` rm ff)+>                        `arrT`+>                        pt (nd `appP` rm a)) $ \ffe ->+>   letConstant "noti" (piT "a" (pt o) $ \a ->+>                          (piT "p" (pt o) $ \p ->+>                              pt (nd `appP` rm a)+>                              `arrT`+>                              pt (nd `appP` rm p))+>                          `arrT`+>                          pt (nd `appP` rm (not `app` rm a))) $ \noti ->+>   letConstant "note" (piT "a" (pt o) $ \a -> piT "c" (pt o) $ \c ->+>                          pt (nd `appP` rm (not `app` rm a))+>                          `arrT`+>                          pt (nd `appP` rm a)+>                          `arrT`+>                          pt (nd `appP` rm c)) $ \note ->+>   letConstant "andi" (piT "a" (pt o) $ \a -> piT "b" (pt o) $ \b ->+>                          pt (nd `appP` rm a)+>                          `arrT`+>                          pt (nd `appP` rm b)+>                          `arrT`+>                          pt (nd `appP` rm (and `app` rm a `app` rm b))) $ \andi ->+>   letConstant "ande1" (piT "a" (pt o) $ \a -> piT "b" (pt o) $ \b ->+>                           pt (nd `appP` rm (and `app` rm a `app` rm b))+>                           `arrT`+>                           pt (nd `appP` rm a)) $ \ande1 ->+>   letConstant "ande2" (piT "a" (pt o) $ \a -> piT "b" (pt o) $ \b ->+>                           pt (nd `appP` rm (and `app` rm a `app` rm b))+>                           `arrT`+>                           pt (nd `appP` rm b)) $ \ande2 ->+>   endSig++> checkSynSig :: (Fresh m, MonadReader Env m, MonadError String m) => Syn m (Signature -> Signature) -> m ()+> checkSynSig sig = do+>   sigf <- unSyn sig+>   withSigOk (sigf NilS) $ return ()++Example:+```haskell+  >>> runExceptT $ runFreshMT $ runReaderT (checkSynSig example1) emptyEnv+  Right ()+```++Appendix: Lens utilities+==============++Some machinery to work with records.++> type Lens s t a b = forall f . Functor f => (a -> f b) -> s -> f t+> type Lens' s a = Lens s s a a++> type Setting s t a b = (a -> Identity b) -> s -> Identity t+> type Setting' s a = Setting s s a a++> over :: Setting s t a b -> (a -> b) -> s -> t+> over l f = runIdentity . l (Identity . f)++> set :: Setting s t a b -> b -> s -> t+> set l = over l . const++> type Getting r s a = (a -> Const r a) -> s -> Const r s++> views :: MonadReader s m => Getting a s a -> (a -> r) -> m r+> views l f = asks (\s -> f (getConst (l Const s)))+

@@ -0,0 +1,1149 @@+% "Meta-programming with names and necessity" using unbound-generics+% Aleksey Kliger+% August 2016+++Introduction+============++This example is based on Nanevski's “Meta-programming with Names and+Necessity”[1](http://reports-archive.adm.cs.cmu.edu/anon/2002/CMU-CS-02-123R.pdf).+In particular, it demonstrates how to represent a language with+multiple sorts of names (value variables, code variables, nominals and+support variables) some with non-standard notions of substitution.++As a tutorial example, we show how to represent the language and+demonstrate its operational semantics.  Additionally, this document+includes a typecheker and pretty printer.++This file is Literate Haskell, so we start with some boilerplate.++Every `unbound-generics` syntax representation needs `deriving (Show, Generic, Typeable)` declarations for all the datatypes.++> {-# language DeriveDataTypeable, DeriveGeneric #-}++> {-# language MultiParamTypeClasses,+>     FlexibleContexts, FlexibleInstances, DefaultSignatures, ViewPatterns, RankNTypes,+>     GeneralizedNewtypeDeriving #-}+> module Nanevski where+> import GHC.Generics (Generic)+> import Data.Typeable (Typeable)+> import Unbound.Generics.LocallyNameless+> import Unbound.Generics.LocallyNameless.Internal.Fold (Fold, foldMapOf)+> import qualified Unbound.Generics.PermM as PermM+>+> import Control.Monad.Except+> import Control.Monad.State+> import Control.Monad.Writer+> import Control.Monad.Reader+> import Data.List (partition, nub, sort, (\\), isSubsequenceOf)+> import Data.Monoid (Any (..))+> import Data.Either (partitionEithers)+> import qualified System.IO as IO+> import qualified Text.PrettyPrint.ANSI.Leijen as PP+> import Text.PrettyPrint.ANSI.Leijen ()++Introduction to meta-programming+--------------------------------++Meta-programming is the process of writing programs that create,+manipulate or reason about other programs.  The meta-program is+written in the *meta-language* and it manipulates *object-language*+programs.++In the system in this document, the object language and the+meta-language coincide.  In general they could be different (for+example the meta-language could be compiled down to machine code,+while the object-language remains as some sort of abstract syntax+trees).++The type discipline of the system in this document applies both to the+meta- and object-languages: a well-typed meta-program can only+construct well-typed object-language programs.++One important concept is the *support* of an object-language+expression: it is the set of meta-language names that appear within+the object-language program fragment.  The meta-language program may+compose larger object-language fragments by substituting+object-language expressions for the names.++Example+-------++Suppose we wanted to construct the object-language cube function `“λx:int. 1 * x * x * x”`++The following program constructs such a function:++> -- >>> ppretty (pexp @@ number 3)+> -- (λn:int.+> --  choose+> --  (νX∼int.+> --   let □w = (Λp.+> --             λe:□_{p} int.+> --             rec+> --               go (m:int) : □_{p} int+> --               is if (□_{p} int;+> --                      m ≤ 0;+> --                      λ_:(). “1”;+> --                      λ_:(). let □u = go (m + -1) in let □w = e in “⟨⟩u * ⟨⟩w”)+> --                  ()) {X}+> --            “X”+> --            n in “λx:int. ⟨X ↦ x⟩w”))+> -- 3+++Syntax+======++Types+-----+++> data BaseType = UnitT | BoolT | IntT+>   deriving (Typeable, Generic, Show)++> data Support = Support { supportNominals :: ![Nominal],+>                          supportVars :: ![SupportVar] }+>   deriving (Typeable, Generic, Show)+> type SupportVar = Name Support++> data Type =+>   BaseT BaseType          -- some base types+>   | ArrT Type Type        -- τ₁→τ₂ functions+>   | BoxT Type Support   -- □_C τ is the type of code of type τ with support C+>   | NomArrT Type Type      -- τ₁ ↛ τ₂ is the type of νN:τ₁.e brings a+>                           -- new name N associated with type τ₁ into+>                           -- scope in a body of type τ₂.  The new+>                           -- name cannot appear in the type τ₂ or in+>                           -- the support of e.  It is thus+>                           -- guaranteed to either be substituted+>                           -- away or only appear in code in e, not+>                           -- in subexpresisons that may be evaluated+>                           -- in teh course of evaluating e.+>   | ForallSupT (Bind SupportVar Type) -- support-polymorphic functions+>   deriving (Typeable, Generic, Show)++Meta-language expressions+-------------------------++> data Expr =+>   V Var+>   | U NominalSubst CodeVar+>   | N Nominal+>   | C BaseConst+>   | P PrimOp [Value] [Expr] -- partially evaluated primop p v₁...vₙ e₁...eₘ+>   | Lambda (Bind (Var, Embed Type) Expr)+>   | RecFun (Bind (Var, Var, Embed Type, Embed Type) Expr) -- fun f (x : τ₁) : τ₂ = e+>   | App Expr Expr+>   | Let Expr (Bind Var Expr)+>   | Box Code  -- A box expression represents some syntactic code as a data structure.+>   | LetBox Expr (Bind CodeVar Expr)+>   | New (Bind (Nominal, Embed Type) Expr)   -- the New operation brings names into scope; it is the job of the type system to ensure that the new name does not appear in the type of the body, nor its support.+>   | Choose Expr+>   | PLamSupport (Bind SupportVar Expr)+>   | PAppSupport Expr Support+>   deriving (Typeable, Generic, Show)+>+> data BaseConst = UnitC | BoolC !Bool | IntC !Int+>   deriving (Typeable, Generic, Show)+> data PrimOp = IfPrim Type | AddPrim | MulPrim | LeqPrim+>   deriving (Typeable, Generic, Show)++>+> type Var = Name Expr++Ordinary variables just stand for expressions.++> type Value = Expr+++> isValue :: Expr -> Bool+> isValue (C _) = True+> isValue (Lambda _) = True+> isValue (Box _) = True+> isValue (New _) = True+> isValue (PLamSupport _) = True+> isValue _ = False++Object-level Code+-----------------++Think of Code as some data structure that the expressions can build+up.  Code is a first-class value in this language.  You can build it+up, pass it to functions, return it as a result etc.  Code that is+open has non-empty support is guaranteed by the type system not to be+evaluated.  Code that is closed and has empty support , on the other+hand may appear in expressions in positions where it may potentially+be run.++> newtype Code = Code { codeExpr :: Expr }+>   deriving (Typeable, Generic, Show)+> type CodeVar = Name Code++Code variables stand for code, but they only occur in expressions+together with an explicit subtitution that substitutes away some Nominals.++> newtype NominalSubst = NominalSubst { nominalSubst :: [(Nominal, Nom)] }+>   deriving (Typeable, Generic, Show)++Nominals+--------++A Nominal can appear in code (but not in an expression that may be+evaluated).  It stands for an expression just like Var, but in+unbound-generics since we want to treat Nominal and Var distinctly, we+add a newtype wrapper around Expr and call it a Nom.++> newtype Nom = Nom {nomExpr :: Expr }+>   deriving (Typeable, Generic, Show)+> type Nominal = Name Nom++Alpha renaming, free names, alpha-equivalence boilerplate+---------------------------------------------------------++All the types we defined will participate in various Alpha operations:+we can collect the free Variabes, Nominals or CodeVars of all the+syntactic categories.  They are also subject to alpha equivalence upto+renaming of bound occurrances, etc.++> instance Alpha Nom+> instance Alpha Code+> instance Alpha Support+> instance Alpha NominalSubst+> instance Alpha Type+> instance Alpha Expr+> instance Alpha BaseType+> instance Alpha BaseConst+> instance Alpha PrimOp++Substitution+============++We also have notions of substitution for variables, nominals and code variables.++For base types, constants and primitive operations, we give some+catch-all substitution operations since they cannot contain any sort+of name.++> instance Subst a BaseType where+>   subst _ _ = id+>   substs _ = id+>+> instance Subst a BaseConst where+>   subst _ _ = id+>   substs _ = id+>+> instance Subst Expr PrimOp where+>   subst _ _ = id+>   substs _ = id+> instance Subst Code PrimOp where+>   subst _ _ = id+>   substs _ = id+> instance Subst Nom PrimOp+> instance Subst Support PrimOp++Expression substitution+-----------------------++Ordinary variables can occur in expressions as well as code, noms and+nominal substitutions.  They don't occur in types, so we can+short-circuit substitution there and return the type unchanged.++> instance Subst Expr Type where+>   subst _ _ = id+>   substs _ = id+> instance Subst Expr Expr where+>   isvar (V v) = Just (SubstName v)+>   isvar _ = Nothing+> instance Subst Expr NominalSubst+> instance Subst Expr Nom+> instance Subst Expr Support where+>   subst _ _ = id+>   substs _ = id++Nominal substitution+--------------------++> instance Subst Nom Nom+> instance Subst Nom Support++To substitute for a nominal N in an expression e, we use need to use+\texttt{isCoerceVar} to pull out the expression from the Nom being+substituted.++> instance Subst Nom Expr where+>   isCoerceVar (N n) = Just $ SubstCoerce n (Just . nomExpr)+>   isCoerceVar _ = Nothing++An important property (justified by the type system) of this language+is that when substituting for a name N or ordinary variable v in an+expression Box (Code e) we can just return Box (Code e) unchanged+since the type system prevents Code from depending on the ordinary+variable context or by using names that do not contribute to the+support of a term.++> instance Subst Nom Code where+>   subst _ _ = id+>   substs _ = id+> instance Subst Expr Code where+>   subst _ _ = id+>   substs _ = id++> instance Subst Nom Type+> instance Subst Nom NominalSubst++Code substitution+-----------------++> instance Subst Code Code++We can substitute for code variables u in expressions, but since+u's appear only together with an explicit substitution for its+Nominals, we use \texttt{isCoerceVar} to have unbound-generics perform+the nominal substitution.++> instance Subst Code Expr where+>   isCoerceVar (U noms u) = Just $ SubstCoerce u (Just . substituteSupported noms)+>   isCoerceVar _ = Nothing+>++Note that in this case we peek inside a \texttt{(Code e)} using+codeExpr. (Just using \texttt{substs (nominalSubst noms) c} would give+us back the same unchanged syntactic object!)++> substituteSupported :: NominalSubst -> Code -> Expr+> substituteSupported noms c = substs (nominalSubst noms) (codeExpr c)++> instance Subst Code NominalSubst+> instance Subst Code Nom++> instance Subst Code Type where+>   subst _ _ = id+>   substs _ = id++> instance Subst Code Support where+>   subst _ _ = id+>   substs _ = id++Support polymorphism substitution+---------------------------------++Support variables stand for support sets.  We have to do a bit of+juggling to normalize the result of the substitution.++> instance Subst Support Support where+>   subst v sup sup0@(Support noms vs) =+>     case Data.List.partition (== v) vs of+>       ((_:_), vs') -> let+>         noms' = sort (supportNominals sup ++ noms)+>         vs'' = sort (supportVars sup ++ vs')+>         in Support noms' vs''+>       _ -> sup0+>   substs ss (Support noms vs) =+>     let f v = case lookup v ss of+>           Just sup -> Left sup+>           Nothing -> Right v+>         (sups, vs') = partitionEithers (map f vs)+>         noms' = sort (concatMap supportNominals sups ++ noms)+>         vs'' = sort (concatMap supportVars sups ++ vs')+>         in Support noms' vs''++> instance Subst Support Type++> instance Subst Support Expr+> instance Subst Support Nom+> instance Subst Support NominalSubst++As with Nominals, since SupportVars stand for the support of an+expression, and boxed code is meant to have empty support until it is+unboxed and evaluated, the support variable substitution on code is+the identity.++> instance Subst Support Code where+>   subst _ _ = id+>   substs _ = id++Operational Semantics+=====================++The operational semantics take configurations consisting of a context+of Nominals together with their associated types and an expression+with empty support to another such configuration.++> data NomCtx = NilNC | SnocNC (Rebind NomCtx (Nominal, Embed Type))+>             | SnocSupNC (NomCtx, SupportVar)+>   deriving (Typeable, Generic, Show)+> instance Alpha NomCtx++A configuration just pairs together a nominal ctx and an expression in some manner.+We will use a state monad. But we could also bind the names of the context in the expression.++> type ClosedConfig = Bind NomCtx Expr++We will need to work in a monad that also gives us fresh names and a way to signal errors++> step :: (MonadError String m, MonadState NomCtx m, Fresh m) => Expr -> m Expr+> step e0 = case e0 of+>   V v -> evalError ("unbound variable: "  ++ show v)+>   U _ u -> evalError ("unbound code variable: " ++ show u)+>   N n -> evalError ("unbound name: " ++ show n)+>   C c -> evalError ("already a value: " ++ show c)+>   P p vs [] -> applyPrim p vs+>   P p vs (e:es) | isValue e -> pure (P p (vs ++ [e]) es) +>                 | otherwise -> P p vs <$> ((:) <$> step e <*> pure es)+>   Lambda _ -> evalError ("already a value: " ++ show e0)+>   efun@(RecFun bnd) -> do+>     ((f, x, t1, _), e) <- unbind bnd+>     return $ Lambda $ bind (x, t1) (subst f efun e)+>   Let e1 bnd | isValue e1 -> do+>                  (x, e2) <- unbind bnd+>                  return $ subst x e1 e2+>   Let e1 bnd -> Let <$> step e1 <*> pure bnd+>   Box _ -> evalError ("already a value: " ++ show e0)+>   App e1@(Lambda bnd) e2 | isValue e2 -> do+>                              ((x, _), ebody) <- unbind bnd+>                              return $ subst x e2 ebody+>                          | otherwise -> do+>                              App e1 <$> step e2+>   App e1 e2 -> App <$> step e1 <*> pure e2+>   LetBox (Box c) bnd -> do+>     (u, ebody) <- unbind bnd+>     return $ subst u c ebody+>   LetBox e1 bnd -> LetBox <$> step e1 <*> pure bnd+>   New _ -> evalError ("already a value: " ++ show e0)+>   Choose (New bnd) -> do+>     -- In the paper there's a side-condition here that the chosen+>     -- name has to be fresh (with respect to the nominal ctx.+>     -- Fortunately unbound-generics will always give us a fresh+>     -- name.+>     (nt, ebody) <- unbind bnd+>     modify (\ctx -> SnocNC $ rebind ctx nt)+>     return ebody+>   Choose e -> Choose <$> step e+>   PLamSupport _ -> evalError ("already a value: " ++ show e0)+>   PAppSupport (PLamSupport bnd) sup -> do+>     (sv, ebody) <- unbind bnd+>     return $ subst sv sup ebody+>   PAppSupport e1 sup -> PAppSupport <$> step e1 <*> pure sup++> evalError :: MonadError String m => String -> m a+> evalError = throwError++> applyPrim :: MonadError String m => PrimOp -> [Value] -> m Value+> applyPrim (IfPrim _t) [C (BoolC b), v1, v2] = return $ if b then v1 else v2+> applyPrim AddPrim [C (IntC x), C (IntC y)] = return $ C $ IntC $ x + y+> applyPrim MulPrim [C (IntC x), C (IntC y)] = return $ C $ IntC $ x * y+> applyPrim LeqPrim [C (IntC x), C (IntC y)] = return $ C $ BoolC $ x <= y+> applyPrim p vs = evalError (show p ++ show vs ++ " does not step")++> eval :: (Fresh m, MonadState NomCtx m, MonadError String m) => Expr -> m Expr+> eval e = if isValue e then return e else step e >>= eval+  +Evaluation Example+==================++A little DSL for term construction+----------------------------------++> lam :: String -> Type -> (Expr -> Expr) -> Expr+> lam s t f =+>   let x = s2n s+>   in Lambda $ bind (x, embed t) (f $ V x)++> recFun :: String -> String -> Type -> Type -> (Expr -> Expr -> Expr) -> Expr+> recFun sfn sx t1 t2 f =+>   let fn = s2n sfn+>       x = s2n sx+>   in RecFun $ bind (fn, x, embed t1, embed t2) (f (V fn) (V x))++> plam :: String -> (SupportVar -> Expr) -> Expr+> plam s f =+>   let sv = s2n s+>   in PLamSupport (bind sv (f sv))++> intT, unitT, boolT :: Type+> intT = BaseT IntT+> unitT = BaseT UnitT+> boolT = BaseT BoolT+> boxT :: Type -> [Nominal] -> [SupportVar] -> Type+> boxT t noms svs = BoxT t (Support noms svs)+> boxT_ :: Type -> [Nominal] -> Type+> boxT_ t noms = boxT t noms []+> arrT :: Type -> Type -> Type+> arrT = ArrT+> infixr 5 `arrT`+> forallSupT :: String -> (SupportVar -> Type) -> Type+> forallSupT s f =+>   let sv = s2n s+>   in ForallSupT (bind sv (f sv))++> (@@) :: Expr -> Expr -> Expr+> (@@) = App+> infixl 5 @@++> papp :: Expr -> [Nominal] -> [SupportVar] -> Expr+> papp e noms svs = PAppSupport e (Support noms svs)++> chooseNew :: String -> Type -> (Nominal -> Expr) -> Expr+> chooseNew s t f =+>   let n = s2n s+>   in Choose $ New $ bind (n, embed t) (f n)++> letExp :: String -> Expr -> (Expr -> Expr) -> Expr+> letExp s e1 f =+>   let x = s2n s+>   in Let e1 (bind x (f $ V x))++> letBox :: String -> Expr -> (CodeVar -> Expr) -> Expr+> letBox s e1 f =+>   let u = s2n s+>   in LetBox e1 (bind u (f u))++> box :: Expr -> Expr+> box = Box . Code++> code :: [(Nominal, Expr)] -> CodeVar -> Expr+> code nome = U (NominalSubst $ map (fmap Nom) nome)++> runCode :: CodeVar -> Expr+> runCode = U (NominalSubst []) ++> name :: Nominal -> Expr+> name = N++> number :: Int -> Expr+> number = C . IntC ++> ifLeqZ :: Type -> Expr -> Expr -> Expr -> Expr+> ifLeqZ tres ex etrue efalse =+>   App (P (IfPrim tres) [] [etest, thunk etrue, thunk efalse]) (C UnitC)+>   where+>     etest = P LeqPrim [] [ex, number 0]+>     thunk e = lam "_" unitT (\_ -> e)++> sub1 :: Expr -> Expr+> sub1 e = P AddPrim [] [e, number (-1)]++> add, mul :: Expr -> Expr -> Expr+> add e1 e2 = P AddPrim [] [e1, e2]+> mul e1 e2 = P MulPrim [] [e1, e2]++> infixl 6 `add`+> infixl 7 `mul`++> (~~) :: a -> b -> (a, b)+> (~~) = (,)+> infix 5 ~~++Example: Staged exponential function+------------------------------------++(Note that within the calculus itself there's not a way to abstract over a nominal like this - the example below chooses a new X which appears in the definition of this helper function.)++First a little recursive helper function that expands out to the m-fold multiplication code \texttt{X * X * X * ... * 1}++> exp' :: Nominal -> Expr+> exp' nX = recFun "exp'" "m" intT (boxT_ intT [nX]) $ \exp' m ->+>   ifLeqZ (boxT_ intT [nX]) m (box $ number 1) (letBox "u" (exp' @@ (sub1 m)) $ \u ->+>                                      box $ mul (name nX) (runCode u))+>   ++And the example exponential function takes an integer n and then constructs a piece of code consiting of a lambda abstraction whose argument x is multiplied with itself n times.++> expon :: Expr+> expon = lam "n" intT $ \n ->+>   chooseNew "X" intT $ \nX ->+>   letExp "exp'" (exp' nX) $ \exp' ->+>   letBox "v"  (exp' @@ n) $ \v ->+>   box (lam "x" intT $ \x -> code [nX ~~ x] v)++Let's set up an environment for running evaluations.++> run :: StateT NomCtx (ExceptT String FreshM) a -> Either String (a, NomCtx)+> run comp = runFreshM (runExceptT (runStateT comp NilNC))++Running the example \texttt{expon 3} we get the expected final+configuration of \texttt{box (λx : int . x * x * x * 1)} and the used+name X1 (which doesn't appear in the code, and therefore we could run+the code).++> -- >>> run (eval (expon @@ number 3))+> -- Right (Box (Code {codeExpr = Lambda (<(x,{BaseT IntT})> P MulPrim [] [V 0@0,P MulPrim [] [V 0@0,P MulPrim [] [V 0@0,C (IntC 1)]]])}),SnocNC (<<NilNC>> (X1,{BaseT IntT})))++> -- >>> run (eval (letBox "exp3" (expon @@ number 3) $ \exp3 -> (runCode exp3) @@ number 2))+> -- Right (C (IntC 8),SnocNC (<<NilNC>> (X1,{BaseT IntT})))+++Example: Staged support-polymorphic exponential kernel+------------------------------------------------------++> pexpKernel :: Expr+> pexpKernel = plam "p" $ \sp ->+>   let tResult = boxT intT [] [sp]+>   in lam "e" tResult $ \e ->+>     recFun "go" "m" intT tResult $ \go m ->+>     ifLeqZ tResult m (box $ number 1) (letBox "u" (go @@ (sub1 m)) $ \u ->+>                                           letBox "w" e $ \w ->+>                                           box $ mul (runCode u) (runCode w))++> -- >>> run $ eval (papp pexpKernel [] [] @@ box (number 42) @@ number 3)+> -- Right (Box (Code {codeExpr = P MulPrim [] [P MulPrim [] [P MulPrim [] [C (IntC 1),C (IntC 42)],C (IntC 42)],C (IntC 42)]}),NilNC)++> pexp :: Expr+> pexp = lam "n" intT $ \n ->+>   chooseNew "X" intT $ \nX ->+>   letBox "w" (papp pexpKernel [nX] [] @@ box (name nX) @@ n) $ \w ->+>   box (lam "x" intT $ \x -> code [nX ~~ x] w)++> -- >>> run $ eval (pexp @@ number 5)+> -- Right (Box (Code {codeExpr = Lambda (<(x,{BaseT IntT})> P MulPrim [] [P MulPrim [] [P MulPrim [] [P MulPrim [] [P MulPrim [] [C (IntC 1),V 0@0],V 0@0],V 0@0],V 0@0],V 0@0])}),SnocNC (<<NilNC>> (X1,{BaseT IntT})))++> -- >>> run $ eval (letBox "c" (pexp @@ number 5) $ \c -> runCode c @@ number 2)+> -- Right (C (IntC 32),SnocNC (<<NilNC>> (X1,{BaseT IntT})))+++Appendix: Type checking and support inference+=============================================++> class Fresh m => TC m where+>  lookupSupportVar :: SupportVar -> m () -- just check it exists+>  lookupVar :: Var -> m Type+>  lookupCodeVar :: CodeVar -> m (Type, Support)+>  lookupNom :: Nominal -> m Type+>  extendVar :: Var -> Type -> m a -> m a+>  extendCodeVar :: CodeVar -> Type -> Support -> m a -> m a+>  extendNom :: Nominal -> Type -> m a -> m a+>  extendSupportVar :: SupportVar -> m a -> m a+>+>  tcError :: String -> m a+>  default tcError :: (MonadError String m) => String -> m a+>  tcError = throwError+>+>  inSupport :: Nominal -> m ()+>  inSupport n = includeSupport (Support [n] [])+>  includeSupport :: Support -> m ()+>  default includeSupport :: (MonadWriter Support m) => Support -> m ()+>  includeSupport = tell+>+>  -- run the subcomputation, grab its support and then completely censor it+>  withEmptySupport :: m a -> m (a, Support)+>  default withEmptySupport :: (MonadWriter Support m) => m a -> m (a, Support)+>  withEmptySupport comp =+>    let censorEverything = const mempty+>    in pass ((\asup -> (asup, censorEverything)) <$> listen comp)+>    ++> wellFormed :: TC m => Type -> m ()+> wellFormed t0 =+>   case t0 of+>     BaseT {} -> return ()+>     (ArrT t1 t2) -> wellFormed t1 >> wellFormed t2+>     (NomArrT t1 t2) -> wellFormed t1 >> wellFormed t2+>     (BoxT t sup) -> wellFormed t >> wellFormedSupport sup+>     (ForallSupT bnd) -> do+>       (sv, t) <- unbind bnd+>       extendSupportVar sv $ wellFormed t+>     _ -> tcError ("Unimplemented! " ++ show t0)++> wellFormedSupport :: TC m => Support -> m ()+> wellFormedSupport (Support _noms svs) = mapM_ lookupSupportVar svs++> newtype Expected a = Expecting { unExpecting :: a }++> inferExpr :: TC m => Expr -> m Type+> inferExpr e = inferExpr_ e (Expecting Nothing)++> expecting :: TC m => Expected (Maybe Type) -> Type -> m Type+> expecting (Expecting Nothing) t = return t+> expecting (Expecting (Just texp)) t = do+>   unless (t `aeq` texp) $ tcError $ "expected type " ++ show texp ++ " but got " ++ show t+>   return texp++> expectingSup :: TC m => Expected (Maybe Support) -> Support -> m Support+> expectingSup (Expecting Nothing) sup = return sup+> expectingSup (Expecting (Just supexp)) sup = do+>   unless (sup `subsup` supexp) $ tcError $ "expected support " ++ show supexp ++ " but got " ++ show sup+>   return supexp++> subsup :: Support -> Support -> Bool+> subsup (Support noms svs) (Support noms' svs') =+>   let nomsLeq = noms `isSubsequenceOf` noms'+>       svsLeq = svs `isSubsequenceOf` svs'+>   in nomsLeq && svsLeq++> checkExpr :: TC m => Expr -> Type -> m ()+> checkExpr e t = inferExpr_ e (Expecting (Just t)) >> return ()+> ++> inferExpr_ :: (TC m) => Expr -> Expected (Maybe Type) -> m Type+> inferExpr_ e0 xpt =+>   case e0 of+>     V x -> lookupVar x >>= expecting xpt+>     U noms u -> do+>       (t, supIn) <- lookupCodeVar u+>       checkSubst noms supIn+>       expecting xpt t+>     N nX -> do+>       t <- lookupNom nX+>       inSupport nX+>       expecting xpt t+>     C bc -> expecting xpt $ BaseT $ inferConst bc+>     P primOp vs es -> do+>       checkPrimitive primOp (vs ++ es) >>= expecting xpt+>     Lambda bnd -> do+>       ((x, unembed -> tDom), e) <- unbind bnd+>       wellFormed tDom+>       xptCod <- unExpectArrType xpt tDom+>       tCod <- extendVar x tDom $ inferExpr_ e xptCod+>       return (tDom `ArrT` tCod)+>     App e1 e2 -> do+>       tf <- inferExpr e1+>       (tDom, tCod) <- matchArrType tf+>       checkExpr e2 tDom+>       expecting xpt tCod+>     RecFun bnd -> do+>       ((f, x, unembed -> tDom, unembed -> tCod), e) <- unbind bnd+>       let funT = tDom `ArrT` tCod+>       extendVar f funT $ extendVar x tDom $ checkExpr e tCod+>       expecting xpt funT+>     Let e1 bnd -> do+>       t <- inferExpr e1+>       (x, e2) <- unbind bnd+>       extendVar x t $ inferExpr_ e2 xpt+>     Box c -> do+>       (xpt, xpsup) <- unExpectBoxType xpt+>       inferCode c xpt xpsup+>     LetBox e1 bnd -> do+>       tbox <- inferExpr e1+>       (t, sup) <- matchBoxType tbox+>       (u, e2) <- unbind bnd+>       extendCodeVar u t sup $ inferExpr_ e2 xpt+>     New bnd -> do+>       ((nX, unembed -> tDom), e) <- unbind bnd+>       wellFormed tDom+>       xptCod <- unExpectNomArrType xpt tDom+>       (tCod, supOut) <- withEmptySupport $ extendNom nX tDom $ inferExpr_ e xptCod+>       let inType = anyOf fv (== nX) tCod+>           inSup = anyOf fv (== nX) (supportNominals supOut)+>       when inType $ tcError ("Name " ++ show nX ++ " appears in the result type of a ν-expression " ++ show tCod)+>       when inSup $ tcError ("Name " ++ show nX ++ " appears in the support of ν-expression " ++ show supOut)+>       includeSupport supOut+>       return (tDom `NomArrT` tCod)+>     Choose e -> do+>       tarr <- inferExpr e+>       (_, tCod) <- matchNomArrType tarr+>       expecting xpt tCod+>     PLamSupport bnd -> do+>       (sv, e) <- unbind bnd+>       xptout <- unExpectForallSupType xpt sv +>       (t, supOut) <- withEmptySupport $ extendSupportVar sv $ inferExpr_ e xptout+>       let inSup = anyOf fv (== sv) (supportVars supOut)+>       when inSup $ tcError ("support variable " ++ show sv ++ " appears in the support of the body of the support-polymorphic function")+>       includeSupport supOut+>       expecting xpt $ ForallSupT (bind sv t)+>     PAppSupport e sup -> do+>       tall <- inferExpr e+>       wellFormedSupport sup+>       (sv, t) <- matchForallSup tall+>       expecting xpt $ subst sv sup t++> inferCode :: TC m => Code -> Expected (Maybe Type) -> Expected (Maybe Support) -> m Type+> inferCode (Code e) xpt xpsup = do+>   (t, supOut) <- withEmptySupport (inferExpr_ e xpt)+>   BoxT t <$> expectingSup xpsup supOut++> matchArrType :: TC m => Type -> m (Type, Type)+> matchArrType (ArrT tdom tcod) = return (tdom, tcod)+> matchArrType t0 = tcError ("Expected an expression of function type, got " ++ show t0)++> matchNomArrType :: TC m => Type -> m (Type, Type)+> matchNomArrType (NomArrT tdom tcod) = return (tdom, tcod)+> matchNomArrType t0 = tcError ("Expected an expression of nominal-function type, got " ++ show t0)++> matchForallSup :: TC m => Type -> m (SupportVar, Type)+> matchForallSup (ForallSupT bnd) = unbind bnd+> matchForallSup t0 = tcError ("Expected a support-polymorphic type, got " ++ show t0)++> matchBoxType :: TC m => Type -> m (Type, Support)+> matchBoxType (BoxT t sup) = return (t, sup)+> matchBoxType t0 = tcError ("Expected an expression of code type, got " ++ show t0)++> unExpectArrType :: TC m => Expected (Maybe Type) -> Type -> m (Expected (Maybe Type))+> unExpectArrType (Expecting Nothing) _ = return (Expecting Nothing)+> unExpectArrType (Expecting (Just texp)) t' = do+>   (tdom, tcod) <- matchArrType texp+>   expecting (Expecting (Just tdom)) t'+>   return (Expecting (Just tcod))++> unExpectNomArrType :: TC m => Expected (Maybe Type) -> Type -> m (Expected (Maybe Type))+> unExpectNomArrType (Expecting Nothing) _ = return (Expecting Nothing)+> unExpectNomArrType (Expecting (Just texp)) t' = do+>   (tdom, tcod) <- matchNomArrType texp+>   expecting (Expecting (Just tdom)) t'+>   return (Expecting (Just tcod))++> unExpectForallSupType :: TC m => Expected (Maybe Type) -> SupportVar -> m (Expected (Maybe Type))+> unExpectForallSupType (Expecting Nothing) _ = return (Expecting Nothing)+> unExpectForallSupType (Expecting (Just texp)) sv = do+>   (sv', t) <- matchForallSup texp+>   return (Expecting (Just (swaps (PermM.single (AnyName sv) (AnyName sv')) t)))++> unExpectBoxType :: TC m => Expected (Maybe Type) -> m (Expected (Maybe Type), Expected (Maybe Support))+> unExpectBoxType (Expecting Nothing) = return (Expecting Nothing, Expecting Nothing)+> unExpectBoxType (Expecting (Just t)) = do+>   (t', sup) <- matchBoxType t+>   return (Expecting (Just t'), Expecting (Just sup))++> inferConst :: BaseConst -> BaseType+> inferConst UnitC = UnitT+> inferConst (BoolC _) = BoolT+> inferConst (IntC _) = IntT++> checkPrimitive :: TC m => PrimOp -> [Expr] -> m Type+> checkPrimitive (IfPrim t) [e, thunk1, thunk2] = do+>   wellFormed t+>   let thunkT = unitT `ArrT` t+>   checkExpr e boolT+>   checkExpr thunk1 thunkT+>   checkExpr thunk2 thunkT+>   return thunkT+> checkPrimitive (IfPrim _) es = tcError $ "if expression expected 2 branches, got " ++ show (length es)+> checkPrimitive AddPrim [e1,e2] = checkExpr e1 intT >> checkExpr e2 intT >> return intT+> checkPrimitive AddPrim es = binOpPrimitiveError AddPrim es+> checkPrimitive MulPrim [e1,e2] = checkExpr e1 intT >> checkExpr e2 intT >> return intT+> checkPrimitive MulPrim es = binOpPrimitiveError MulPrim es+> checkPrimitive LeqPrim [e1,e2] = checkExpr e1 intT >> checkExpr e2 intT >> return boolT+> checkPrimitive LeqPrim es = binOpPrimitiveError LeqPrim es+>+> binOpPrimitiveError :: TC m => PrimOp -> [Expr] -> m a+> binOpPrimitiveError p es = tcError $ "expected 2 arguments to " ++ show p ++ ", got " ++ show (length es)+++> checkSubst :: (TC m) => NominalSubst -> Support -> m ()+> checkSubst = go . nominalSubst+>   where+>     go :: (TC m) => [(Nominal, Nom)] -> Support -> m ()+>     go [] = includeSupport+>     go ((nX, ne):noms) = \supIn -> do+>       t <- lookupNom nX+>       checkExpr (nomExpr ne) t+>       go noms (supIn `excludingNominal` nX)++> excludingNominal :: Support -> Nominal -> Support+> excludingNominal (Support noms svs) nX = Support (noms \\ [nX]) svs++> instance Monoid Support where+>   mempty = Support [] []+>   (Support noms svs) `mappend` (Support noms' svs') = Support noms'' svs''+>     where+>       noms'' = nub $ sort (noms ++ noms')+>       svs'' = nub $ sort (svs ++ svs')++> anyOf :: Fold s a -> (a -> Bool) -> s -> Bool+> anyOf l f =  getAny . foldMapOf l (Any . f)++> data Env = Env { envSigma :: NomCtx, envDelta :: [(CodeVar, Embed (Type, Support))], envGamma :: [(Var, Embed Type)] }++> newtype TypeCheck a = TypeCheck { unTypeCheck :: ReaderT Env (WriterT Support (ExceptT String FreshM)) a }+>                     deriving (Functor, Applicative, Monad, Fresh)++> hasSupportNomCtx :: SupportVar -> NomCtx -> Bool+> hasSupportNomCtx  _ NilNC = False+> hasSupportNomCtx sv (SnocNC (unrebind -> (ctx, _))) = hasSupportNomCtx sv ctx+> hasSupportNomCtx sv (SnocSupNC (ctx, sv')) | sv == sv' = True+>                                            | otherwise = hasSupportNomCtx sv ctx+>   ++> lookupNominalNomCtx :: Nominal -> NomCtx -> Maybe (Embed Type)+> lookupNominalNomCtx _ NilNC = Nothing+> lookupNominalNomCtx nX (SnocNC (unrebind -> (ctx, (nY, t)))) | nX == nY = Just t+>                                                              | otherwise = lookupNominalNomCtx nX ctx+> lookupNominalNomCtx nX (SnocSupNC (ctx, _)) = lookupNominalNomCtx nX ctx++> instance TC TypeCheck where+>   lookupSupportVar sv = do+>     b <- TypeCheck $ asks (hasSupportNomCtx sv . envSigma)+>     unless b $ tcError ("Support variable " ++ show sv ++ " not in scope")+>   lookupVar x = do+>     m <- TypeCheck $ asks (lookup x . envGamma)+>     case m of+>       Just t -> return (unembed t)+>       Nothing -> tcError ("Variable " ++ show x ++ " not in scope")+>   lookupCodeVar u = do+>     m <- TypeCheck $ asks (lookup u . envDelta)+>     case m of+>       Just ts -> return (unembed ts)+>       Nothing -> tcError ("Code variable " ++ show u ++ " not in scope")+>   lookupNom nX = do+>     m <- TypeCheck $ asks (lookupNominalNomCtx nX . envSigma)+>     case m of+>       Just t -> return (unembed t)+>       Nothing -> tcError ("Nominal " ++ show nX ++ " not in scope")+>   extendVar x t = TypeCheck . local (\env -> env { envGamma = (x, embed t) : envGamma env  }) . unTypeCheck+>   extendCodeVar u t sup = TypeCheck . local (\env -> env { envDelta = (u, embed (t, sup)) : envDelta env } ) . unTypeCheck+>   extendNom nX t = TypeCheck . local (\env -> env { envSigma = SnocNC (rebind (envSigma env) (nX, embed t)) } ) . unTypeCheck+>   extendSupportVar sv = TypeCheck . local (\env -> env { envSigma = SnocSupNC (envSigma env, sv) } ) . unTypeCheck+> +>   tcError = TypeCheck . throwError+>+>   includeSupport = TypeCheck . tell+>+>   withEmptySupport comp =+>     let censorEverything = const mempty+>     in TypeCheck (pass ((\asup -> (asup, censorEverything)) <$> listen (unTypeCheck comp)))++> inferClosedConfig :: TC m => ClosedConfig -> m Type+> inferClosedConfig bnd = do+>   (ctx, expr) <- unbind bnd+>   inferConfiguration ctx expr++> inferConfiguration :: TC m => NomCtx -> Expr -> m Type+> inferConfiguration ctx = inWellFormedNomCtx ctx . inferExpr++> inWellFormedNomCtx :: TC m => NomCtx -> m a -> m a+> inWellFormedNomCtx NilNC = id+> inWellFormedNomCtx (SnocNC (unrebind -> (ctx, (nX, unembed -> t)))) = \k ->+>   inWellFormedNomCtx ctx $ do+>   wellFormed t+>   extendNom nX t k+> inWellFormedNomCtx (SnocSupNC (ctx,sv)) = inWellFormedNomCtx ctx . extendSupportVar sv ++> runTypeCheck :: TypeCheck a -> Either String (a, Support)+> runTypeCheck comp = runFreshM (runExceptT (runWriterT (runReaderT (unTypeCheck comp) emptyEnv)))+>   where emptyEnv = Env emptySigma emptyDelta emptyGamma+>         emptySigma = NilNC+>         emptyDelta = []+>         emptyGamma = []++Appendix: Pretty Printing+==========================++We need our own pretty printer class because we want locally fresh+names when we descened under binders.++> type Precedence = Int++> class Pretty a where+>   pp :: LFresh m => a -> Precedence -> m PP.Doc++> paren :: Functor m => Bool -> m PP.Doc -> m PP.Doc+> paren b = if b then fmap PP.parens else id++> lowest, quantBodyPrec, arrPrec, arrPrecLeft, boxPrec, quantPrec :: Precedence+> lowest = -1+> quantBodyPrec = 2+> arrPrec = 5+> arrPrecLeft = 6+> boxPrec = 9+> quantPrec = 2++> lamBodyPrec, appPrec :: Precedence+> semiPrec = 1+> letBodyPrec = 1+> lamBodyPrec = 2+> leqPrec = 3+> addPrec = 4+> addPrecRight = 5+> mulPrec = 5+> mulPrecRight = 6+> lambdaPrec = 7+> letPrec = 7+> bindingPrec = 8+> appPrec = 10++> instance Pretty BaseType where+>   pp b _p = pure $ PP.text $ case b of+>     UnitT -> "()"+>     BoolT -> "bool"+>     IntT  -> "int"++> instance Pretty Type where+>   pp t0 p = case t0 of+>     BaseT b -> pp b lowest+>     ArrT t1 t2 -> paren (p > arrPrec) (infixBinary <$> pp t1 arrPrecLeft <*> pure (PP.text "→") <*> pp t2 arrPrec)+>     NomArrT t1 t2 -> paren (p > arrPrec) (infixBinary <$> pp t1 arrPrecLeft <*> pure (PP.text "↛") <*> pp t2 arrPrec)+>     BoxT t sup -> paren (p > boxPrec) (ppboxType <$> pp t boxPrec <*> pp sup lowest)+>     ForallSupT bnd -> paren (p > quantPrec) (quantifier "∀" <$> lunbind bnd (\(sv, t) -> (,) <$> pp sv lowest <*> pp t quantBodyPrec))++> instance Pretty Support where+>   pp (Support noms svs) _dk = ppsupport <$> traverse (fmap decorNominal . flip pp lowest) noms <*> traverse (fmap decorSupportVar . flip pp lowest) svs++> decorSupportVar :: PP.Doc -> PP.Doc+> decorSupportVar = PP.dullblue++> decorCodeVar :: PP.Doc -> PP.Doc+> decorCodeVar = PP.dullmagenta++> decorNominal :: PP.Doc -> PP.Doc+> decorNominal = PP.bold++> instance Pretty (Name a) where+>   pp a _dk = pure $ PP.text $ show a++> ppboxType :: PP.Doc -> PP.Doc -> PP.Doc+> ppboxType t sup = PP.hang 2 (PP.text "□_" PP.<> sup PP.</> PP.group t)++> ppsupport :: [PP.Doc] -> [PP.Doc] -> PP.Doc+> ppsupport noms svs = PP.group $ PP.hang 2 $ PP.braces $ PP.fillSep $ PP.punctuate PP.comma (noms ++ svs)+++> infixBinary :: PP.Doc -> PP.Doc -> PP.Doc -> PP.Doc+> infixBinary p1 s p2 = PP.group $ PP.fillSep [p1, s, p2]++> quantifier :: String -> (PP.Doc, PP.Doc) -> PP.Doc+> quantifier q (obj, body) = PP.text q PP.<//> obj PP.<//> PP.dot PP.<//> body++> instance Pretty Expr where+>   pp e0 p = case e0 of+>     V x -> pp x lowest+>     U subs u -> (PP.<>) <$> pp subs lowest <*> (fmap decorCodeVar . flip pp lowest) u+>     N nom -> decorNominal <$> pp nom lowest+>     C c -> pp c lowest+>     P prim vs es -> paren (p > primPrecedence prim) (ppPrimitive prim (vs ++ es))+>     Lambda bnd -> paren (p > lambdaPrec) (pplambda "λ" <$> lunbind bnd (\((x, unembed -> t), e) -> (,) <$> (colonclass <$> pp x lowest <*> pp t lowest) <*> pp e lamBodyPrec))+>     RecFun bnd -> paren (p > lambdaPrec) (pprecfun <$> lunbind bnd (\((f, x, unembed -> targ, unembed -> tres), e) -> (,,,,) <$> pp f lowest <*> pp x lowest <*> pp targ lowest <*> pp tres lowest <*> pp e lamBodyPrec ))+>     App e1 e2 -> paren (p > appPrec) (ppapp <$> pp e1 appPrec <*> pp e2 (appPrec + 1))+>     Let e1 bnd -> paren (p > letPrec) (pplet PP.empty <$> pp e1 bindingPrec <*> lunbind bnd (\(x, e2) -> (,) <$> pp x lowest <*> pp e2 letBodyPrec))+>     LetBox e1 bnd -> paren (p > letPrec) (pplet (PP.text "□") <$> pp e1 bindingPrec <*> lunbind bnd (\(u, e2) -> (,) <$> (fmap decorCodeVar . flip pp lowest) u <*> pp e2 letBodyPrec))+>     Box code -> pp code lowest+>     New bnd -> paren (p > lambdaPrec) (pplambda "ν" <$> lunbind bnd (\((nX, unembed -> t), e) -> (,) <$> ppnombind nX t <*> pp e lamBodyPrec))+>     Choose e -> paren (p > appPrec) (ppapp (PP.text "choose") <$> pp e appPrec)+>     PLamSupport bnd -> paren (p > lambdaPrec) (pplambda "Λ" <$> lunbind bnd (\(sv, e) -> (,) <$> (fmap decorSupportVar . flip pp lowest) sv <*> pp e lamBodyPrec))+>     PAppSupport e sup -> paren (p > appPrec) (PP.nest 2 <$> ((PP.</>) <$> (fmap PP.group . flip pp appPrec) e <*> pp sup lowest))++> ppnombind nX t = assocclass <$> fmap decorNominal (pp nX lowest) <*> pp t lowest++> instance Pretty Code where+>   pp (Code e) _dk = ppcode <$> pp e lowest+>     where+>       ppcode c = PP.enclose (PP.text "“") (PP.text "”") (PP.underline c)++> instance Pretty BaseConst where+>   pp bc _dk = pure $ case bc of+>     UnitC -> PP.text "()"+>     BoolC b -> PP.text $ show b+>     IntC i -> PP.int i++> primPrecedence :: PrimOp -> Precedence+> primPrecedence (IfPrim _) = appPrec+> primPrecedence AddPrim = addPrec+> primPrecedence MulPrim = mulPrec+> primPrecedence LeqPrim = leqPrec+>+> ppPrimitive :: LFresh m => Pretty a => PrimOp -> [a] -> m PP.Doc+> ppPrimitive (IfPrim t) es = do+>   let prettyExpr = fmap PP.group . flip pp semiPrec+>   pes <- traverse prettyExpr es+>   pt <- pp t lowest+>   return $ PP.group (PP.text "if" PP.</> (PP.parens $ PP.group $ PP.align $ PP.vsep $ PP.punctuate PP.semi (pt:pes)))+> ppPrimitive AddPrim [e1,e2] = infixBinary <$> pp e1 addPrec <*> pure (PP.text "+") <*> pp e2 addPrecRight+> ppPrimitive MulPrim [e1,e2] = infixBinary <$> pp e1 mulPrec <*> pure (PP.text "*") <*> pp e2 mulPrecRight+> ppPrimitive LeqPrim [e1,e2] = infixBinary <$> pp e1 leqPrec <*> pure (PP.text "≤") <*> pp e2 leqPrec+> ppPrimitive _ _ = error "cant' happen (in well-typed code)"++> colonclass :: PP.Doc -> PP.Doc -> PP.Doc+> colonclass v clas = v PP.<//> PP.colon PP.<//> clas++> assocclass :: PP.Doc -> PP.Doc -> PP.Doc+> assocclass v clas = v PP.<//> PP.text "∼" PP.<//> clas++> pplambda :: String -> (PP.Doc, PP.Doc) -> PP.Doc+> pplambda lam (vclas, body) = PP.group $ PP.align $ PP.vsep [PP.group (PP.vcat [PP.text lam, vclas, PP.dot]), PP.group body]++> ppapp :: PP.Doc -> PP.Doc -> PP.Doc+> ppapp e1 e2 = PP.group $ PP.align $ PP.vsep [PP.group e1, PP.nest 2 (PP.group e2)]++> pprecfun :: (PP.Doc, PP.Doc, PP.Doc, PP.Doc, PP.Doc) -> PP.Doc+> pprecfun (f, x, targ, tres, e) = PP.group $ PP.hang 2 $ PP.vsep [PP.text "rec", PP.group (PP.sep [f, binding, PP.colon, tres]), PP.group (PP.text "is" PP.</> PP.nest 2 (PP.group e))]+>   where+>     binding = PP.parens (colonclass x targ)++> pplet :: PP.Doc -> PP.Doc -> (PP.Doc, PP.Doc) -> PP.Doc+> pplet unclas e1 (x,e2) = PP.fillSep [PP.text "let", PP.hang 2 binding] PP.</> PP.group (PP.hang 2 (PP.text "in" PP.</> PP.nest 2 e2))+>   where+>     binding = PP.group (PP.fillSep [unclas PP.<//> x, PP.text "="] PP.</> PP.hang 2 e1)++> instance Pretty NominalSubst where+>   pp (NominalSubst subs) _dk =+>     ppsubstitution <$> traverse ppsub subs+>     where+>       ppsubstitution = PP.enclose (PP.text "⟨") (PP.text "⟩") . PP.fillSep . PP.punctuate PP.comma+>       ppsub (nX, nom) = mapto <$> (fmap decorNominal . flip pp lowest) nX <*> pp nom lowest+>       mapto nX nom = PP.group (nX PP.</> PP.text "↦") PP.</> nom++> instance Pretty Nom where+>   pp = pp . nomExpr++> pretty :: Pretty a => a -> String+> pretty a = flip PP.displayS "" $ PP.renderSmart 0.8 80 $ runLFreshM $ pp a lowest++> ppretty :: Pretty a => a -> IO ()+> ppretty a = do+>   PP.displayIO IO.stdout $ PP.renderSmart 0.8 80 $ runLFreshM $ pp a lowest+>   putStrLn ""++Example+-------++> -- >>> ppretty (pexp @@ number 3)+> -- (λn:int.+> -- choose+> --  (νX∼int.+> --   let □w = (Λp.+> --             λe:□_{p} int.+> --             rec+> --               go (m:int) : □_{p} int+> --               is if (□_{p} int;+> --                      m ≤ 0;+> --                      λ_:(). “1”;+> --                      λ_:(). let □u = go (m + -1) in let □w = e in “⟨⟩u * ⟨⟩w”)+> --                  ()) {X}+> --            “X”+> --            n in “λx:int. ⟨X ↦ x⟩w”))+> -- 3++Appendix: Tracing evaluator+===========================++> instance Pretty NomCtx where+>   pp NilNC _ = pure PP.empty+>   pp (SnocNC (unrebind -> (NilNC, (nX, unembed -> t)))) _ = ppnombind nX t+>   pp (SnocNC (unrebind -> (ctx, (nX, unembed -> t)))) _ = (PP.</>) <$> fmap (\pctx -> pctx PP.</> PP.comma) (pp ctx lowest) <*> ppnombind nX t+>   pp (SnocSupNC (NilNC, sv)) _ = decorSupportVar <$> pp sv lowest+>   pp (SnocSupNC (ctx, sv)) _ = (PP.</>) <$> fmap (\pctx -> pctx PP.</> PP.comma) (pp ctx lowest) <*> (decorSupportVar <$> pp sv lowest)++> data WellTypedProgram = WellTypedProgram NomCtx Expr Type Support+>+> instance Pretty WellTypedProgram where+>   pp (WellTypedProgram ctx e t sup) _ = do+>     pctx <- pp ctx lowest+>     pe <- pp e lowest+>     pt <- pp t lowest+>     psup <- pp sup lowest+>     return $ PP.group $ PP.vcat [pctx, PP.text "⊢", pe, PP.nest 2 PP.colon, PP.nest 4 pt, PP.nest 4 psup]++> traceProgram :: Expr -> IO ()+> traceProgram initialExpr = do+>   let tc ctx e = case runTypeCheck (inferConfiguration ctx e) of+>         Right (t, sup) -> ppretty (WellTypedProgram ctx e t sup)+>         Left err -> putStrLn err >> fail "(Not running)"+>   let+>     trace :: (Fresh m, MonadState NomCtx m, MonadError String m, MonadIO m) => Expr -> m ()+>     trace e =+>         if isValue e+>         then return ()+>         else+>         do+>           e' <- step e+>           ctx <- get+>           liftIO $ do+>             tc ctx e'+>             putStrLn "————"+>           trace e'+>   tc NilNC initialExpr+>   putStrLn "————"+>   _ <- runFreshMT (runExceptT (runStateT (trace initialExpr) NilNC))+>   return ()+> _ = ()++

@@ -0,0 +1,42 @@+{-# language GADTs, RankNTypes #-}+module Prof where++import Data.Profunctor++data Shop a b s t where+  Shop :: (s -> a) -> (s -> b -> t) -> Shop a b s t++type Optic p s t a b  = p a b -> p s t+type Lens s t a b = forall p . (Strong p) => Optic p s t a b++lens :: (s -> a) -> (s -> b -> t) -> Lens s t a b+lens get set pab = dimap (\s -> (s, get s)) (uncurry set) (second' pab)++instance Profunctor (Shop a b) where+  dimap f g (Shop get set) = Shop (get . f) (\s -> g . set (f s))++instance Strong (Shop a b) where+   first' (Shop get set) = Shop (get . fst) (\(s,c) b -> (set s b, c))++withLens :: Lens s t a b -> ((s -> a) -> (s -> b -> t) -> r) -> r+withLens l k = case l (Shop id (const id)) of+                 Shop getter setter -> k getter setter+++type Prism s t a b = forall p . (Choice p) => Optic p s t a b++prism :: (s -> Either t a) -> (b -> t) -> Prism s t a b+prism view review pab = dimap view (either id review) (right' pab)++data Market a b s t where+  Market :: (s -> Either t a) -> (b -> t) -> Market a b s t++instance Profunctor (Market a b) where+  dimap f g (Market view review) = Market (either (Left . g) Right . (view . f)) (g . review)++instance Choice (Market a b) where+  left' (Market view review) = Market (either (either (Left . Left) Right . view) (Left . Right)) (Left . review)++withPrism :: Prism s t a b -> ((s -> Either t a) -> (b -> t) -> r) -> r+withPrism l k = case l (Market Right id) of+                  Market view review -> k view review

@@ -58,8 +58,9 @@ import Data.Functor.Contravariant (Contravariant(..)) import Data.Foldable (Foldable(..)) import Data.List (intersect)-import Data.Monoid (Monoid(..), (<>), All(..))+import Data.Monoid (Monoid(..), All(..)) import Data.Ratio (Ratio)+import Data.Semigroup as Sem import Data.Typeable (Typeable, gcast, typeOf) import GHC.Generics @@ -117,13 +118,17 @@ -- @ newtype DisjointSet a = DisjointSet (Maybe [a]) -instance Eq a => Monoid (DisjointSet a) where-  mempty = DisjointSet (Just [])-  mappend s1 s2 =+-- | @since 0.3.2+instance Eq a => Sem.Semigroup (DisjointSet a) where+  (<>) = \s1 s2 ->     case (s1, s2) of       (DisjointSet (Just xs), DisjointSet (Just ys)) | disjointLists xs ys -> DisjointSet (Just (xs <> ys))       _ -> inconsistentDisjointSet +instance Eq a => Monoid (DisjointSet a) where+  mempty = DisjointSet (Just [])+  mappend = (<>)+ instance Foldable DisjointSet where   foldMap summarize (DisjointSet ms) = foldMap (foldMap summarize) ms @@ -262,12 +267,13 @@   {-# INLINE fmap #-}  instance Applicative (FFM f) where-  pure = return+  pure x = FFM (\r _j -> r x)+  {-# INLINE pure #-}   (FFM h) <*> (FFM k) = FFM (\r j -> h (\f -> k (r . f) j) j)   {-# INLINE (<*>) #-}  instance Monad (FFM f) where-  return x = FFM (\r _j -> r x)+  return = pure   {-# INLINE return #-}   (FFM h) >>= f = FFM (\r j -> h (\x -> runFFM (f x) r j) j)   {-# INLINE (>>=) #-}@@ -291,13 +297,17 @@ -- is the @i@th name in @a@ newtype NthPatFind = NthPatFind { runNthPatFind :: Integer -> Either Integer AnyName } -instance Monoid NthPatFind where-  mempty = NthPatFind Left-  mappend (NthPatFind f) (NthPatFind g) =+-- | @since 0.3.2+instance Sem.Semigroup NthPatFind where+  (<>) = \(NthPatFind f) (NthPatFind g) ->     NthPatFind $ \i -> case f i of     Left i' -> g i'     found@Right {} -> found +instance Monoid NthPatFind where+  mempty = NthPatFind Left+  mappend = (<>)+ -- | The result of @'namePatFind' a x@ is either @Left i@ if @a@ is a pattern that -- contains @i@ free names none of which are @x@, or @Right j@ if @x@ is the @j@th name -- in @a@@@ -306,14 +316,18 @@                                                       -- Right - index of the name we found                                                       -> Either Integer Integer } -instance Monoid NamePatFind where-  mempty = NamePatFind (\_ -> Left 0)-  mappend (NamePatFind f) (NamePatFind g) =+-- | @since 0.3.2+instance Sem.Semigroup NamePatFind where+  (<>) = \(NamePatFind f) (NamePatFind g) ->     NamePatFind $ \nm -> case f nm of     ans@Right {} -> ans     Left n -> case g nm of       Left m -> Left $! n + m       Right i -> Right $! n + i++instance Monoid NamePatFind where+  mempty = NamePatFind (\_ -> Left 0)+  mappend = (<>)  -- | The "Generic" representation version of 'Alpha' class GAlpha f where

@@ -19,6 +19,7 @@  import Control.Monad.Identity +import Control.Monad.Catch (MonadThrow, MonadCatch, MonadMask) import Control.Monad.Trans import Control.Monad.Trans.Except import Control.Monad.Trans.Error@@ -53,7 +54,18 @@ --   still globally unused, and increments the index every time it is --   asked for a fresh name. newtype FreshMT m a = FreshMT { unFreshMT :: St.StateT Integer m a }-  deriving (Functor, Applicative, Alternative, Monad, MonadPlus, MonadIO, MonadFix)+  deriving+    ( Functor+    , Applicative+    , Alternative+    , Monad+    , MonadIO+    , MonadPlus+    , MonadFix+    , MonadThrow+    , MonadCatch+    , MonadMask+    )  -- | Run a 'FreshMT' computation (with the global index starting at zero). runFreshMT :: Monad m => FreshMT m a -> m a

@@ -63,6 +63,7 @@ import Data.Monoid import Data.Typeable (Typeable) +import Control.Monad.Catch (MonadThrow, MonadCatch, MonadMask) import Control.Monad.Reader import Control.Monad.Identity import Control.Applicative (Applicative, Alternative)@@ -102,7 +103,18 @@ -- avoid, and when asked for a fresh one will choose the first numeric -- prefix of the given name which is currently unused. newtype LFreshMT m a = LFreshMT { unLFreshMT :: ReaderT (Set AnyName) m a }-  deriving (Functor, Applicative, Alternative, Monad, MonadIO, MonadPlus, MonadFix)+  deriving+    ( Functor+    , Applicative+    , Alternative+    , Monad+    , MonadIO+    , MonadPlus+    , MonadFix+    , MonadThrow+    , MonadCatch+    , MonadMask+    )  -- | Run an 'LFreshMT' computation in an empty context. runLFreshMT :: LFreshMT m a -> m a

@@ -47,9 +47,10 @@   ) where  import Prelude (Eq(..), Show(..), (.), ($), Monad(return), Ord(..), Maybe(..), otherwise, (&&), Bool(..), id, uncurry, Functor(..))-import Data.Monoid+import Data.Monoid hiding ((<>)) import Data.List import Data.Map (Map)+import Data.Semigroup as Sem import qualified Data.Map as M import qualified Data.Set as S import Control.Arrow ((&&&))@@ -97,10 +98,15 @@   Perm (M.fromList ([ (x,M.findWithDefault y y b) | (x,y) <- M.toList a]          ++ [ (x, M.findWithDefault x x b) | x <- M.keys b, M.notMember x a])) --- | Permutations form a monoid under composition.+-- | Permutations form a semigroup under 'compose'.+-- @since 0.3.2+instance Ord a => Sem.Semigroup (Perm a) where+  (<>) = compose++-- | Permutations form a monoid with identity 'empty'. instance Ord a => Monoid (Perm a) where   mempty  = empty-  mappend = compose+  mappend = (<>)  -- | Is this the identity permutation? isid :: Ord a => Perm a -> Bool

@@ -2,7 +2,7 @@ -- documentation, see http://haskell.org/cabal/users-guide/  name:                unbound-generics-version:             0.3.1+version:             0.3.2 synopsis:            Support for programming with names and binders using GHC Generics description:         Specify the binding structure of your data type with an                      expressive set of type combinators, and unbound-generics@@ -12,7 +12,7 @@                      @Unbound.Generics.LocallyNameless@ to get started.                      .                      This is an independent re-implementation of <http://hackage.haskell.org/package/unbound Unbound>-                     but using <http://www.haskell.org/ghc/docs/latest/html/libraries/base-4.9.0.0/GHC-Generics.html GHC.Generics>+                     but using <https://hackage.haskell.org/package/base/docs/GHC-Generics.html GHC.Generics>                      instead of <http://hackage.haskell.org/package/RepLib RepLib>.                      See the accompanying README for some porting notes.                      @@ -22,14 +22,14 @@ license-file:        LICENSE author:              Aleksey Kliger maintainer:          aleksey@lambdageek.org-copyright:           (c) 2014-2016, Aleksey Kliger+copyright:           (c) 2014-2018, Aleksey Kliger category:            Language build-type:          Simple-extra-source-files:  examples/*.hs,+extra-source-files:  examples/*.hs, examples/*.lhs,                      README.md,                      Changelog.md cabal-version:       >=1.10-tested-with: GHC == 7.6.3, GHC == 7.8.4, GHC == 7.10.3, GHC == 8.0.1+tested-with: GHC == 7.6.3, GHC == 7.8.4, GHC == 7.10.3, GHC == 8.0.1, GHC == 8.2.2, GHC == 8.4.1               library   exposed-modules:     Unbound.Generics.LocallyNameless@@ -54,16 +54,22 @@   -- other-extensions:       build-depends:       base >=4.6 && <5,                        template-haskell >= 2.8.0.0,-                       deepseq >= 1.3,+                       deepseq >= 1.3.0.0,                        mtl >= 2.1,                        transformers >= 0.3,                        transformers-compat >= 0.3,                        containers == 0.5.*,                        contravariant >= 0.5,-                       profunctors >= 4.0+                       profunctors >= 4.0,+                       ansi-wl-pprint >= 0.6.7.2 && < 0.7,+                       exceptions >= 0.8 && < 0.9   hs-source-dirs:      src   default-language:    Haskell2010   ghc-options:         -Wall+  if impl (ghc >= 8.0.0)+    ghc-options:     -Wcompat+  if !impl(ghc >= 8.0)+    build-depends: semigroups == 0.18.*  Test-Suite test-unbound-generics   type:                exitcode-stdio-1.0@@ -88,6 +94,8 @@   hs-source-dirs:      test   default-language:    Haskell2010   ghc-options:         -Wall+  if impl (ghc >= 8.0.0)+    ghc-options:     -Wcompat  Benchmark benchmark-unbound-generics   type:                exitcode-stdio-1.0@@ -95,12 +103,19 @@   hs-source-dirs:      benchmarks   main-is:             benchmark-main.hs   build-depends:       base-                     , criterion+                     , criterion >= 1.0.0.1                      , deepseq >= 1.3.0.0-                     , deepseq-generics >= 0.1.1.2                      , unbound-generics+  if impl (ghc == 7.6.*)+    build-depends:     unix <= 2.6.0.1+  if impl (ghc == 7.6.*) || impl (ghc == 7.8.*)+    build-depends:     deepseq-generics+  else+    build-depends:     deepseq >= 1.4.0.0   other-modules:       BenchLam   ghc-options:       -Wall+  if impl (ghc >= 8.0.0)+    ghc-options:     -Wcompat  source-repository head   type:                git