unbound-generics 0.1.2.1 → 0.2

raw patch · 12 files changed

+281/−8 lines, 12 filesdep +criteriondep +deepseqdep +deepseq-genericsdep ~basePVP ok

version bump matches the API change (PVP)

Dependencies added: criterion, deepseq, deepseq-generics

Dependency ranges changed: base

API changes (from Hackage documentation)

Files

• Changelog.md +19/−0
• README.md +61/−0
• benchmarks/BenchLam.hs +75/−0
• benchmarks/benchmark-main.hs +20/−0
• src/Unbound/Generics/LocallyNameless/Alpha.hs +64/−6
• src/Unbound/Generics/LocallyNameless/Bind.hs +5/−0
• src/Unbound/Generics/LocallyNameless/Embed.hs +5/−1
• src/Unbound/Generics/LocallyNameless/Name.hs +5/−0
• src/Unbound/Generics/LocallyNameless/Rebind.hs +4/−0
• src/Unbound/Generics/LocallyNameless/Rec.hs +4/−0
• src/Unbound/Generics/LocallyNameless/Shift.hs +4/−0
• unbound-generics.cabal +15/−1

@@ -1,3 +1,22 @@+# 0.2++* Incorporating some of the extras/oversights from+  [clash-lib Unbound.Generics.LocallyNameless.Extra](https://github.com/clash-lang/clash-compiler/blob/master/clash-lib/src/Unbound/Generics/LocallyNameless/Extra.hs)++	* Make `Embed` an instance of `Ord`+	* `NFData` instances (see below)++* Re-implement `freshen'` and `gfreshen` using a free monad to give+  GHC a chance to inline it all away.  This changes the type of+  `gfreshen`.  Major version bump.++	* Expose `FFM`, `liftFFM` and `retractFFM`++* Provide `NFData` instances for all the combinators.+  Depend on 'deepseq'++* Start benchmarking some of the operations (particularly `unbind`).+ # 0.1.2.1  * Fix ghc-7.10 build.

@@ -2,9 +2,70 @@  [![Build Status](https://travis-ci.org/lambdageek/unbound-generics.svg)](https://travis-ci.org/lambdageek/unbound-generics) +Support for programming with names and binders using GHC Generics. +## Summary++Specify the binding structure of your data type with an expressive set of type combinators, and `unbound-generics`+handles the rest!  Automatically derives alpha-equivalence, free variable calculation, capture-avoiding substitution, and more. See [`Unbound.Generics.LocallyNameless`](src/Unbound/Generics/LocallyNameless.hs) to get started.+ 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++Here is how you would implement call by value evaluation for the untyped lambda calculus:++```haskell+{-# LANGUAGE DeriveDataTypeable, DeriveGeneric, MultiParamTypeClasses #-}+module UntypedLambdaCalc where+import Unbound.Generics.LocallyNameless+import GHC.Generics (Generic)+import Data.Typeable (Typeable)++-- | Variables stand for expressions+type Var = Name Expr++-- | Expressions+data Expr = V Var                -- ^ variables+          | Lam (Bind Var Expr) -- ^ lambdas bind a variable within a body expression+          | App Expr Expr       -- ^ application+          deriving (Show, Generic, Typeable)++-- Automatically construct alpha equivalence, free variable computation and binding operations.+instance Alpha Expr++-- semi-automatically implement capture avoiding substitution of expressions for expressions+instance Subst Expr Expr where+  -- `isvar` identifies the variable case in your AST.+  isvar (V x) = Just (SubstName x)+  isvar _     = Nothing++-- evaluation takes an expression and returns a value while using a source of fresh names+eval :: Expr -> FreshM Expr+eval (V x) = fail $ "unbound variable " ++ show x+eval e@(Lam {}) = return e+eval (App e1 e2) = do+  v1 <- eval e1+  v2 <- eval e2+  case v1 of+   (Lam bnd) -> do+     -- open the lambda by picking a fresh name for the bound variable x in body+     (x, body) <- unbind bnd+     let body' = subst x v2 body+     eval body'+   _ -> fail "application of non-lambda"++example :: Expr+example =+  let x = s2n "x"+      y = s2n "y"+      e = Lam $ bind x (Lam $ bind y (App (V y) (V x)))+  in runFreshM $ eval (App (App e e) e)+  +-- >>> example+-- Lam (<y> App (V 0@0) (Lam (<x> Lam (<y> App (V 0@0) (V 1@0)))))++``` ## Differences from `unbound`  For the most part, I tried to keep the same methods with the same signatures.  However there are a few differences.

@@ -0,0 +1,75 @@+-- | Untyped lambda calc for benchmarking+{-# LANGUAGE DeriveGeneric, DeriveDataTypeable #-}+module BenchLam where++import Control.Applicative+import Control.Monad (replicateM)+import Data.List (foldl')++import GHC.Generics (Generic)+import Data.Typeable (Typeable)++import Control.DeepSeq (NFData(..), deepseq)+import Control.DeepSeq.Generics (genericRnf)+import Criterion (Benchmark, env, bench, nf)++import Unbound.Generics.LocallyNameless++type Var = Name Term++data Term =+  V !Var+  | App !Term !Term+  | Lam !(Bind Var Term)+    deriving (Show, Generic, Typeable)++instance Alpha Term+instance NFData Term where rnf = genericRnf+++-- | lambda abstract over all the given vars+lams :: [Var] -> Term -> Term+lams [] = id+lams (v:vs) = Lam . bind v . lams vs++-- | apply the given term to the given terms+apps :: Term -> [Term] -> Term+apps = foldl' App++-- eta-expand a term a given number of times+etaN :: Fresh m => Term -> Int -> m Term+etaN m n = do+  vs <- replicateM n (fresh $ s2n "v")+  let ms = map V vs+  return (lams vs $ apps m ms)++-- | While the head is a lambda, descend under it and then do something;+-- then close all the lambdas back up.+workHeadUnderLams :: Fresh m => (Term -> m Term) -> (Term -> m Term)+workHeadUnderLams comp = go+  where+    go m =+      case m of+      Lam bnd -> do+        (x, m') <- unbind bnd+        m'' <- go m'+        return $ Lam $ bind x m''+      _ -> comp m++freshNeutralTermHead :: (Applicative m, Fresh m) => Term -> m Term+freshNeutralTermHead (App m n) = App <$> freshNeutralTermHead m <*> pure n+freshNeutralTermHead (V v) = V <$> fresh v+freshNeutralTermHead lam@(Lam {}) = return lam++-- | A benchmark that creates an eta expansion of the term "x" of a given size+-- and then freshens the "x" by traversing down below all the lambdas.+--+-- Every time we go under a lambda, we freshen the body, so to go+-- under N lambdas, we do O(N²) work.+freshenEtaTermBench :: Int -> Benchmark+freshenEtaTermBench n =+  let name = "freshen eta term of size " ++ show n+  in name `deepseq` env setup $ \m ->+  bench name $ nf (runFreshM . workHeadUnderLams freshNeutralTermHead) m+  where+    setup = return $ runFreshM $ etaN (V $ s2n "x") n

@@ -0,0 +1,20 @@+module Main where++import Criterion.Main++import BenchLam (freshenEtaTermBench)++main :: IO ()+main =+  defaultMain+  [+    bgroup "unbound-generics" [+        freshenEtaTermBench 10+        , freshenEtaTermBench 20+        , freshenEtaTermBench 30+        , freshenEtaTermBench 40+        , freshenEtaTermBench 50+        , freshenEtaTermBench 100+        , freshenEtaTermBench 200+        ]+  ]

@@ -9,7 +9,9 @@ -- Use the 'Alpha' typeclass to mark types that may contain 'Name's. {-# LANGUAGE DefaultSignatures              , FlexibleContexts-             , TypeOperators #-}+             , TypeOperators+             , RankNTypes+  #-} module Unbound.Generics.LocallyNameless.Alpha (   -- * Name-aware opertions   Alpha(..)@@ -43,6 +45,10 @@   , gfreshen   , glfreshen   , gacompare+    -- ** Interal helpers for gfreshen+  , FFM+  , liftFFM+  , retractFFM   ) where  import Control.Applicative (Applicative(..), (<$>))@@ -216,13 +222,59 @@   -- in the given term to be distinct from all other names seen in the monad @m@.   freshen' :: Fresh m => AlphaCtx -> a -> m (a, Perm AnyName)   default freshen'  :: (Generic a, GAlpha (Rep a), Fresh m) => AlphaCtx -> a -> m (a, Perm AnyName)-  freshen' ctx = liftM (first to) . gfreshen ctx . from+  freshen' ctx = retractFFM . liftM (first to) . gfreshen ctx . from    -- | See 'Unbound.Generics.LocallyNameless.Operations.acompare'. An alpha-respecting total order on terms involving binders.   acompare' :: AlphaCtx -> a -> a -> Ordering   default acompare' :: (Generic a, GAlpha (Rep a)) => AlphaCtx -> a -> a -> Ordering   acompare' c = (gacompare c) `on` from +-- Internal: the free monad over the Functor f.  Note that 'freshen''+-- has a monadic return type and moreover we have to thread the+-- permutation through the 'gfreshen' calls to crawl over the value+-- constructors.  Since we don't know anything about the monad @m@,+-- GHC can't help us.  But note that none of the code in the generic+-- 'gfreshen' instances actually makes use of the 'Fresh.fresh'+-- function; they just plumb the dictionary through to any 'K' nodes+-- that happen to contain a value of a type like 'Name' that does+-- actually freshen something.  So what we do is we actually make+-- gfreshen work not in the monad @m@, but in the monad @FFM m@ and+-- then use 'retractFFM' in the default 'Alpha' method to return back+-- down to @m@.  We don't really make use of the fact that 'FFM'+-- reassociates the binds of the underlying monad, but it doesn't hurt+-- anything.  Mostly what we care about is giving the inliner a chance+-- to eliminate most of the monadic plumbing.+newtype FFM f a = FFM { runFFM :: forall r . (a -> r) -> (f r -> r) -> r }++instance Functor (FFM f) where+  fmap f (FFM h) = FFM (\r j -> h (r . f) j)+  {-# INLINE fmap #-}++instance Applicative (FFM f) where+  pure = return+  (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)+  {-# INLINE return #-}+  (FFM h) >>= f = FFM (\r j -> h (\x -> runFFM (f x) r j) j)+  {-# INLINE (>>=) #-}++instance Fresh m => Fresh (FFM m) where+  fresh = liftFFM . fresh +  {-# INLINE fresh #-}++liftFFM :: Monad m => m a -> FFM m a+liftFFM m = FFM (\r j -> j (liftM r m))+{-# INLINE liftFFM #-}++retractFFM :: Monad m => FFM m a -> m a+retractFFM (FFM h) = h return j+  where+    j mmf = mmf >>= \mf -> mf+{-# INLINE retractFFM #-}+ -- | The result of @'nthPatFind' a i@ is @Left k@ where @k@ is the -- number of names in pattern @a@ with @k < i@ or @Right x@ where @x@ -- is the @i@th name in @a@@@ -250,7 +302,7 @@   gnamePatFind :: f a -> NamePatFind    gswaps :: AlphaCtx -> Perm AnyName -> f a -> f a-  gfreshen :: Fresh m => AlphaCtx -> f a -> m (f a, Perm AnyName)+  gfreshen :: Fresh m => AlphaCtx -> f a -> FFM m (f a, Perm AnyName)    glfreshen :: LFresh m => AlphaCtx -> f a -> (f a -> Perm AnyName -> m b) -> m b @@ -271,7 +323,8 @@   gnamePatFind = namePatFind . unK1    gswaps ctx perm = K1 . swaps' ctx perm . unK1-  gfreshen ctx = liftM (first K1) . freshen' ctx . unK1+  gfreshen ctx = liftM (first K1) . liftFFM . freshen' ctx . unK1+  {-# INLINE gfreshen #-}    glfreshen ctx (K1 c) cont = lfreshen' ctx c (cont . K1) @@ -293,6 +346,7 @@    gswaps ctx perm = M1 . gswaps ctx perm . unM1   gfreshen ctx = liftM (first M1) . gfreshen ctx . unM1+  {-# INLINE gfreshen #-}    glfreshen ctx (M1 f) cont =     glfreshen ctx f (cont . M1)@@ -315,6 +369,7 @@    gswaps _ctx _perm _ = U1   gfreshen _ctx _ = return (U1, mempty)+  {-# INLINE gfreshen #-}    glfreshen _ctx _ cont = cont U1 mempty @@ -336,6 +391,7 @@    gswaps _ctx _perm _ = undefined   gfreshen _ctx _ = return (undefined, mempty)+  {-# INLINE gfreshen #-}    glfreshen _ctx _ cont = cont undefined mempty @@ -367,9 +423,10 @@     gswaps ctx perm f :*: gswaps ctx perm g    gfreshen ctx (f :*: g) = do-    (g', perm2) <- gfreshen ctx g-    (f', perm1) <- gfreshen ctx (gswaps ctx perm2 f)+    ~(g', perm2) <- gfreshen ctx g+    ~(f', perm1) <- gfreshen ctx (gswaps ctx perm2 f)     return (f' :*: g', perm1 <> perm2)+  {-# INLINE gfreshen #-}    glfreshen ctx (f :*: g) cont =     glfreshen ctx g $ \g' perm2 ->@@ -409,6 +466,7 @@    gfreshen ctx (L1 f) = liftM (first L1) (gfreshen ctx f)   gfreshen ctx (R1 f) = liftM (first R1) (gfreshen ctx f)+  {-# INLINE gfreshen #-}      glfreshen ctx (L1 f) cont =     glfreshen ctx f (cont . L1)

@@ -18,6 +18,7 @@   ) where  import Control.Applicative (Applicative(..), (<$>))+import Control.DeepSeq (NFData(..)) import Data.Monoid ((<>))  import GHC.Generics (Generic)@@ -33,6 +34,9 @@ data Bind p t = B p t               deriving (Generic) +instance (NFData p, NFData t) => NFData (Bind p t) where+  rnf (B p t) = rnf p `seq` rnf t `seq` ()+ instance (Show p, Show t) => Show (Bind p t) where   showsPrec prec (B p t) =     showParen (prec > 0) (showString "<"@@ -70,6 +74,7 @@     (p', perm1) <- freshen' (patternCtx ctx) p     (t', perm2) <- freshen' (incrLevelCtx ctx) (swaps' (incrLevelCtx ctx) perm1 t)     return (B p' t', perm1 <> perm2)+  {-# INLINE freshen' #-}    lfreshen' ctx (B p t) cont =     lfreshen' (patternCtx ctx) p $ \p' pm1 ->

@@ -11,6 +11,7 @@ module Unbound.Generics.LocallyNameless.Embed where  import Control.Applicative (pure, (<$>))+import Control.DeepSeq (NFData(..)) import Data.Monoid (mempty) import Data.Profunctor (Profunctor(..)) @@ -31,7 +32,7 @@ --   (You may also use the functions 'embed' and 'unembed', which --   additionally can construct or destruct any number of enclosing --   'Shift's at the same time.)-newtype Embed t = Embed t deriving (Eq, Generic)+newtype Embed t = Embed t deriving (Eq, Ord, Generic)  class IsEmbed e where   -- | The term type embedded in the embedding 'e'@@ -49,6 +50,9 @@   type Embedded (Embed t) = t   embedded = iso (\(Embed t) -> t) Embed   +instance NFData t => NFData (Embed t) where+  rnf (Embed t) = rnf t `seq` ()+ instance Show a => Show (Embed a) where   showsPrec _ (Embed a) = showString "{" . showsPrec 0 a . showString "}" 

@@ -27,6 +27,7 @@        , AnyName(..)        ) where +import Control.DeepSeq (NFData(..)) import Data.Typeable (Typeable, gcast, typeOf) import GHC.Generics (Generic) @@ -48,6 +49,10 @@ data Name a = Fn String !Integer    -- free names             | Bn !Integer !Integer  -- bound names / binding level + pattern index             deriving (Eq, Ord, Typeable, Generic)++instance NFData (Name a) where+  rnf (Fn s n) = rnf s `seq` rnf n `seq` ()+  rnf (Bn i j) = rnf i `seq` rnf j `seq` ()  -- | Returns 'True' iff the given @Name a@ is free. isFreeName :: Name a -> Bool

@@ -13,6 +13,7 @@ module Unbound.Generics.LocallyNameless.Rebind where  import Control.Applicative ((<*>), (<$>))+import Control.DeepSeq (NFData(..)) import Data.Monoid ((<>)) import GHC.Generics @@ -39,6 +40,9 @@ -- @ data Rebind p1 p2 = Rebnd p1 p2                   deriving (Generic, Eq)++instance (NFData p1, NFData p2) => NFData (Rebind p1 p2) where+  rnf (Rebnd p1 p2) = rnf p1 `seq` rnf p2 `seq` ()  instance (Show p1, Show p2) => Show (Rebind p1 p2) where   showsPrec paren (Rebnd p1 p2) =

@@ -19,6 +19,7 @@        , TRec (..)        ) where +import Control.DeepSeq (NFData(..)) import GHC.Generics (Generic)  import Unbound.Generics.LocallyNameless.Alpha@@ -30,6 +31,9 @@ -- Agda's dot notation. newtype Rec p = Rec p               deriving (Generic, Eq)++instance NFData p => NFData (Rec p) where+  rnf (Rec p) = rnf p `seq` ()  instance Show a => Show (Rec a) where   showsPrec _ (Rec a) = showString "[" . showsPrec 0 a . showString "]"

@@ -12,6 +12,7 @@ module Unbound.Generics.LocallyNameless.Shift where  import Control.Applicative+import Control.DeepSeq (NFData(..)) import Data.Monoid (Monoid(..))  import Unbound.Generics.LocallyNameless.Alpha (Alpha(..),@@ -33,6 +34,9 @@   type Embedded (Shift e) = Embedded e   embedded = iso (\(Shift e) -> e) Shift . embedded   +instance NFData e => NFData (Shift e) where+  rnf (Shift e) = rnf e `seq` ()+ instance Show e => Show (Shift e) where   showsPrec _ (Shift e) = showString "{" . showsPrec 0 e . showString "}" 

@@ -2,7 +2,7 @@ -- documentation, see http://haskell.org/cabal/users-guide/  name:                unbound-generics-version:             0.1.2.1+version:             0.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@@ -53,6 +53,7 @@   -- other-extensions:       build-depends:       base >=4.6 && <5,                        template-haskell >= 2.8.0.0,+                       deepseq >= 1.3,                        mtl >= 2.1,                        transformers >= 0.3,                        transformers-compat >= 0.3,@@ -86,6 +87,19 @@   hs-source-dirs:      test   default-language:    Haskell2010   ghc-options:         -Wall++Benchmark benchmark-unbound-generics+  type:                exitcode-stdio-1.0+  default-language:    Haskell2010+  hs-source-dirs:      benchmarks+  main-is:             benchmark-main.hs+  build-depends:       base+                     , criterion+                     , deepseq >= 1.3.0.0+                     , deepseq-generics >= 0.1.1.2+                     , unbound-generics+  other-modules:       BenchLam+  ghc-options:       -Wall  source-repository head   type:                git