bound 2.0.6 → 2.0.7
raw patch · 23 files changed
+3630/−3618 lines, 23 filesdep ~deepseqdep ~hashabledep ~th-abstractionsetup-changedPVP ok
version bump matches the API change (PVP)
Dependency ranges changed: deepseq, hashable, th-abstraction
API changes (from Hackage documentation)
Files
- .gitignore +32/−32
- .vim.custom +31/−31
- AUTHORS.markdown +10/−10
- CHANGELOG.markdown +130/−126
- LICENSE +30/−30
- README.markdown +71/−71
- Setup.lhs +7/−7
- bound.cabal +158/−156
- doc/BoundLaws.hs +102/−102
- doc/LICENSE +30/−30
- doc/bound-laws.cabal +40/−38
- examples/Deriving.hs +131/−131
- examples/Imperative.hs +286/−286
- examples/Overkill.hs +344/−344
- examples/Simple.hs +183/−183
- src/Bound.hs +146/−146
- src/Bound/Class.hs +118/−118
- src/Bound/Name.hs +254/−254
- src/Bound/Scope.hs +465/−465
- src/Bound/Scope/Simple.hs +434/−434
- src/Bound/TH.hs +345/−341
- src/Bound/Term.hs +62/−62
- src/Bound/Var.hs +221/−221
.gitignore view
@@ -1,32 +1,32 @@-dist -dist-newstyle -docs -wiki -TAGS -tags -wip -.DS_Store -.*.swp -.*.swo -*.o -*.hi -*~ -*# -.stack-work/ -cabal-dev -*.chi -*.chs.h -*.dyn_o -*.dyn_hi -.hpc -.hsenv -.cabal-sandbox/ -cabal.sandbox.config -*.prof -*.aux -*.hp -*.eventlog -cabal.project.local -cabal.project.local~ -.HTF/ -.ghc.environment.* +dist+dist-newstyle+docs+wiki+TAGS+tags+wip+.DS_Store+.*.swp+.*.swo+*.o+*.hi+*~+*#+.stack-work/+cabal-dev+*.chi+*.chs.h+*.dyn_o+*.dyn_hi+.hpc+.hsenv+.cabal-sandbox/+cabal.sandbox.config+*.prof+*.aux+*.hp+*.eventlog+cabal.project.local+cabal.project.local~+.HTF/+.ghc.environment.*
.vim.custom view
@@ -1,31 +1,31 @@-" Add the following to your .vimrc to automatically load this on startup - -" if filereadable(".vim.custom") -" so .vim.custom -" endif - -function StripTrailingWhitespace() - let myline=line(".") - let mycolumn = col(".") - silent %s/ *$// - call cursor(myline, mycolumn) -endfunction - -" enable syntax highlighting -syntax on - -" search for the tags file anywhere between here and / -set tags=TAGS;/ - -" highlight tabs and trailing spaces -set listchars=tab:‗‗,trail:‗ -set list - -" f2 runs hasktags -map <F2> :exec ":!hasktags -x -c --ignore src"<CR><CR> - -" strip trailing whitespace before saving -" au BufWritePre *.hs,*.markdown silent! cal StripTrailingWhitespace() - -" rebuild hasktags after saving -au BufWritePost *.hs silent! :exec ":!hasktags -x -c --ignore src" +" Add the following to your .vimrc to automatically load this on startup++" if filereadable(".vim.custom")+" so .vim.custom+" endif++function StripTrailingWhitespace()+ let myline=line(".")+ let mycolumn = col(".")+ silent %s/ *$//+ call cursor(myline, mycolumn)+endfunction++" enable syntax highlighting+syntax on++" search for the tags file anywhere between here and /+set tags=TAGS;/++" highlight tabs and trailing spaces+set listchars=tab:‗‗,trail:‗+set list++" f2 runs hasktags+map <F2> :exec ":!hasktags -x -c --ignore src"<CR><CR>++" strip trailing whitespace before saving+" au BufWritePre *.hs,*.markdown silent! cal StripTrailingWhitespace()++" rebuild hasktags after saving+au BufWritePost *.hs silent! :exec ":!hasktags -x -c --ignore src"
AUTHORS.markdown view
@@ -1,10 +1,10 @@-Bound started as a one man project by: - -* [Edward Kmett](mailto:ekmett@gmail.com) [@ekmett](https://github.com/ekmett) - -Other contributions: - -* [Nicolas Pouillard](mailto:np@nicolaspouillard.fr) [@np](https://github.com/np) - - * Contributed the module 'Bound.Scope.Simple' as a naïve (but compatible) - version of the module 'Bound.Scope'. +Bound started as a one man project by:++* [Edward Kmett](mailto:ekmett@gmail.com) [@ekmett](https://github.com/ekmett)++Other contributions:++* [Nicolas Pouillard](mailto:np@nicolaspouillard.fr) [@np](https://github.com/np)++ * Contributed the module 'Bound.Scope.Simple' as a naïve (but compatible)+ version of the module 'Bound.Scope'.
CHANGELOG.markdown view
@@ -1,126 +1,130 @@-2.0.6 [2023.01.18] ------------------- -* Allow the examples to build with `base-4.18.*` (GHC 9.6). - -2.0.5 [2022.05.07] ------------------- -* Allow building with `transformers-0.6.*`. - -2.0.4 [2021.11.07] ------------------- -* Allow building with `template-haskell-2.18` (GHC 9.2). -* The `Bound.TH` module no longer requires the `TemplateHaskell` extension - (only `TemplateHaskellQuotes`) when building with GHC 9.0 or later. -* Drop support for pre-8.0 versions of GHC. - -2.0.3 [2021.02.05] ------------------- -* Allow the examples to build with `vector-0.12.2` or later. -* The build-type has been changed from `Custom` to `Simple`. - To achieve this, the `doctests` test suite has been removed in favor of using [`cabal-docspec`](https://github.com/phadej/cabal-extras/tree/master/cabal-docspec) to run the doctests. - -2.0.2 [2020.10.01] ------------------- -* Allow building with GHC 9.0. - -2.0.1 ------ -* Add `abstractEither` and `instantiateEither` to `Bound.Scope`, and - add `abstractEitherName` and `instantiateEitherName` to `Bound.Scope.Name` -* Add `Generic(1)` instances for `Name` and `Scope` -* Support `doctest-0.12` - -2 -- -* GHC 8.0 and 8.2 support -* Converted from `prelude-extras` to `transformers` + `transformers-compat` for the `Eq1`, `Ord1`, `Show1`, and `Read1` functionality. -* `makeBound` supports `Functor` components -* Add `MFunctor` instance for `Scope` -* Add `NFData` instances for `Name`, `Scope`, and `Var` -* Revamp `Setup.hs` to use `cabal-doctest`. This makes it build - with `Cabal-1.25`, and makes the `doctest`s work with `cabal new-build` and - sandboxes. - -1.0.7 ------- -* Added an `-f-template-haskell` option to allow disabling `template-haskell` support. This is an unsupported configuration but may be useful for expert users in sandbox configurations. -* Support `cereal` 0.5 - -1.0.6 ------ -* Compiles warning-free on GHC 7.10 - -1.0.5 ------ -* Widened version bound on `bifunctors`. -* Widened version bound on `profunctors`. - -1.0.4 ------ -* Widened version bound on `transformers`. - -1.0.3 ------ -* Added `bitransverseScope`. - -1.0.2 ------ -* Removed unneccesary constraint on `hoistScope`. - -1.0.1 ------ -* Added a monomorphic `hoistScope` for `Bound.Scope.Simple` - -1.0 ---- -* Added instances for `Bound` for all of the `mtl` monads. -* Added `Data` and `Typeable` support to both versions of `Scope` -* Added the missing `Applictive` instance to `Bound.Scope.Simple` -* Moved `hoistScope`, `bitraverseScope`, `transverseScope`, and `instantiateVars` here from the `ermine` compiler. - -0.9.1.1 -------- -* Updated to work with `bifunctors` 4.0 - -0.9.1 ------ -* Updated to work with `comonad` 4.0 and `profunctors` 4.0 - -0.9 ---- -* Added the missing instance for `Applicative (Scope b f)` - -0.8.1 ------ -* SafeHaskell support - -0.8 ---- -* Added `Serial`, `Binary` and `Serialize` instances for `Scope`. - -0.7 ---- -* Added `Hashable`, `Hashable1` and `Hashable2` instances where appropriate for `Name`, `Var` and `Scope`. - -0.6.1 ------ -* More aggressive inlining -* Added `unvar`, `_B`, `_F` to `Bound.Var`. -* Added `_Name` to `Bound.Name`. - -0.6 ---- -* Support for `prelude-extras` 0.3 - -0.5.1 ------ -* Removed my personal inter-package dependency upper bounds -* Updated doctest suite to use exact versions. - -0.5 ---- -* Created a `doctest`-based test suite -* Added many examples -* 100% haddock coverage -* Added the `Name` `Comonad`, to help retain names for bound variables. -* Bumped dependencies +2.0.7 [2023.08.06]+------------------+* Support building with `template-haskell-2.21.*` (GHC 9.8).++2.0.6 [2023.01.18]+------------------+* Allow the examples to build with `base-4.18.*` (GHC 9.6).++2.0.5 [2022.05.07]+------------------+* Allow building with `transformers-0.6.*`.++2.0.4 [2021.11.07]+------------------+* Allow building with `template-haskell-2.18` (GHC 9.2).+* The `Bound.TH` module no longer requires the `TemplateHaskell` extension+ (only `TemplateHaskellQuotes`) when building with GHC 9.0 or later.+* Drop support for pre-8.0 versions of GHC.++2.0.3 [2021.02.05]+------------------+* Allow the examples to build with `vector-0.12.2` or later.+* The build-type has been changed from `Custom` to `Simple`.+ To achieve this, the `doctests` test suite has been removed in favor of using [`cabal-docspec`](https://github.com/phadej/cabal-extras/tree/master/cabal-docspec) to run the doctests.++2.0.2 [2020.10.01]+------------------+* Allow building with GHC 9.0.++2.0.1+-----+* Add `abstractEither` and `instantiateEither` to `Bound.Scope`, and+ add `abstractEitherName` and `instantiateEitherName` to `Bound.Scope.Name`+* Add `Generic(1)` instances for `Name` and `Scope`+* Support `doctest-0.12`++2+-+* GHC 8.0 and 8.2 support+* Converted from `prelude-extras` to `transformers` + `transformers-compat` for the `Eq1`, `Ord1`, `Show1`, and `Read1` functionality.+* `makeBound` supports `Functor` components+* Add `MFunctor` instance for `Scope`+* Add `NFData` instances for `Name`, `Scope`, and `Var`+* Revamp `Setup.hs` to use `cabal-doctest`. This makes it build+ with `Cabal-1.25`, and makes the `doctest`s work with `cabal new-build` and+ sandboxes.++1.0.7+------+* Added an `-f-template-haskell` option to allow disabling `template-haskell` support. This is an unsupported configuration but may be useful for expert users in sandbox configurations.+* Support `cereal` 0.5++1.0.6+-----+* Compiles warning-free on GHC 7.10++1.0.5+-----+* Widened version bound on `bifunctors`.+* Widened version bound on `profunctors`.++1.0.4+-----+* Widened version bound on `transformers`.++1.0.3+-----+* Added `bitransverseScope`.++1.0.2+-----+* Removed unneccesary constraint on `hoistScope`.++1.0.1+-----+* Added a monomorphic `hoistScope` for `Bound.Scope.Simple`++1.0+---+* Added instances for `Bound` for all of the `mtl` monads.+* Added `Data` and `Typeable` support to both versions of `Scope`+* Added the missing `Applictive` instance to `Bound.Scope.Simple`+* Moved `hoistScope`, `bitraverseScope`, `transverseScope`, and `instantiateVars` here from the `ermine` compiler.++0.9.1.1+-------+* Updated to work with `bifunctors` 4.0++0.9.1+-----+* Updated to work with `comonad` 4.0 and `profunctors` 4.0++0.9+---+* Added the missing instance for `Applicative (Scope b f)`++0.8.1+-----+* SafeHaskell support++0.8+---+* Added `Serial`, `Binary` and `Serialize` instances for `Scope`.++0.7+---+* Added `Hashable`, `Hashable1` and `Hashable2` instances where appropriate for `Name`, `Var` and `Scope`.++0.6.1+-----+* More aggressive inlining+* Added `unvar`, `_B`, `_F` to `Bound.Var`.+* Added `_Name` to `Bound.Name`.++0.6+---+* Support for `prelude-extras` 0.3++0.5.1+-----+* Removed my personal inter-package dependency upper bounds+* Updated doctest suite to use exact versions.++0.5+---+* Created a `doctest`-based test suite+* Added many examples+* 100% haddock coverage+* Added the `Name` `Comonad`, to help retain names for bound variables.+* Bumped dependencies
LICENSE view
@@ -1,30 +1,30 @@-Copyright 2012 Edward Kmett - -All rights reserved. - -Redistribution and use in source and binary forms, with or without -modification, are permitted provided that the following conditions -are met: - -1. Redistributions of source code must retain the above copyright - notice, this list of conditions and the following disclaimer. - -2. Redistributions in binary form must reproduce the above copyright - notice, this list of conditions and the following disclaimer in the - documentation and/or other materials provided with the distribution. - -3. Neither the name of the author nor the names of his contributors - may be used to endorse or promote products derived from this software - without specific prior written permission. - -THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND ANY EXPRESS OR -IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED -WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE -DISCLAIMED. IN NO EVENT SHALL THE AUTHORS OR CONTRIBUTORS BE LIABLE FOR -ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL -DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS -OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) -HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, -STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN -ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE -POSSIBILITY OF SUCH DAMAGE. +Copyright 2012 Edward Kmett++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions+are met:++1. Redistributions of source code must retain the above copyright+ notice, this list of conditions and the following disclaimer.++2. Redistributions in binary form must reproduce the above copyright+ notice, this list of conditions and the following disclaimer in the+ documentation and/or other materials provided with the distribution.++3. Neither the name of the author nor the names of his contributors+ may be used to endorse or promote products derived from this software+ without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND ANY EXPRESS OR+IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED+WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE+DISCLAIMED. IN NO EVENT SHALL THE AUTHORS OR CONTRIBUTORS BE LIABLE FOR+ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL+DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS+OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION)+HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT,+STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN+ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE+POSSIBILITY OF SUCH DAMAGE.
README.markdown view
@@ -1,71 +1,71 @@-Bound -===== - -[](https://hackage.haskell.org/package/bound) [](https://github.com/ekmett/bound/actions?query=workflow%3AHaskell-CI) - -Goals ------ - -This library provides convenient combinators for working with "locally-nameless" terms. These can be useful -when writing a type checker, evaluator, parser, or pretty printer for terms that contain binders like forall -or lambda, as they ease the task of avoiding variable capture and testing for alpha-equivalence. - -See [the documentation](http://hackage.haskell.org/package/bound) on hackage for more information, but here is an example: - -```haskell -{-# LANGUAGE DeriveFunctor #-} -{-# LANGUAGE DeriveFoldable #-} -{-# LANGUAGE DeriveTraversable #-} -{-# LANGUAGE TemplateHaskell #-} - -import Bound -import Control.Applicative -import Control.Monad -import Data.Functor.Classes -import Data.Foldable -import Data.Traversable -import Data.Eq.Deriving (deriveEq1) -- these two are from the -import Text.Show.Deriving (deriveShow1) -- deriving-compat package - -infixl 9 :@ -data Exp a = V a | Exp a :@ Exp a | Lam (Scope () Exp a) - deriving (Eq,Show,Functor,Foldable,Traversable) - -instance Applicative Exp where pure = V; (<*>) = ap - -instance Monad Exp where - return = V - V a >>= f = f a - (x :@ y) >>= f = (x >>= f) :@ (y >>= f) - Lam e >>= f = Lam (e >>>= f) - -lam :: Eq a => a -> Exp a -> Exp a -lam v b = Lam (abstract1 v b) - -whnf :: Exp a -> Exp a -whnf (f :@ a) = case whnf f of - Lam b -> whnf (instantiate1 a b) - f' -> f' :@ a -whnf e = e - -deriveEq1 ''Exp -deriveShow1 ''Exp - -main :: IO () -main = do - let term = lam 'x' (V 'x') :@ V 'y' - print term -- Lam (Scope (V (B ()))) :@ V 'y' - print $ whnf term -- V 'y' -``` - - There are longer examples in the [examples/ folder](https://github.com/ekmett/bound/tree/master/examples). - -Contact Information -------------------- - -Contributions and bug reports are welcome! - -Please feel free to contact me through github or on the #haskell IRC channel on irc.freenode.net. - --Edward Kmett - +Bound+=====++[](https://hackage.haskell.org/package/bound) [](https://github.com/ekmett/bound/actions?query=workflow%3AHaskell-CI)++Goals+-----++This library provides convenient combinators for working with "locally-nameless" terms. These can be useful+when writing a type checker, evaluator, parser, or pretty printer for terms that contain binders like forall+or lambda, as they ease the task of avoiding variable capture and testing for alpha-equivalence.++See [the documentation](http://hackage.haskell.org/package/bound) on hackage for more information, but here is an example:++```haskell+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE DeriveFoldable #-}+{-# LANGUAGE DeriveTraversable #-}+{-# LANGUAGE TemplateHaskell #-}++import Bound+import Control.Applicative+import Control.Monad+import Data.Functor.Classes+import Data.Foldable+import Data.Traversable+import Data.Eq.Deriving (deriveEq1) -- these two are from the+import Text.Show.Deriving (deriveShow1) -- deriving-compat package++infixl 9 :@+data Exp a = V a | Exp a :@ Exp a | Lam (Scope () Exp a)+ deriving (Eq,Show,Functor,Foldable,Traversable)++instance Applicative Exp where pure = V; (<*>) = ap++instance Monad Exp where+ return = V+ V a >>= f = f a+ (x :@ y) >>= f = (x >>= f) :@ (y >>= f)+ Lam e >>= f = Lam (e >>>= f)++lam :: Eq a => a -> Exp a -> Exp a+lam v b = Lam (abstract1 v b)++whnf :: Exp a -> Exp a+whnf (f :@ a) = case whnf f of+ Lam b -> whnf (instantiate1 a b)+ f' -> f' :@ a+whnf e = e++deriveEq1 ''Exp+deriveShow1 ''Exp++main :: IO ()+main = do+ let term = lam 'x' (V 'x') :@ V 'y'+ print term -- Lam (Scope (V (B ()))) :@ V 'y'+ print $ whnf term -- V 'y'+```++ There are longer examples in the [examples/ folder](https://github.com/ekmett/bound/tree/master/examples).++Contact Information+-------------------++Contributions and bug reports are welcome!++Please feel free to contact me through github or on the #haskell IRC channel on irc.freenode.net.++-Edward Kmett+
Setup.lhs view
@@ -1,7 +1,7 @@-#!/usr/bin/runhaskell -> module Main (main) where - -> import Distribution.Simple - -> main :: IO () -> main = defaultMain +#!/usr/bin/runhaskell+> module Main (main) where++> import Distribution.Simple++> main :: IO ()+> main = defaultMain
bound.cabal view
@@ -1,156 +1,158 @@-name: bound -category: Language, Compilers/Interpreters -version: 2.0.6 -license: BSD3 -cabal-version: >= 1.10 -license-file: LICENSE -author: Edward A. Kmett -maintainer: Edward A. Kmett <ekmett@gmail.com> -stability: experimental -homepage: http://github.com/ekmett/bound/ -bug-reports: http://github.com/ekmett/bound/issues -copyright: Copyright (C) 2012-2013 Edward A. Kmett -synopsis: Making de Bruijn Succ Less -build-type: Simple -description: - We represent the target language itself as an ideal monad supplied by the - user, and provide a 'Scope' monad transformer for introducing bound variables - in user supplied terms. Users supply a 'Monad' and 'Traversable' instance, - and we traverse to find free variables, and use the Monad to perform - substitution that avoids bound variables. - . - Slides describing and motivating this approach to name binding are available - online at: - . - <http://www.slideshare.net/ekmett/bound-making-de-bruijn-succ-less> - . - The goal of this package is to make it as easy as possible to deal with name - binding without forcing an awkward monadic style on the user. - . - With generalized de Bruijn term you can 'lift' whole trees instead of just - applying 'succ' to individual variables, weakening the all variables bound - by a scope and greatly speeding up instantiation. By giving binders more - structure we permit easy simultaneous substitution and further speed up - instantiation. - -extra-source-files: - .gitignore - .vim.custom - doc/*.hs - doc/bound-laws.cabal - doc/LICENSE - README.markdown - CHANGELOG.markdown - AUTHORS.markdown - -tested-with: - GHC==8.0.2, - GHC==8.2.2, - GHC==8.4.4, - GHC==8.6.5, - GHC==8.8.4, - GHC==8.10.7, - GHC==9.0.1, - GHC==9.2.1 - -flag template-haskell - description: - You can disable the use of the `template-haskell` package using `-f-template-haskell`. - . - Disabling this is an unsupported configuration, but it may be useful for accelerating builds in sandboxes for expert users. - default: True - manual: True - -source-repository head - type: git - location: git://github.com/ekmett/bound.git - -library - hs-source-dirs: src - - exposed-modules: - Bound - Bound.Class - Bound.Name - Bound.Scope - Bound.Scope.Simple - Bound.Term - Bound.TH - Bound.Var - - build-depends: - base >= 4.9 && < 5, - bifunctors >= 5 && < 6, - binary >= 0.8.3 && < 0.9, - bytes >= 0.15.2 && < 1, - cereal >= 0.4.1 && < 0.6, - comonad >= 5 && < 6, - hashable >= 1.2.5.0 && < 1.5, - mmorph >= 1.0 && < 1.3, - deepseq >= 1.4.2 && < 1.5, - profunctors >= 3.3 && < 6, - th-abstraction >= 0.4 && < 0.5, - transformers >= 0.5 && < 0.7, - transformers-compat >= 0.5 && < 1 - - ghc-options: -Wall -O2 -fspec-constr -fdicts-cheap -funbox-strict-fields - - default-language: Haskell2010 - - if flag(template-haskell) && impl(ghc) - build-depends: template-haskell >= 2.11.1 && < 3.0 - -test-suite Simple - type: exitcode-stdio-1.0 - main-is: Simple.hs - hs-source-dirs: examples - buildable: True - - ghc-options: -Wall -threaded - default-language: Haskell2010 - build-depends: - base >= 4.5 && < 5, - bound, - deriving-compat >= 0.3.4 && < 0.7, - transformers, - transformers-compat - -test-suite Overkill - type: exitcode-stdio-1.0 - main-is: Overkill.hs - hs-source-dirs: examples - ghc-options: -Wall -threaded - default-language: Haskell2010 - build-depends: - base >= 4.5 && < 5, - bound, - transformers, - transformers-compat, - vector >= 0.12 - if !impl(ghc >= 7.8) - buildable: False - -test-suite Deriving - type: exitcode-stdio-1.0 - main-is: Deriving.hs - hs-source-dirs: examples - ghc-options: -Wall -threaded - default-language: Haskell2010 - build-depends: - base >= 4.5 && < 5, - bound, - transformers, - transformers-compat - -test-suite Imperative - type: exitcode-stdio-1.0 - main-is: Imperative.hs - hs-source-dirs: examples - ghc-options: -Wall -threaded - default-language: Haskell2010 - build-depends: - base >= 4.5 && < 5, - bound, - transformers, - transformers-compat, - void +name: bound+category: Language, Compilers/Interpreters+version: 2.0.7+license: BSD3+cabal-version: >= 1.10+license-file: LICENSE+author: Edward A. Kmett+maintainer: Edward A. Kmett <ekmett@gmail.com>+stability: experimental+homepage: http://github.com/ekmett/bound/+bug-reports: http://github.com/ekmett/bound/issues+copyright: Copyright (C) 2012-2013 Edward A. Kmett+synopsis: Making de Bruijn Succ Less+build-type: Simple+description:+ We represent the target language itself as an ideal monad supplied by the+ user, and provide a 'Scope' monad transformer for introducing bound variables+ in user supplied terms. Users supply a 'Monad' and 'Traversable' instance,+ and we traverse to find free variables, and use the Monad to perform+ substitution that avoids bound variables.+ .+ Slides describing and motivating this approach to name binding are available+ online at:+ .+ <http://www.slideshare.net/ekmett/bound-making-de-bruijn-succ-less>+ .+ The goal of this package is to make it as easy as possible to deal with name+ binding without forcing an awkward monadic style on the user.+ .+ With generalized de Bruijn term you can 'lift' whole trees instead of just+ applying 'succ' to individual variables, weakening the all variables bound+ by a scope and greatly speeding up instantiation. By giving binders more+ structure we permit easy simultaneous substitution and further speed up+ instantiation.++extra-source-files:+ .gitignore+ .vim.custom+ doc/*.hs+ doc/bound-laws.cabal+ doc/LICENSE+ README.markdown+ CHANGELOG.markdown+ AUTHORS.markdown++tested-with:+ GHC==8.0.2,+ GHC==8.2.2,+ GHC==8.4.4,+ GHC==8.6.5,+ GHC==8.8.4,+ GHC==8.10.7,+ GHC==9.0.2,+ GHC==9.2.8,+ GHC==9.4.5,+ GHC==9.6.2++flag template-haskell+ description:+ You can disable the use of the `template-haskell` package using `-f-template-haskell`.+ .+ Disabling this is an unsupported configuration, but it may be useful for accelerating builds in sandboxes for expert users.+ default: True+ manual: True++source-repository head+ type: git+ location: git://github.com/ekmett/bound.git++library+ hs-source-dirs: src++ exposed-modules:+ Bound+ Bound.Class+ Bound.Name+ Bound.Scope+ Bound.Scope.Simple+ Bound.Term+ Bound.TH+ Bound.Var++ build-depends:+ base >= 4.9 && < 5,+ bifunctors >= 5 && < 6,+ binary >= 0.8.3 && < 0.9,+ bytes >= 0.15.2 && < 1,+ cereal >= 0.4.1 && < 0.6,+ comonad >= 5 && < 6,+ hashable >= 1.2.5.0 && < 1.5,+ mmorph >= 1.0 && < 1.3,+ deepseq >= 1.4.2 && < 1.6,+ profunctors >= 3.3 && < 6,+ th-abstraction >= 0.4 && < 0.7,+ transformers >= 0.5 && < 0.7,+ transformers-compat >= 0.5 && < 1++ ghc-options: -Wall -O2 -fspec-constr -fdicts-cheap -funbox-strict-fields++ default-language: Haskell2010++ if flag(template-haskell) && impl(ghc)+ build-depends: template-haskell >= 2.11.1 && < 3.0++test-suite Simple+ type: exitcode-stdio-1.0+ main-is: Simple.hs+ hs-source-dirs: examples+ buildable: True++ ghc-options: -Wall -threaded+ default-language: Haskell2010+ build-depends:+ base >= 4.5 && < 5,+ bound,+ deriving-compat >= 0.3.4 && < 0.7,+ transformers,+ transformers-compat++test-suite Overkill+ type: exitcode-stdio-1.0+ main-is: Overkill.hs+ hs-source-dirs: examples+ ghc-options: -Wall -threaded+ default-language: Haskell2010+ build-depends:+ base >= 4.5 && < 5,+ bound,+ transformers,+ transformers-compat,+ vector >= 0.12+ if !impl(ghc >= 7.8)+ buildable: False++test-suite Deriving+ type: exitcode-stdio-1.0+ main-is: Deriving.hs+ hs-source-dirs: examples+ ghc-options: -Wall -threaded+ default-language: Haskell2010+ build-depends:+ base >= 4.5 && < 5,+ bound,+ transformers,+ transformers-compat++test-suite Imperative+ type: exitcode-stdio-1.0+ main-is: Imperative.hs+ hs-source-dirs: examples+ ghc-options: -Wall -threaded+ default-language: Haskell2010+ build-depends:+ base >= 4.5 && < 5,+ bound,+ transformers,+ transformers-compat,+ void
doc/BoundLaws.hs view
@@ -1,102 +1,102 @@-{-# LANGUAGE CPP #-} -{-# LANGUAGE KindSignatures #-} -module BoundLaws where - -import Bound.Class -import Control.Monad -import Data.Kind - -{- - -What laws should Bound have? - -We need at least enough to make sure the typical Monad Exp instances are valid. - -Let's start by writing some generic Bound instances. - --} - -newtype Const x (m :: Type -> Type) a = Const x - -instance Bound (Const x) where - Const x >>>= _ = Const x - - -newtype Identity (m :: Type -> Type) a = Id (m a) - -instance Bound Identity where - Id ma >>>= f = Id (ma >>= f) - - -data Product f g (m :: Type -> Type) a = f m a :*: g m a - -instance (Bound f, Bound g) => Bound (Product f g) where - (fma :*: gma) >>>= f = (fma >>>= f) :*: (gma >>>= f) - - -data Sum f g (m :: Type -> Type) a = Inl (f m a) | Inr (g m a) - -instance (Bound f, Bound g) => Bound (Sum f g) where - Inl fma >>>= f = Inl (fma >>>= f) - Inr gma >>>= f = Inr (gma >>>= f) - - -{- - -Now we can actually write the typical Monad Exp instance generically -(for theory, not practice), since sums and products and all of the -above is plenty enough to specify an AST. - --} - -data Exp (f :: (Type -> Type) -> Type -> Type) a = Var a | Branch (f (Exp f) a) - -instance Bound f => Functor (Exp f) where - fmap = liftM - -instance Bound f => Applicative (Exp f) where - pure = Var - (<*>) = ap - -instance Bound f => Monad (Exp f) where -#if !(MIN_VERSION_base(4,11,0)) - return = Var -#endif - Var a >>= f = f a - Branch fE >>= f = Branch (fE >>>= f) - -{- - -Is this valid? Let's go to Agda and try to prove the Monad laws. - - - left-return : ∀ {A B} (x : A)(f : A -> Exp F B) -> (return x >>= f) ≡ f x - left-return x f = refl - - right-return : ∀ {A}(m : Exp F A) -> (m >>= return) ≡ m - right-return (Var x) = refl - right-return (Branch m) = cong Branch {!!}0 - - assoc : ∀ {A B C} (m : Exp F A) (k : A -> Exp F B) (h : B -> Exp F C) -> (m >>= (\ x -> k x >>= h)) ≡ ((m >>= k) >>= h) - assoc (Var x) k h = refl - assoc (Branch m) k h = cong Branch {!!}1 - - -So the first one is fine, but we have two holes: - - ?0 : m >>>= return ≡ m - ?1 : m >>>= (λ x → k x >>= h) ≡ (m >>>= k) >>>= h - -But all of the instances above respect these laws, and they are implied by -the current law for monad transformers, we could just make them the -Bound class laws. - -Btw these laws correspond to requiring (f m) to be an m-left module for every m [1], -so we'd also get a law-abiding fmap for (f m). - - -Bonus: composing pointwise (\m a -> f m (g m a)) would also create a valid Bound - - -[1] Modules over Monads and Initial Semantics - http://web.math.unifi.it/users/maggesi/syn.pdf --} +{-# LANGUAGE CPP #-}+{-# LANGUAGE KindSignatures #-}+module BoundLaws where++import Bound.Class+import Control.Monad+import Data.Kind++{-++What laws should Bound have?++We need at least enough to make sure the typical Monad Exp instances are valid.++Let's start by writing some generic Bound instances.++-}++newtype Const x (m :: Type -> Type) a = Const x++instance Bound (Const x) where+ Const x >>>= _ = Const x+++newtype Identity (m :: Type -> Type) a = Id (m a)++instance Bound Identity where+ Id ma >>>= f = Id (ma >>= f)+++data Product f g (m :: Type -> Type) a = f m a :*: g m a++instance (Bound f, Bound g) => Bound (Product f g) where+ (fma :*: gma) >>>= f = (fma >>>= f) :*: (gma >>>= f)+++data Sum f g (m :: Type -> Type) a = Inl (f m a) | Inr (g m a)++instance (Bound f, Bound g) => Bound (Sum f g) where+ Inl fma >>>= f = Inl (fma >>>= f)+ Inr gma >>>= f = Inr (gma >>>= f)+++{-++Now we can actually write the typical Monad Exp instance generically+(for theory, not practice), since sums and products and all of the+above is plenty enough to specify an AST.++-}++data Exp (f :: (Type -> Type) -> Type -> Type) a = Var a | Branch (f (Exp f) a)++instance Bound f => Functor (Exp f) where+ fmap = liftM++instance Bound f => Applicative (Exp f) where+ pure = Var+ (<*>) = ap++instance Bound f => Monad (Exp f) where+#if !(MIN_VERSION_base(4,11,0))+ return = Var+#endif+ Var a >>= f = f a+ Branch fE >>= f = Branch (fE >>>= f)++{-++Is this valid? Let's go to Agda and try to prove the Monad laws.+++ left-return : ∀ {A B} (x : A)(f : A -> Exp F B) -> (return x >>= f) ≡ f x+ left-return x f = refl++ right-return : ∀ {A}(m : Exp F A) -> (m >>= return) ≡ m+ right-return (Var x) = refl+ right-return (Branch m) = cong Branch {!!}0++ assoc : ∀ {A B C} (m : Exp F A) (k : A -> Exp F B) (h : B -> Exp F C) -> (m >>= (\ x -> k x >>= h)) ≡ ((m >>= k) >>= h)+ assoc (Var x) k h = refl+ assoc (Branch m) k h = cong Branch {!!}1+++So the first one is fine, but we have two holes:++ ?0 : m >>>= return ≡ m+ ?1 : m >>>= (λ x → k x >>= h) ≡ (m >>>= k) >>>= h++But all of the instances above respect these laws, and they are implied by+the current law for monad transformers, we could just make them the+Bound class laws.++Btw these laws correspond to requiring (f m) to be an m-left module for every m [1],+so we'd also get a law-abiding fmap for (f m).+++Bonus: composing pointwise (\m a -> f m (g m a)) would also create a valid Bound+++[1] Modules over Monads and Initial Semantics - http://web.math.unifi.it/users/maggesi/syn.pdf+-}
doc/LICENSE view
@@ -1,30 +1,30 @@-Copyright 2012 Edward Kmett - -All rights reserved. - -Redistribution and use in source and binary forms, with or without -modification, are permitted provided that the following conditions -are met: - -1. Redistributions of source code must retain the above copyright - notice, this list of conditions and the following disclaimer. - -2. Redistributions in binary form must reproduce the above copyright - notice, this list of conditions and the following disclaimer in the - documentation and/or other materials provided with the distribution. - -3. Neither the name of the author nor the names of his contributors - may be used to endorse or promote products derived from this software - without specific prior written permission. - -THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND ANY EXPRESS OR -IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED -WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE -DISCLAIMED. IN NO EVENT SHALL THE AUTHORS OR CONTRIBUTORS BE LIABLE FOR -ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL -DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS -OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) -HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, -STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN -ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE -POSSIBILITY OF SUCH DAMAGE. +Copyright 2012 Edward Kmett++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions+are met:++1. Redistributions of source code must retain the above copyright+ notice, this list of conditions and the following disclaimer.++2. Redistributions in binary form must reproduce the above copyright+ notice, this list of conditions and the following disclaimer in the+ documentation and/or other materials provided with the distribution.++3. Neither the name of the author nor the names of his contributors+ may be used to endorse or promote products derived from this software+ without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND ANY EXPRESS OR+IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED+WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE+DISCLAIMED. IN NO EVENT SHALL THE AUTHORS OR CONTRIBUTORS BE LIABLE FOR+ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL+DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS+OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION)+HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT,+STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN+ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE+POSSIBILITY OF SUCH DAMAGE.
doc/bound-laws.cabal view
@@ -1,38 +1,40 @@-name: bound-laws -category: Language, Compilers/Interpreters -version: 0.1 -license: BSD3 -cabal-version: >= 1.10 -license-file: LICENSE -author: Edward A. Kmett -maintainer: Edward A. Kmett <ekmett@gmail.com> -stability: experimental -homepage: http://github.com/ekmett/bound/ -bug-reports: http://github.com/ekmett/bound/issues -copyright: Copyright (C) 2012-2013 Edward A. Kmett -synopsis: Making de Bruijn Succ Less -build-type: Simple -description: Some laws for the @Bound@ class - -tested-with: - GHC==8.0.2, - GHC==8.2.2, - GHC==8.4.4, - GHC==8.6.5, - GHC==8.8.4, - GHC==8.10.7, - GHC==9.0.1, - GHC==9.2.1 - -source-repository head - type: git - location: git://github.com/ekmett/bound.git - -library - exposed-modules: BoundLaws - hs-source-dirs: . - ghc-options: -Wall - default-language: Haskell2010 - build-depends: - base >= 4.9 && < 5, - bound +name: bound-laws+category: Language, Compilers/Interpreters+version: 0.1+license: BSD3+cabal-version: >= 1.10+license-file: LICENSE+author: Edward A. Kmett+maintainer: Edward A. Kmett <ekmett@gmail.com>+stability: experimental+homepage: http://github.com/ekmett/bound/+bug-reports: http://github.com/ekmett/bound/issues+copyright: Copyright (C) 2012-2013 Edward A. Kmett+synopsis: Making de Bruijn Succ Less+build-type: Simple+description: Some laws for the @Bound@ class++tested-with:+ GHC==8.0.2,+ GHC==8.2.2,+ GHC==8.4.4,+ GHC==8.6.5,+ GHC==8.8.4,+ GHC==8.10.7,+ GHC==9.0.2,+ GHC==9.2.8,+ GHC==9.4.5,+ GHC==9.6.2++source-repository head+ type: git+ location: git://github.com/ekmett/bound.git++library+ exposed-modules: BoundLaws+ hs-source-dirs: .+ ghc-options: -Wall+ default-language: Haskell2010+ build-depends:+ base >= 4.9 && < 5,+ bound
examples/Deriving.hs view
@@ -1,131 +1,131 @@-{-# LANGUAGE CPP, DeriveFunctor, DeriveFoldable, DeriveTraversable #-} -module Main where - -import qualified Data.List as L -import Control.Monad -import Data.Functor.Classes -import Bound - -infixl 9 :@ - -data Exp a - = V a - | Exp a :@ Exp a - | Lam {-# UNPACK #-} !Int (Pat Exp a) (Scope Int Exp a) - | Let {-# UNPACK #-} !Int [Scope Int Exp a] (Scope Int Exp a) - | Case (Exp a) [Alt Exp a] - deriving (Eq,Functor,Foldable,Traversable) - -instance Applicative Exp where - pure = V - (<*>) = ap - -instance Monad Exp where -#if !(MIN_VERSION_base(4,11,0)) - return = V -#endif - V a >>= f = f a - (x :@ y) >>= f = (x >>= f) :@ (y >>= f) - Lam n p e >>= f = Lam n (p >>>= f) (e >>>= f) - Let n bs e >>= f = Let n (map (>>>= f) bs) (e >>>= f) - Case e as >>= f = Case (e >>= f) (map (>>>= f) as) - -instance Eq1 Exp where - liftEq eq (V a) (V b) = eq a b - liftEq eq (a :@ a') (b :@ b') = liftEq eq a b && liftEq eq a' b' - liftEq eq (Lam n p e) (Lam n' p' e') = n == n' && liftEq eq p p' && liftEq eq e e' - liftEq eq (Let n bs e) (Let n' bs' e') = n == n' && liftEq (liftEq eq) bs bs' && liftEq eq e e' - liftEq eq (Case e as) (Case e' as') = liftEq eq e e' && liftEq (liftEq eq) as as' - liftEq _ _ _ = False --- And "similarly" for Ord1, Show1 and Read1 - -data Pat f a - = VarP - | WildP - | AsP (Pat f a) - | ConP String [Pat f a] - | ViewP (Scope Int f a) (Pat f a) - deriving (Eq,Ord,Show,Read,Functor,Foldable,Traversable) - -instance (Eq1 f, Monad f) => Eq1 (Pat f) where - liftEq _ VarP VarP = True - liftEq _ WildP WildP = True - liftEq eq (AsP p) (AsP p') = liftEq eq p p' - liftEq eq (ConP g ps) (ConP g' ps') = g == g' && liftEq (liftEq eq) ps ps' - liftEq eq (ViewP e p) (ViewP e' p') = liftEq eq e e' && liftEq eq p p' - liftEq _ _ _ = False - -instance Bound Pat where - VarP >>>= _ = VarP - WildP >>>= _ = WildP - AsP p >>>= f = AsP (p >>>= f) - ConP g ps >>>= f = ConP g (map (>>>= f) ps) - ViewP e p >>>= f = ViewP (e >>>= f) (p >>>= f) - -data Alt f a = Alt {-# UNPACK #-} !Int (Pat f a) (Scope Int f a) - deriving (Eq,Functor,Foldable,Traversable) - -instance (Eq1 f, Monad f) => Eq1 (Alt f) where - liftEq eq (Alt n p b) (Alt n' p' b') = - n == n' && liftEq eq p p' && liftEq eq b b' - -instance Bound Alt where - Alt n p b >>>= f = Alt n (p >>>= f) (b >>>= f) - --- ** smart patterns - -data P a = P { pattern :: [a] -> Pat Exp a, bindings :: [a] } - --- | --- >>> lam (varp "x") (V "x") --- Lam 1 VarP (Scope (V (B 0))) -varp :: a -> P a -varp a = P (const VarP) [a] - -wildp :: P a -wildp = P (const WildP) [] - -asp :: a -> P a -> P a -asp a (P p as) = P (\bs -> AsP (p (a:bs))) (a:as) - --- | --- >>> lam (conp "Hello" [varp "x", wildp]) (V "y") --- Lam 1 (ConP "Hello" [VarP,WildP]) (Scope (V (F (V "y")))) -conp :: String -> [P a] -> P a -conp g ps = P (ConP g . go ps) (ps >>= bindings) - where - go (P p as:ps') bs = p bs : go ps' (bs ++ as) - go [] _ = [] - --- | view patterns can view variables that are bound earlier than them in the pattern -viewp :: Eq a => Exp a -> P a -> P a -viewp t (P p as) = P (\bs -> ViewP (abstract (`L.elemIndex` bs) t) (p bs)) as - --- | smart lam constructor --- --- >>> let_ [("x",V "y"),("y",V "x" :@ V "y")] $ lam (varp "z") (V "z" :@ V "y") --- Let 2 [Scope (V (B 1)),Scope (V (B 0) :@ V (B 1))] (Scope (Lam 1 VarP (Scope (V (B 0) :@ V (F (V (B 1))))))) --- --- >>> lam (conp "F" [varp "x", viewp (V "x") $ varp "y"]) (V "y") --- Lam 2 (ConP "F" [VarP,ViewP (Scope (V (B 0))) VarP]) (Scope (V (B 1))) --- --- >>> lam (conp "F" [varp "x", viewp (V "y") $ varp "y"]) (V "y") --- Lam 2 (ConP "F" [VarP,ViewP (Scope (V (F (V "y")))) VarP]) (Scope (V (B 1))) -lam :: Eq a => P a -> Exp a -> Exp a -lam (P p as) t = Lam (length as) (p []) (abstract (`L.elemIndex` as) t) - --- | smart let constructor -let_ :: Eq a => [(a, Exp a)] -> Exp a -> Exp a -let_ bs b = Let (length bs) (map (abstr . snd) bs) (abstr b) - where vs = map fst bs - abstr = abstract (`L.elemIndex` vs) - --- | smart alt constructor --- --- >>> lam (varp "x") $ Case (V "x") [alt (conp "Hello" [varp "z",wildp]) (V "x"), alt (varp "y") (V "y")] --- Lam 1 VarP (Scope (Case (V (B 0)) [Alt 1 (ConP "Hello" [VarP,WildP]) (Scope (V (F (V (B 0))))),Alt 1 VarP (Scope (V (B 0)))])) -alt :: Eq a => P a -> Exp a -> Alt Exp a -alt (P p as) t = Alt (length as) (p []) (abstract (`L.elemIndex` as) t) - -main :: IO () -main = return () +{-# LANGUAGE CPP, DeriveFunctor, DeriveFoldable, DeriveTraversable #-}+module Main where++import qualified Data.List as L+import Control.Monad+import Data.Functor.Classes+import Bound++infixl 9 :@++data Exp a+ = V a+ | Exp a :@ Exp a+ | Lam {-# UNPACK #-} !Int (Pat Exp a) (Scope Int Exp a)+ | Let {-# UNPACK #-} !Int [Scope Int Exp a] (Scope Int Exp a)+ | Case (Exp a) [Alt Exp a]+ deriving (Eq,Functor,Foldable,Traversable)++instance Applicative Exp where+ pure = V+ (<*>) = ap++instance Monad Exp where+#if !(MIN_VERSION_base(4,11,0))+ return = V+#endif+ V a >>= f = f a+ (x :@ y) >>= f = (x >>= f) :@ (y >>= f)+ Lam n p e >>= f = Lam n (p >>>= f) (e >>>= f)+ Let n bs e >>= f = Let n (map (>>>= f) bs) (e >>>= f)+ Case e as >>= f = Case (e >>= f) (map (>>>= f) as)++instance Eq1 Exp where+ liftEq eq (V a) (V b) = eq a b+ liftEq eq (a :@ a') (b :@ b') = liftEq eq a b && liftEq eq a' b'+ liftEq eq (Lam n p e) (Lam n' p' e') = n == n' && liftEq eq p p' && liftEq eq e e'+ liftEq eq (Let n bs e) (Let n' bs' e') = n == n' && liftEq (liftEq eq) bs bs' && liftEq eq e e'+ liftEq eq (Case e as) (Case e' as') = liftEq eq e e' && liftEq (liftEq eq) as as'+ liftEq _ _ _ = False+-- And "similarly" for Ord1, Show1 and Read1++data Pat f a+ = VarP+ | WildP+ | AsP (Pat f a)+ | ConP String [Pat f a]+ | ViewP (Scope Int f a) (Pat f a)+ deriving (Eq,Ord,Show,Read,Functor,Foldable,Traversable)++instance (Eq1 f, Monad f) => Eq1 (Pat f) where+ liftEq _ VarP VarP = True+ liftEq _ WildP WildP = True+ liftEq eq (AsP p) (AsP p') = liftEq eq p p'+ liftEq eq (ConP g ps) (ConP g' ps') = g == g' && liftEq (liftEq eq) ps ps'+ liftEq eq (ViewP e p) (ViewP e' p') = liftEq eq e e' && liftEq eq p p'+ liftEq _ _ _ = False++instance Bound Pat where+ VarP >>>= _ = VarP+ WildP >>>= _ = WildP+ AsP p >>>= f = AsP (p >>>= f)+ ConP g ps >>>= f = ConP g (map (>>>= f) ps)+ ViewP e p >>>= f = ViewP (e >>>= f) (p >>>= f)++data Alt f a = Alt {-# UNPACK #-} !Int (Pat f a) (Scope Int f a)+ deriving (Eq,Functor,Foldable,Traversable)++instance (Eq1 f, Monad f) => Eq1 (Alt f) where+ liftEq eq (Alt n p b) (Alt n' p' b') =+ n == n' && liftEq eq p p' && liftEq eq b b'++instance Bound Alt where+ Alt n p b >>>= f = Alt n (p >>>= f) (b >>>= f)++-- ** smart patterns++data P a = P { pattern :: [a] -> Pat Exp a, bindings :: [a] }++-- |+-- >>> lam (varp "x") (V "x")+-- Lam 1 VarP (Scope (V (B 0)))+varp :: a -> P a+varp a = P (const VarP) [a]++wildp :: P a+wildp = P (const WildP) []++asp :: a -> P a -> P a+asp a (P p as) = P (\bs -> AsP (p (a:bs))) (a:as)++-- |+-- >>> lam (conp "Hello" [varp "x", wildp]) (V "y")+-- Lam 1 (ConP "Hello" [VarP,WildP]) (Scope (V (F (V "y"))))+conp :: String -> [P a] -> P a+conp g ps = P (ConP g . go ps) (ps >>= bindings)+ where+ go (P p as:ps') bs = p bs : go ps' (bs ++ as)+ go [] _ = []++-- | view patterns can view variables that are bound earlier than them in the pattern+viewp :: Eq a => Exp a -> P a -> P a+viewp t (P p as) = P (\bs -> ViewP (abstract (`L.elemIndex` bs) t) (p bs)) as++-- | smart lam constructor+--+-- >>> let_ [("x",V "y"),("y",V "x" :@ V "y")] $ lam (varp "z") (V "z" :@ V "y")+-- Let 2 [Scope (V (B 1)),Scope (V (B 0) :@ V (B 1))] (Scope (Lam 1 VarP (Scope (V (B 0) :@ V (F (V (B 1)))))))+--+-- >>> lam (conp "F" [varp "x", viewp (V "x") $ varp "y"]) (V "y")+-- Lam 2 (ConP "F" [VarP,ViewP (Scope (V (B 0))) VarP]) (Scope (V (B 1)))+--+-- >>> lam (conp "F" [varp "x", viewp (V "y") $ varp "y"]) (V "y")+-- Lam 2 (ConP "F" [VarP,ViewP (Scope (V (F (V "y")))) VarP]) (Scope (V (B 1)))+lam :: Eq a => P a -> Exp a -> Exp a+lam (P p as) t = Lam (length as) (p []) (abstract (`L.elemIndex` as) t)++-- | smart let constructor+let_ :: Eq a => [(a, Exp a)] -> Exp a -> Exp a+let_ bs b = Let (length bs) (map (abstr . snd) bs) (abstr b)+ where vs = map fst bs+ abstr = abstract (`L.elemIndex` vs)++-- | smart alt constructor+--+-- >>> lam (varp "x") $ Case (V "x") [alt (conp "Hello" [varp "z",wildp]) (V "x"), alt (varp "y") (V "y")]+-- Lam 1 VarP (Scope (Case (V (B 0)) [Alt 1 (ConP "Hello" [VarP,WildP]) (Scope (V (F (V (B 0))))),Alt 1 VarP (Scope (V (B 0)))]))+alt :: Eq a => P a -> Exp a -> Alt Exp a+alt (P p as) t = Alt (length as) (p []) (abstract (`L.elemIndex` as) t)++main :: IO ()+main = return ()
examples/Imperative.hs view
@@ -1,286 +1,286 @@-{-# LANGUAGE DeriveFunctor, DeriveFoldable, DeriveTraversable, RankNTypes, ScopedTypeVariables #-} -module Main where - --- It's possible to use bound "sideways" in order to support terms which do not --- have a Monad instance. A typical situation in which this would happen is when --- modelling an imperative language: variables are bound by statements, but they --- are used in positions where it would make no sense to replace them by another --- statement. - -import Bound.Scope -- .Simple -import Bound.Var -import Control.Monad (ap) -import Data.Functor.Identity -import Data.IORef -import Data.Void (Void, absurd) - --- PART 1: We want to model a tiny assembly language. --- --- %0 = add 1 2 --- %1 = add %0 %0 --- ret %1 --- --- Add binds a fresh variable, and its operands can either be literals or --- previously-bound variables. Ret must be the last instruction. --- --- Operand is monadic, traversable, and satisfies all the other requirements in --- order to be used with bound. But this is not sufficient, since Operand is --- not the whole language: we also need to define Prog, the sequence of --- instructions. -data Operand a - = Lit Int - | Var a - deriving (Eq,Ord,Show,Read,Functor,Foldable,Traversable) - -instance Applicative Operand where - pure = Var - (<*>) = ap - -instance Monad Operand where - return = pure - Lit i >>= _ = Lit i - Var x >>= f = f x - --- The following definition correctly models the instructions and their free --- variables. But since the Var in Operand cannot be replaced with a Prog, this --- definition is not monadic, and so we cannot manipulate the (Scope () Prog a) --- using bound's functions. This defeats the point of using Scope at all! --- --- data Prog a --- = Ret (Operand a) --- | Add (Operand a) (Operand a) --- (Scope () Prog a) -- one more bound variable, available --- -- in the rest of the program --- --- The sideways trick is to replace the Operand constructor with a (* -> *) type --- parameter. Instantiating this with the real Operand will allow Operand to --- access the same free variables as Prog. But if we instantiate this with --- (Scope () Operand) instead, then the operands will have access to one extra --- bound variable! This way, we can bind fresh variables which can only be used --- inside the operands, and not in Prog. -data Prog operand a - = Ret (operand a) - | Add (operand a) (operand a) - (Prog (Scope () operand) a) - deriving (Eq,Ord,Show,Read,Functor,Foldable,Traversable) - --- The fact that the variables are not available in Prog after they are bound --- might seem strange, and we'll fix this in part 2, but it is actually a good --- thing. We want to be able to replace those variables with operand values, and --- that would not be possible if variables were allowed to appear inside Prog --- but outside of an operand. -pInstantiate1 :: forall operand b a. (Applicative operand, Monad operand) - => operand a - -> Prog (Scope b operand) a - -> Prog operand a -pInstantiate1 = go instantiate1 - where - -- A value of type (Prog (Scope b operand) a) contains operands of type - -- (Scope b operand a), on which we can call instantiate1: - -- - -- instantiate1 :: operand a -> Scope b operand a -> operand a - -- - -- In the function below, (Scope b operand) and operand become o and o', - -- and instantiate1 is called f: - -- - -- f :: operand v -> o v -> o' v - go :: forall o o' u. (Monad o, Monad o') - => (forall v. operand v -> o v -> o' v) - -> operand u -> Prog o u -> Prog o' u - go f x (Ret o) = Ret (f x o) - go f x (Add o1 o2 cc) = Add (f x o1) (f x o2) - $ go f' x cc - where - -- The rest of the program has access to one extra variable: - -- - -- cc :: Prog (Scope () (Scope b operand)) a - -- - -- In there, the operands have type (Scope () (Scope b operand) a), and - -- this time we cannot call instantiate1 because it would instantiate () - -- instead of instantiating b. Instead, we create a function f' which - -- preserves the outer (Scope ()): - -- - -- f' :: operand a -> Scope () (Scope b operand) a -> Scope () operand a - -- f' :: operand a -> Scope () o a -> Scope () o' a - -- - -- In the recursive call to go, (Scope () (Scope b operand)) and - -- (Scope () operand) become o and o', and f' is called f. - f' :: operand v -> Scope () o v -> Scope () o' v - f' v = toScope . f (fmap F v) . fromScope - -pAbstract1 :: forall operand a. (Applicative operand, Monad operand, Eq a) - => a - -> Prog operand a - -> Prog (Scope () operand) a -pAbstract1 = go abstract1 - where - go :: forall o o' u. (Eq u, Monad o, Monad o') - => (forall v. Eq v => v -> o v -> o' v) - -> u -> Prog o u -> Prog o' u - go f x (Ret o) = Ret (f x o) - go f x (Add o1 o2 cc) = Add (f x o1) (f x o2) - $ go f' x cc - where - f' :: forall v. Eq v => v -> Scope () o v -> Scope () o' v - f' v = toScope . f (F v) . fromScope - -evalOperand :: Operand Void -> Int -evalOperand (Lit i) = i -evalOperand (Var void) = absurd void - --- | --- >>> :{ --- let Just prog = closed --- $ Add (Lit 1) (Lit 2) $ pAbstract1 "%0" --- $ Add (Var "%0") (Var "%0") $ pAbstract1 "%1" --- $ Ret (Var "%1") --- :} --- --- >>> evalProg prog --- 6 -evalProg :: Prog Operand Void -> Int -evalProg (Ret o) = evalOperand o -evalProg (Add o1 o2 cc) = evalProg cc' - where - result :: Int - result = evalOperand o1 + evalOperand o2 - - cc' :: Prog Operand Void - cc' = pInstantiate1 (Lit result) cc - - --- PART 2: Here's a slightly more complicated language. --- --- %0 = add 1 2 --- %1 = add %0 %0 --- swp %0 %1 --- ret %1 --- --- The new swp command swaps the contents of two variables, so the two arguments --- must be previously-bound variables, they cannot be literals. This time the --- naïve definition looks like this: --- --- data Prog' a --- = Ret' (Operand a) --- | Swp' a a --- (Prog' a) --- | Add' (Operand a) (Operand a) --- (Scope () Prog' a) --- --- If we apply the sideways trick to this definition, the newly-bound variables --- will only be available in the operands, and so it won't be possible to call --- swp on them. The first step towards a solution is to add seemingly-useless --- Identity wrappers: --- --- data Prog' a --- = Ret' (Operand a) --- | Swp' (Identity a) (Identity a) --- (Prog' a) --- | Add' (Operand a) (Operand a) --- (Scope () Prog' a) --- --- We can now apply the sideways trick twice: once for Operand, and once for --- Identity. This gives us a lot of control: we can bind fresh variables which --- can only be used inside the operands, we can bind fresh variables which can --- be used inside Prog but not inside the operands, and as required for this --- example, we can bind fresh variables which can be used in both. -data Prog' operand identity a - = Ret' (operand a) - | Swp' (identity a) (identity a) - (Prog' operand identity a) - | Add' (operand a) (operand a) - (Prog' (Scope () operand) (Scope () identity) a) - deriving (Eq,Ord,Show,Read,Functor,Foldable,Traversable) - --- Bound variables can now occur in both operand and identity, so we can no --- longer instantiate them with operands. Instead, we'll have to instantiate --- them with a value which both (Operand a) and (Identity a) can contain: --- a free variable. -pInstantiate1' :: ( Applicative operand, Monad operand - , Applicative identity, Monad identity - ) - => a - -> Prog' (Scope () operand) (Scope () identity) a - -> Prog' operand identity a -pInstantiate1' = go (instantiate1 . pure) (instantiate1 . pure) - where - go :: forall o o' i i' u. (Monad i, Monad i', Monad o, Monad o') - => (forall v. v -> o v -> o' v) - -> (forall v. v -> i v -> i' v) - -> u -> Prog' o i u -> Prog' o' i' u - go fo fi x = go' - where - go' (Ret' o) = Ret' (fo x o) - go' (Swp' i1 i2 cc) = Swp' (fi x i1) - (fi x i2) - (go' cc) - go' (Add' o1 o2 cc) = Add' (fo x o1) - (fo x o2) - (go fo' fi' x cc) - - fo' :: v -> Scope () o v -> Scope () o' v - fo' v = toScope . fo (F v) . fromScope - - fi' :: v -> Scope () i v -> Scope () i' v - fi' v = toScope . fi (F v) . fromScope - -pAbstract1' :: ( Applicative operand, Monad operand - , Applicative identity, Monad identity - , Eq a - ) - => a - -> Prog' operand identity a - -> Prog' (Scope () operand) (Scope () identity) a -pAbstract1' = go abstract1 abstract1 - where - go :: forall o o' i i' u. (Eq u, Monad i, Monad i', Monad o, Monad o') - => (forall v. Eq v => v -> o v -> o' v) - -> (forall v. Eq v => v -> i v -> i' v) - -> u -> Prog' o i u -> Prog' o' i' u - go fo fi x = go' - where - go' (Ret' o) = Ret' (fo x o) - go' (Swp' i1 i2 cc) = Swp' (fi x i1) - (fi x i2) - (go' cc) - go' (Add' o1 o2 cc) = Add' (fo x o1) - (fo x o2) - (go fo' fi' x cc) - - fo' :: Eq v => v -> Scope () o v -> Scope () o' v - fo' v = toScope . fo (F v) . fromScope - - fi' :: Eq v => v -> Scope () i v -> Scope () i' v - fi' v = toScope . fi (F v) . fromScope - -evalOperand' :: Operand (IORef Int) -> IO Int -evalOperand' (Lit i) = return i -evalOperand' (Var ref) = readIORef ref - --- | --- >>> :{ --- let Just prog' = closed --- $ Add' (Lit 1) (Lit 2) $ pAbstract1' "%0" --- $ Add' (Var "%0") (Var "%0") $ pAbstract1' "%1" --- $ Swp' (Identity "%0") (Identity "%1") --- $ Ret' (Var "%1") --- :} --- --- >>> evalProg' prog' --- 3 -evalProg' :: Prog' Operand Identity (IORef Int) -> IO Int -evalProg' (Ret' o) = evalOperand' o -evalProg' (Swp' (Identity ref1) (Identity ref2) cc) = do - x <- readIORef ref1 - y <- readIORef ref2 - writeIORef ref1 y - writeIORef ref2 x - evalProg' cc -evalProg' (Add' o1 o2 cc) = do - result <- (+) <$> evalOperand' o1 <*> evalOperand' o2 - ref <- newIORef result - evalProg' (pInstantiate1' ref cc) - - -main :: IO () -main = return () +{-# LANGUAGE DeriveFunctor, DeriveFoldable, DeriveTraversable, RankNTypes, ScopedTypeVariables #-}+module Main where++-- It's possible to use bound "sideways" in order to support terms which do not+-- have a Monad instance. A typical situation in which this would happen is when+-- modelling an imperative language: variables are bound by statements, but they+-- are used in positions where it would make no sense to replace them by another+-- statement.++import Bound.Scope -- .Simple+import Bound.Var+import Control.Monad (ap)+import Data.Functor.Identity+import Data.IORef+import Data.Void (Void, absurd)++-- PART 1: We want to model a tiny assembly language.+--+-- %0 = add 1 2+-- %1 = add %0 %0+-- ret %1+--+-- Add binds a fresh variable, and its operands can either be literals or+-- previously-bound variables. Ret must be the last instruction.+--+-- Operand is monadic, traversable, and satisfies all the other requirements in+-- order to be used with bound. But this is not sufficient, since Operand is+-- not the whole language: we also need to define Prog, the sequence of+-- instructions.+data Operand a+ = Lit Int+ | Var a+ deriving (Eq,Ord,Show,Read,Functor,Foldable,Traversable)++instance Applicative Operand where+ pure = Var+ (<*>) = ap++instance Monad Operand where+ return = pure+ Lit i >>= _ = Lit i+ Var x >>= f = f x++-- The following definition correctly models the instructions and their free+-- variables. But since the Var in Operand cannot be replaced with a Prog, this+-- definition is not monadic, and so we cannot manipulate the (Scope () Prog a)+-- using bound's functions. This defeats the point of using Scope at all!+--+-- data Prog a+-- = Ret (Operand a)+-- | Add (Operand a) (Operand a)+-- (Scope () Prog a) -- one more bound variable, available+-- -- in the rest of the program+--+-- The sideways trick is to replace the Operand constructor with a (* -> *) type+-- parameter. Instantiating this with the real Operand will allow Operand to+-- access the same free variables as Prog. But if we instantiate this with+-- (Scope () Operand) instead, then the operands will have access to one extra+-- bound variable! This way, we can bind fresh variables which can only be used+-- inside the operands, and not in Prog.+data Prog operand a+ = Ret (operand a)+ | Add (operand a) (operand a)+ (Prog (Scope () operand) a)+ deriving (Eq,Ord,Show,Read,Functor,Foldable,Traversable)++-- The fact that the variables are not available in Prog after they are bound+-- might seem strange, and we'll fix this in part 2, but it is actually a good+-- thing. We want to be able to replace those variables with operand values, and+-- that would not be possible if variables were allowed to appear inside Prog+-- but outside of an operand.+pInstantiate1 :: forall operand b a. (Applicative operand, Monad operand)+ => operand a+ -> Prog (Scope b operand) a+ -> Prog operand a+pInstantiate1 = go instantiate1+ where+ -- A value of type (Prog (Scope b operand) a) contains operands of type+ -- (Scope b operand a), on which we can call instantiate1:+ --+ -- instantiate1 :: operand a -> Scope b operand a -> operand a+ --+ -- In the function below, (Scope b operand) and operand become o and o',+ -- and instantiate1 is called f:+ --+ -- f :: operand v -> o v -> o' v+ go :: forall o o' u. (Monad o, Monad o')+ => (forall v. operand v -> o v -> o' v)+ -> operand u -> Prog o u -> Prog o' u+ go f x (Ret o) = Ret (f x o)+ go f x (Add o1 o2 cc) = Add (f x o1) (f x o2)+ $ go f' x cc+ where+ -- The rest of the program has access to one extra variable:+ --+ -- cc :: Prog (Scope () (Scope b operand)) a+ --+ -- In there, the operands have type (Scope () (Scope b operand) a), and+ -- this time we cannot call instantiate1 because it would instantiate ()+ -- instead of instantiating b. Instead, we create a function f' which+ -- preserves the outer (Scope ()):+ --+ -- f' :: operand a -> Scope () (Scope b operand) a -> Scope () operand a+ -- f' :: operand a -> Scope () o a -> Scope () o' a+ --+ -- In the recursive call to go, (Scope () (Scope b operand)) and+ -- (Scope () operand) become o and o', and f' is called f.+ f' :: operand v -> Scope () o v -> Scope () o' v+ f' v = toScope . f (fmap F v) . fromScope++pAbstract1 :: forall operand a. (Applicative operand, Monad operand, Eq a)+ => a+ -> Prog operand a+ -> Prog (Scope () operand) a+pAbstract1 = go abstract1+ where+ go :: forall o o' u. (Eq u, Monad o, Monad o')+ => (forall v. Eq v => v -> o v -> o' v)+ -> u -> Prog o u -> Prog o' u+ go f x (Ret o) = Ret (f x o)+ go f x (Add o1 o2 cc) = Add (f x o1) (f x o2)+ $ go f' x cc+ where+ f' :: forall v. Eq v => v -> Scope () o v -> Scope () o' v+ f' v = toScope . f (F v) . fromScope++evalOperand :: Operand Void -> Int+evalOperand (Lit i) = i+evalOperand (Var void) = absurd void++-- |+-- >>> :{+-- let Just prog = closed+-- $ Add (Lit 1) (Lit 2) $ pAbstract1 "%0"+-- $ Add (Var "%0") (Var "%0") $ pAbstract1 "%1"+-- $ Ret (Var "%1")+-- :}+--+-- >>> evalProg prog+-- 6+evalProg :: Prog Operand Void -> Int+evalProg (Ret o) = evalOperand o+evalProg (Add o1 o2 cc) = evalProg cc'+ where+ result :: Int+ result = evalOperand o1 + evalOperand o2++ cc' :: Prog Operand Void+ cc' = pInstantiate1 (Lit result) cc+++-- PART 2: Here's a slightly more complicated language.+--+-- %0 = add 1 2+-- %1 = add %0 %0+-- swp %0 %1+-- ret %1+--+-- The new swp command swaps the contents of two variables, so the two arguments+-- must be previously-bound variables, they cannot be literals. This time the+-- naïve definition looks like this:+--+-- data Prog' a+-- = Ret' (Operand a)+-- | Swp' a a+-- (Prog' a)+-- | Add' (Operand a) (Operand a)+-- (Scope () Prog' a)+--+-- If we apply the sideways trick to this definition, the newly-bound variables+-- will only be available in the operands, and so it won't be possible to call+-- swp on them. The first step towards a solution is to add seemingly-useless+-- Identity wrappers:+--+-- data Prog' a+-- = Ret' (Operand a)+-- | Swp' (Identity a) (Identity a)+-- (Prog' a)+-- | Add' (Operand a) (Operand a)+-- (Scope () Prog' a)+--+-- We can now apply the sideways trick twice: once for Operand, and once for+-- Identity. This gives us a lot of control: we can bind fresh variables which+-- can only be used inside the operands, we can bind fresh variables which can+-- be used inside Prog but not inside the operands, and as required for this+-- example, we can bind fresh variables which can be used in both.+data Prog' operand identity a+ = Ret' (operand a)+ | Swp' (identity a) (identity a)+ (Prog' operand identity a)+ | Add' (operand a) (operand a)+ (Prog' (Scope () operand) (Scope () identity) a)+ deriving (Eq,Ord,Show,Read,Functor,Foldable,Traversable)++-- Bound variables can now occur in both operand and identity, so we can no+-- longer instantiate them with operands. Instead, we'll have to instantiate+-- them with a value which both (Operand a) and (Identity a) can contain:+-- a free variable.+pInstantiate1' :: ( Applicative operand, Monad operand+ , Applicative identity, Monad identity+ )+ => a+ -> Prog' (Scope () operand) (Scope () identity) a+ -> Prog' operand identity a+pInstantiate1' = go (instantiate1 . pure) (instantiate1 . pure)+ where+ go :: forall o o' i i' u. (Monad i, Monad i', Monad o, Monad o')+ => (forall v. v -> o v -> o' v)+ -> (forall v. v -> i v -> i' v)+ -> u -> Prog' o i u -> Prog' o' i' u+ go fo fi x = go'+ where+ go' (Ret' o) = Ret' (fo x o)+ go' (Swp' i1 i2 cc) = Swp' (fi x i1)+ (fi x i2)+ (go' cc)+ go' (Add' o1 o2 cc) = Add' (fo x o1)+ (fo x o2)+ (go fo' fi' x cc)++ fo' :: v -> Scope () o v -> Scope () o' v+ fo' v = toScope . fo (F v) . fromScope++ fi' :: v -> Scope () i v -> Scope () i' v+ fi' v = toScope . fi (F v) . fromScope++pAbstract1' :: ( Applicative operand, Monad operand+ , Applicative identity, Monad identity+ , Eq a+ )+ => a+ -> Prog' operand identity a+ -> Prog' (Scope () operand) (Scope () identity) a+pAbstract1' = go abstract1 abstract1+ where+ go :: forall o o' i i' u. (Eq u, Monad i, Monad i', Monad o, Monad o')+ => (forall v. Eq v => v -> o v -> o' v)+ -> (forall v. Eq v => v -> i v -> i' v)+ -> u -> Prog' o i u -> Prog' o' i' u+ go fo fi x = go'+ where+ go' (Ret' o) = Ret' (fo x o)+ go' (Swp' i1 i2 cc) = Swp' (fi x i1)+ (fi x i2)+ (go' cc)+ go' (Add' o1 o2 cc) = Add' (fo x o1)+ (fo x o2)+ (go fo' fi' x cc)++ fo' :: Eq v => v -> Scope () o v -> Scope () o' v+ fo' v = toScope . fo (F v) . fromScope++ fi' :: Eq v => v -> Scope () i v -> Scope () i' v+ fi' v = toScope . fi (F v) . fromScope++evalOperand' :: Operand (IORef Int) -> IO Int+evalOperand' (Lit i) = return i+evalOperand' (Var ref) = readIORef ref++-- |+-- >>> :{+-- let Just prog' = closed+-- $ Add' (Lit 1) (Lit 2) $ pAbstract1' "%0"+-- $ Add' (Var "%0") (Var "%0") $ pAbstract1' "%1"+-- $ Swp' (Identity "%0") (Identity "%1")+-- $ Ret' (Var "%1")+-- :}+--+-- >>> evalProg' prog'+-- 3+evalProg' :: Prog' Operand Identity (IORef Int) -> IO Int+evalProg' (Ret' o) = evalOperand' o+evalProg' (Swp' (Identity ref1) (Identity ref2) cc) = do+ x <- readIORef ref1+ y <- readIORef ref2+ writeIORef ref1 y+ writeIORef ref2 x+ evalProg' cc+evalProg' (Add' o1 o2 cc) = do+ result <- (+) <$> evalOperand' o1 <*> evalOperand' o2+ ref <- newIORef result+ evalProg' (pInstantiate1' ref cc)+++main :: IO ()+main = return ()
examples/Overkill.hs view
@@ -1,344 +1,344 @@-{-# LANGUAGE CPP #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE PolyKinds #-} -{-# LANGUAGE GADTs #-} -{-# LANGUAGE TypeOperators #-} - -{-# OPTIONS_GHC -Wincomplete-patterns -Wno-orphans #-} - -module Main where - -import Data.Kind -import qualified Data.Vector as Vector -import Data.Vector (Vector) -import qualified Data.List as List -import Data.Foldable -import Data.Traversable -import Control.Monad -import Control.Applicative -import Prelude hiding (foldr) -import Data.Functor.Classes -import Data.Type.Equality -import Bound - -infixl 9 :@ -infixr 5 :> - -data Exp a - = Var a - | Exp a :@ Exp a - | forall (b :: Index). Lam (Pat b Exp a) (Scope (Path b) Exp a) - | Let (Vector (Scope Int Exp a)) (Scope Int Exp a) - -data Index = VarI | WildI | AsI Index | ConI [Index] - -data Pat :: Index -> (Type -> Type) -> Type -> Type where - VarP :: Pat 'VarI f a - WildP :: Pat 'WildI f a - AsP :: Pat i f a -> Pat ('AsI i) f a - ConP :: String -> Pats bs f a -> Pat ('ConI bs) f a - ViewP :: f a -> Pat b f a -> Pat b f a -- TODO: allow references to earlier variables - -data Pats :: [Index] -> (Type -> Type) -> Type -> Type where - NilP :: Pats '[] f a - (:>) :: Pat b f a -> Pats bs f a -> Pats (b ': bs) f a - -data Path :: Index -> Type where - V :: Path 'VarI - L :: Path ('AsI a) - R :: Path a -> Path ('AsI a) - C :: MPath as -> Path ('ConI as) - -data MPath :: [Index] -> Type where - H :: Path a -> MPath (a ':as) - T :: MPath as -> MPath (a ':as) - -instance Functor Exp where - fmap = fmapDefault - -instance Foldable Exp where - foldMap = foldMapDefault - -instance Applicative Exp where - pure = Var - (<*>) = ap - -instance Traversable Exp where - traverse f (Var a) = Var <$> f a - traverse f (x :@ y) = (:@) <$> traverse f x <*> traverse f y - traverse f (Lam p e) = Lam <$> traverse f p <*> traverse f e - traverse f (Let bs e) = Let <$> traverse (traverse f) bs <*> traverse f e - -instance Monad Exp where -#if !(MIN_VERSION_base(4,11,0)) - return = Var -#endif - Var a >>= f = f a - (x :@ y) >>= f = (x >>= f) :@ (y >>= f) - Lam p e >>= f = Lam (p >>>= f) (e >>>= f) - Let bs e >>= f = Let (fmap (>>>= f) bs) (e >>>= f) - -instance Eq a => Eq (Exp a) where (==) = eq1 -instance Eq1 Exp where - liftEq eq (Var a) (Var b) = eq a b - liftEq eq (a :@ a') (b :@ b') = liftEq eq a b && liftEq eq a' b' - liftEq eq (Lam ps a) (Lam qs b) = - case eqPat' eq ps qs of - Nothing -> False - Just Refl -> liftEq eq a b - - liftEq eq (Let as a) (Let bs b) = liftEq (liftEq eq) as bs && liftEq eq a b - liftEq _ _ _ = False - -instance Show a => Show (Exp a) where showsPrec = showsPrec1 -instance Show1 Exp where - liftShowsPrec s _ d (Var a) = showParen (d > 10) $ showString "Var " . s 11 a - liftShowsPrec s sl d (a :@ b) = showParen (d > 9) $ liftShowsPrec s sl 9 a . showString " :@ " . liftShowsPrec s sl 10 b - liftShowsPrec s sl d (Lam ps b) = showParen (d > 10) $ showString "Lam " . liftShowsPrec s sl 11 ps . showChar ' ' . liftShowsPrec s sl 11 b - liftShowsPrec s sl d (Let bs b) = showParen (d > 10) $ showString "Let " . liftShowsPrec (liftShowsPrec s sl) (liftShowList s sl) 11 bs . showChar ' ' . liftShowsPrec s sl 11 b - --- * smart lam - --- ** smart patterns - -data P a = forall b. P (Pat b Exp a) [a] (a -> Maybe (Path b)) - -varp :: Eq a => a -> P a -varp a = P VarP [a] (\v -> if a == v then Just V else Nothing) - -wildp :: P a -wildp = P WildP [] (const Nothing) - -asp :: Eq a => a -> P a -> P a -asp a (P p as f) = P (AsP p) (a:as) $ \v -> case f v of - Just b -> Just (R b) - Nothing | a == v -> Just L - | otherwise -> Nothing - -data Ps a = forall bs. Ps (Pats bs Exp a) [a] (a -> Maybe (MPath bs)) - -conp :: String -> [P a] -> P a -conp g ps = case go ps of - Ps qs as f -> P (ConP g qs) as (fmap C . f) - where - go :: [P a] -> Ps a - go [] = Ps NilP [] (const Nothing) - go (P p as f : xs) = case go xs of - Ps ps' ass g' -> Ps (p :> ps') (as ++ ass) $ \v -> - T <$> g' v <|> H <$> f v - --- * smart lam -lam :: P a -> Exp a -> Exp a -lam (P p _ f) t = Lam p (abstract f t) - --- * smart let -let_ :: Eq a => [(a, Exp a)] -> Exp a -> Exp a -let_ bs b = Let (Vector.fromList $ map (abstr . snd) bs) (abstr b) - where vs = map fst bs - abstr = abstract (`List.elemIndex` vs) - --- * Pat - --- ** A Kind of Shape - -eqPat :: (Eq1 f) => (a -> b -> Bool) -> Pat i f a -> Pat i' f b -> Bool -eqPat _ VarP VarP = True -eqPat _ WildP WildP = True -eqPat eq (AsP p) (AsP q) = eqPat eq p q -eqPat eq (ConP g ps) (ConP h qs) = g == h && eqPats eq ps qs -eqPat eq (ViewP e p) (ViewP f q) = liftEq eq e f && eqPat eq p q -eqPat _ _ _ = False - --- The same as eqPat, but if the patterns are equal, it returns a --- proof that their type arguments are the same. -eqPat' :: (Eq1 f) => (a -> a' -> Bool) -> Pat b f a -> Pat b' f a' -> Maybe (b :~: b') -eqPat' _ VarP VarP = Just Refl -eqPat' _ WildP WildP = Just Refl -eqPat' eq (AsP p) (AsP q) = do - Refl <- eqPat' eq p q - Just Refl -eqPat' eq (ConP g ps) (ConP h qs) = do - guard (g == h) - Refl <- eqPats' eq ps qs - Just Refl -eqPat' eq (ViewP e p) (ViewP f q) = guard (liftEq eq e f) >> eqPat' eq p q -eqPat' _ _ _ = Nothing - -instance Eq1 f => Eq1 (Pat b f) where liftEq = eqPat -instance (Eq1 f, Eq a) => Eq (Pat b f a) where (==) = eq1 - -instance (Show1 f, Show a) => Show (Pat b f a) where showsPrec = showsPrec1 - -instance Show1 f => Show1 (Pat b f) where - liftShowsPrec _ _ _ VarP = showString "VarP" - liftShowsPrec _ _ _ WildP = showString "WildP" - liftShowsPrec s sl d (AsP p) = showParen (d > 10) $ showString "AsP " . liftShowsPrec s sl 11 p - liftShowsPrec s sl d (ConP g ps) = showParen (d > 10) $ showString "ConP " . showsPrec 11 g . showChar ' ' . liftShowsPrec s sl 11 ps - liftShowsPrec s sl d (ViewP e p) = showParen (d > 10) $ showString "ViewP " . liftShowsPrec s sl 11 e . showChar ' ' . liftShowsPrec s sl 11 p - -instance Functor f => Functor (Pat b f) where - fmap _ VarP = VarP - fmap _ WildP = WildP - fmap f (AsP p) = AsP (fmap f p) - fmap f (ConP g ps) = ConP g (fmap f ps) - fmap f (ViewP e p) = ViewP (fmap f e) (fmap f p) - -instance Foldable f => Foldable (Pat b f) where - foldMap f (AsP p) = foldMap f p - foldMap f (ConP _g ps) = foldMap f ps - foldMap f (ViewP e p) = foldMap f e `mappend` foldMap f p - foldMap _ _ = mempty - -instance Traversable f => Traversable (Pat b f) where - traverse _ VarP = pure VarP - traverse _ WildP = pure WildP - traverse f (AsP p) = AsP <$> traverse f p - traverse f (ConP g ps) = ConP g <$> traverse f ps - traverse f (ViewP e p) = ViewP <$> traverse f e <*> traverse f p - -instance Bound (Pat b) where - VarP >>>= _ = VarP - WildP >>>= _ = WildP - AsP p >>>= f = AsP (p >>>= f) - ConP g ps >>>= f = ConP g (ps >>>= f) - ViewP e p >>>= f = ViewP (e >>= f) (p >>>= f) - --- ** Pats -eqPats :: (Eq1 f) => (a -> b -> Bool) -> Pats bs f a -> Pats bs' f b -> Bool -eqPats _ NilP NilP = True -eqPats eq (p :> ps) (q :> qs) = eqPat eq p q && eqPats eq ps qs -eqPats _ _ _ = False - --- Like eqPats, but if the patses are equal, it returns a proof that their --- type arguments are the same. -eqPats' :: (Eq1 f) => (a -> a' -> Bool) -> Pats bs f a -> Pats bs' f a' -> Maybe (bs :~: bs') -eqPats' _ NilP NilP = Just Refl -eqPats' eq (p :> ps) (q :> qs) = do - Refl <- eqPat' eq p q - Refl <- eqPats' eq ps qs - Just Refl -eqPats' _ _ _ = Nothing - -instance Eq1 f => Eq1 (Pats bs f) where liftEq = eqPats -instance (Eq1 f, Eq a) => Eq (Pats bs f a) where (==) = eq1 - -instance (Show1 f, Show a) => Show (Pats bs f a) where showsPrec = showsPrec1 -instance Show1 f => Show1 (Pats bs f) where - liftShowsPrec _ _ _ NilP = showString "NilP" - liftShowsPrec s sl d (p :> ps) = showParen (d > 5) $ - liftShowsPrec s sl 6 p . showString " :> " . liftShowsPrec s sl 5 ps - -instance Functor f => Functor (Pats bs f) where - fmap _ NilP = NilP - fmap f (p :> ps) = fmap f p :> fmap f ps - -instance Foldable f => Foldable (Pats bs f) where - foldMap f (p :> ps) = foldMap f p `mappend` foldMap f ps - foldMap _ _ = mempty - -instance Traversable f => Traversable (Pats bs f) where - traverse _f NilP = pure NilP - traverse f (p :> ps) = (:>) <$> traverse f p <*> traverse f ps - -instance Bound (Pats bs) where - NilP >>>= _ = NilP - (p :> ps) >>>= f = (p >>>= f) :> (ps >>>= f) - --- ** Path into Pats --- Internally, this is only used to implement eqPath, which is only --- used to implement this. -eqMPath :: MPath is -> MPath js -> Bool -eqMPath (H m) (H n) = eqPath m n -eqMPath (T p) (T q) = eqMPath p q -eqMPath _ _ = False - -instance Eq (MPath is) where - H m == H n = m == n - T p == T q = p == q - _ == _ = False - --- Internally, this is only used to define comparePath, which --- is only used here to define this. -compareMPath :: MPath is -> MPath js -> Ordering -compareMPath (H m) (H n) = comparePath m n -compareMPath (H _) (T _) = LT -compareMPath (T p) (T q) = compareMPath p q -compareMPath (T _) (H _) = GT - -instance Ord (MPath is) where - compare (H m) (H n) = compare m n - compare (H _) (T _) = LT - compare (T p) (T q) = compare p q - compare (T _) (H _) = GT - -instance Show (MPath is) where - showsPrec d (H m) = showParen (d > 10) $ showString "H " . showsPrec 11 m - showsPrec d (T p) = showParen (d > 10) $ showString "T " . showsPrec 11 p - --- instance Read (MPath is) - --- ** Path into Pat --- Internally, this is only used to implement eqMPath, which is only used --- to implement this. -eqPath :: Path i -> Path j -> Bool -eqPath V V = True -eqPath L L = True -eqPath (R m) (R n) = eqPath m n -eqPath (C p) (C q) = eqMPath p q -eqPath _ _ = False - -instance Eq (Path i) where - p == q = case compare p q of - EQ -> True - _ -> False - --- Internally, this is only used to define compareMPath, which --- is only used here to define this. -comparePath :: Path i -> Path j -> Ordering -comparePath V V = EQ -comparePath V _ = LT -comparePath L V = GT -comparePath L L = EQ -comparePath L _ = LT -comparePath (R _) V = GT -comparePath (R _) L = GT -comparePath (R m) (R n) = comparePath m n -comparePath (R _) (C _) = LT -comparePath (C p) (C q) = compareMPath p q -comparePath (C _) _ = GT - -instance Ord (Path i) where - compare V y = case (y :: Path 'VarI) of V -> EQ - compare L y = cpL y - where - cpL :: Path ('AsI a) -> Ordering - cpL L = EQ - cpL (R _) = LT - compare (R r) y = cpR r y - where - cpR :: Path a -> Path ('AsI a) -> Ordering - cpR _ L = GT - cpR m (R n) = compare m n - compare (C c) y = cpC c y - where - cpC :: MPath as -> Path ('ConI as) -> Ordering - cpC p (C q) = compare p q - -instance Show (Path i) where - showsPrec _ V = showString "V" - showsPrec _ L = showString "L" - showsPrec d (R m) = showParen (d > 10) $ showString "R " . showsPrec 11 m - showsPrec d (C p) = showParen (d > 10) $ showString "C " . showsPrec 11 p - --- | --- >>> let_ [("x",Var "y"),("y",Var "x" :@ Var "y")] $ lam (varp "z") (Var "z" :@ Var "y") --- Let (fromList [Scope (Var (B 1)),Scope (Var (B 0) :@ Var (B 1))]) (Scope (Lam VarP (Scope (Var (B V) :@ Var (F (Var (B 1))))))) --- --- >>> lam (varp "x") (Var "x") --- Lam VarP (Scope (Var (B V))) --- --- >>> lam (conp "Hello" [varp "x", wildp]) (Var "y") --- Lam (ConP "Hello" (VarP :> WildP :> NilP)) (Scope (Var (F (Var "y")))) -main :: IO () -main = return () +{-# LANGUAGE CPP #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE TypeOperators #-}++{-# OPTIONS_GHC -Wincomplete-patterns -Wno-orphans #-}++module Main where++import Data.Kind+import qualified Data.Vector as Vector+import Data.Vector (Vector)+import qualified Data.List as List+import Data.Foldable+import Data.Traversable+import Control.Monad+import Control.Applicative+import Prelude hiding (foldr)+import Data.Functor.Classes+import Data.Type.Equality+import Bound++infixl 9 :@+infixr 5 :>++data Exp a+ = Var a+ | Exp a :@ Exp a+ | forall (b :: Index). Lam (Pat b Exp a) (Scope (Path b) Exp a)+ | Let (Vector (Scope Int Exp a)) (Scope Int Exp a)++data Index = VarI | WildI | AsI Index | ConI [Index]++data Pat :: Index -> (Type -> Type) -> Type -> Type where+ VarP :: Pat 'VarI f a+ WildP :: Pat 'WildI f a+ AsP :: Pat i f a -> Pat ('AsI i) f a+ ConP :: String -> Pats bs f a -> Pat ('ConI bs) f a+ ViewP :: f a -> Pat b f a -> Pat b f a -- TODO: allow references to earlier variables++data Pats :: [Index] -> (Type -> Type) -> Type -> Type where+ NilP :: Pats '[] f a+ (:>) :: Pat b f a -> Pats bs f a -> Pats (b ': bs) f a++data Path :: Index -> Type where+ V :: Path 'VarI+ L :: Path ('AsI a)+ R :: Path a -> Path ('AsI a)+ C :: MPath as -> Path ('ConI as)++data MPath :: [Index] -> Type where+ H :: Path a -> MPath (a ':as)+ T :: MPath as -> MPath (a ':as)++instance Functor Exp where+ fmap = fmapDefault++instance Foldable Exp where+ foldMap = foldMapDefault++instance Applicative Exp where+ pure = Var+ (<*>) = ap++instance Traversable Exp where+ traverse f (Var a) = Var <$> f a+ traverse f (x :@ y) = (:@) <$> traverse f x <*> traverse f y+ traverse f (Lam p e) = Lam <$> traverse f p <*> traverse f e+ traverse f (Let bs e) = Let <$> traverse (traverse f) bs <*> traverse f e++instance Monad Exp where+#if !(MIN_VERSION_base(4,11,0))+ return = Var+#endif+ Var a >>= f = f a+ (x :@ y) >>= f = (x >>= f) :@ (y >>= f)+ Lam p e >>= f = Lam (p >>>= f) (e >>>= f)+ Let bs e >>= f = Let (fmap (>>>= f) bs) (e >>>= f)++instance Eq a => Eq (Exp a) where (==) = eq1+instance Eq1 Exp where+ liftEq eq (Var a) (Var b) = eq a b+ liftEq eq (a :@ a') (b :@ b') = liftEq eq a b && liftEq eq a' b'+ liftEq eq (Lam ps a) (Lam qs b) =+ case eqPat' eq ps qs of+ Nothing -> False+ Just Refl -> liftEq eq a b++ liftEq eq (Let as a) (Let bs b) = liftEq (liftEq eq) as bs && liftEq eq a b+ liftEq _ _ _ = False++instance Show a => Show (Exp a) where showsPrec = showsPrec1+instance Show1 Exp where+ liftShowsPrec s _ d (Var a) = showParen (d > 10) $ showString "Var " . s 11 a+ liftShowsPrec s sl d (a :@ b) = showParen (d > 9) $ liftShowsPrec s sl 9 a . showString " :@ " . liftShowsPrec s sl 10 b+ liftShowsPrec s sl d (Lam ps b) = showParen (d > 10) $ showString "Lam " . liftShowsPrec s sl 11 ps . showChar ' ' . liftShowsPrec s sl 11 b+ liftShowsPrec s sl d (Let bs b) = showParen (d > 10) $ showString "Let " . liftShowsPrec (liftShowsPrec s sl) (liftShowList s sl) 11 bs . showChar ' ' . liftShowsPrec s sl 11 b++-- * smart lam++-- ** smart patterns++data P a = forall b. P (Pat b Exp a) [a] (a -> Maybe (Path b))++varp :: Eq a => a -> P a+varp a = P VarP [a] (\v -> if a == v then Just V else Nothing)++wildp :: P a+wildp = P WildP [] (const Nothing)++asp :: Eq a => a -> P a -> P a+asp a (P p as f) = P (AsP p) (a:as) $ \v -> case f v of+ Just b -> Just (R b)+ Nothing | a == v -> Just L+ | otherwise -> Nothing++data Ps a = forall bs. Ps (Pats bs Exp a) [a] (a -> Maybe (MPath bs))++conp :: String -> [P a] -> P a+conp g ps = case go ps of+ Ps qs as f -> P (ConP g qs) as (fmap C . f)+ where+ go :: [P a] -> Ps a+ go [] = Ps NilP [] (const Nothing)+ go (P p as f : xs) = case go xs of+ Ps ps' ass g' -> Ps (p :> ps') (as ++ ass) $ \v ->+ T <$> g' v <|> H <$> f v++-- * smart lam+lam :: P a -> Exp a -> Exp a+lam (P p _ f) t = Lam p (abstract f t)++-- * smart let+let_ :: Eq a => [(a, Exp a)] -> Exp a -> Exp a+let_ bs b = Let (Vector.fromList $ map (abstr . snd) bs) (abstr b)+ where vs = map fst bs+ abstr = abstract (`List.elemIndex` vs)++-- * Pat++-- ** A Kind of Shape++eqPat :: (Eq1 f) => (a -> b -> Bool) -> Pat i f a -> Pat i' f b -> Bool+eqPat _ VarP VarP = True+eqPat _ WildP WildP = True+eqPat eq (AsP p) (AsP q) = eqPat eq p q+eqPat eq (ConP g ps) (ConP h qs) = g == h && eqPats eq ps qs+eqPat eq (ViewP e p) (ViewP f q) = liftEq eq e f && eqPat eq p q+eqPat _ _ _ = False++-- The same as eqPat, but if the patterns are equal, it returns a+-- proof that their type arguments are the same.+eqPat' :: (Eq1 f) => (a -> a' -> Bool) -> Pat b f a -> Pat b' f a' -> Maybe (b :~: b')+eqPat' _ VarP VarP = Just Refl+eqPat' _ WildP WildP = Just Refl+eqPat' eq (AsP p) (AsP q) = do+ Refl <- eqPat' eq p q+ Just Refl+eqPat' eq (ConP g ps) (ConP h qs) = do+ guard (g == h)+ Refl <- eqPats' eq ps qs+ Just Refl+eqPat' eq (ViewP e p) (ViewP f q) = guard (liftEq eq e f) >> eqPat' eq p q+eqPat' _ _ _ = Nothing++instance Eq1 f => Eq1 (Pat b f) where liftEq = eqPat+instance (Eq1 f, Eq a) => Eq (Pat b f a) where (==) = eq1++instance (Show1 f, Show a) => Show (Pat b f a) where showsPrec = showsPrec1++instance Show1 f => Show1 (Pat b f) where+ liftShowsPrec _ _ _ VarP = showString "VarP"+ liftShowsPrec _ _ _ WildP = showString "WildP"+ liftShowsPrec s sl d (AsP p) = showParen (d > 10) $ showString "AsP " . liftShowsPrec s sl 11 p+ liftShowsPrec s sl d (ConP g ps) = showParen (d > 10) $ showString "ConP " . showsPrec 11 g . showChar ' ' . liftShowsPrec s sl 11 ps+ liftShowsPrec s sl d (ViewP e p) = showParen (d > 10) $ showString "ViewP " . liftShowsPrec s sl 11 e . showChar ' ' . liftShowsPrec s sl 11 p++instance Functor f => Functor (Pat b f) where+ fmap _ VarP = VarP+ fmap _ WildP = WildP+ fmap f (AsP p) = AsP (fmap f p)+ fmap f (ConP g ps) = ConP g (fmap f ps)+ fmap f (ViewP e p) = ViewP (fmap f e) (fmap f p)++instance Foldable f => Foldable (Pat b f) where+ foldMap f (AsP p) = foldMap f p+ foldMap f (ConP _g ps) = foldMap f ps+ foldMap f (ViewP e p) = foldMap f e `mappend` foldMap f p+ foldMap _ _ = mempty++instance Traversable f => Traversable (Pat b f) where+ traverse _ VarP = pure VarP+ traverse _ WildP = pure WildP+ traverse f (AsP p) = AsP <$> traverse f p+ traverse f (ConP g ps) = ConP g <$> traverse f ps+ traverse f (ViewP e p) = ViewP <$> traverse f e <*> traverse f p++instance Bound (Pat b) where+ VarP >>>= _ = VarP+ WildP >>>= _ = WildP+ AsP p >>>= f = AsP (p >>>= f)+ ConP g ps >>>= f = ConP g (ps >>>= f)+ ViewP e p >>>= f = ViewP (e >>= f) (p >>>= f)++-- ** Pats+eqPats :: (Eq1 f) => (a -> b -> Bool) -> Pats bs f a -> Pats bs' f b -> Bool+eqPats _ NilP NilP = True+eqPats eq (p :> ps) (q :> qs) = eqPat eq p q && eqPats eq ps qs+eqPats _ _ _ = False++-- Like eqPats, but if the patses are equal, it returns a proof that their+-- type arguments are the same.+eqPats' :: (Eq1 f) => (a -> a' -> Bool) -> Pats bs f a -> Pats bs' f a' -> Maybe (bs :~: bs')+eqPats' _ NilP NilP = Just Refl+eqPats' eq (p :> ps) (q :> qs) = do+ Refl <- eqPat' eq p q+ Refl <- eqPats' eq ps qs+ Just Refl+eqPats' _ _ _ = Nothing++instance Eq1 f => Eq1 (Pats bs f) where liftEq = eqPats+instance (Eq1 f, Eq a) => Eq (Pats bs f a) where (==) = eq1++instance (Show1 f, Show a) => Show (Pats bs f a) where showsPrec = showsPrec1+instance Show1 f => Show1 (Pats bs f) where+ liftShowsPrec _ _ _ NilP = showString "NilP"+ liftShowsPrec s sl d (p :> ps) = showParen (d > 5) $+ liftShowsPrec s sl 6 p . showString " :> " . liftShowsPrec s sl 5 ps++instance Functor f => Functor (Pats bs f) where+ fmap _ NilP = NilP+ fmap f (p :> ps) = fmap f p :> fmap f ps++instance Foldable f => Foldable (Pats bs f) where+ foldMap f (p :> ps) = foldMap f p `mappend` foldMap f ps+ foldMap _ _ = mempty++instance Traversable f => Traversable (Pats bs f) where+ traverse _f NilP = pure NilP+ traverse f (p :> ps) = (:>) <$> traverse f p <*> traverse f ps++instance Bound (Pats bs) where+ NilP >>>= _ = NilP+ (p :> ps) >>>= f = (p >>>= f) :> (ps >>>= f)++-- ** Path into Pats+-- Internally, this is only used to implement eqPath, which is only+-- used to implement this.+eqMPath :: MPath is -> MPath js -> Bool+eqMPath (H m) (H n) = eqPath m n+eqMPath (T p) (T q) = eqMPath p q+eqMPath _ _ = False++instance Eq (MPath is) where+ H m == H n = m == n+ T p == T q = p == q+ _ == _ = False++-- Internally, this is only used to define comparePath, which+-- is only used here to define this.+compareMPath :: MPath is -> MPath js -> Ordering+compareMPath (H m) (H n) = comparePath m n+compareMPath (H _) (T _) = LT+compareMPath (T p) (T q) = compareMPath p q+compareMPath (T _) (H _) = GT++instance Ord (MPath is) where+ compare (H m) (H n) = compare m n+ compare (H _) (T _) = LT+ compare (T p) (T q) = compare p q+ compare (T _) (H _) = GT++instance Show (MPath is) where+ showsPrec d (H m) = showParen (d > 10) $ showString "H " . showsPrec 11 m+ showsPrec d (T p) = showParen (d > 10) $ showString "T " . showsPrec 11 p++-- instance Read (MPath is)++-- ** Path into Pat+-- Internally, this is only used to implement eqMPath, which is only used+-- to implement this.+eqPath :: Path i -> Path j -> Bool+eqPath V V = True+eqPath L L = True+eqPath (R m) (R n) = eqPath m n+eqPath (C p) (C q) = eqMPath p q+eqPath _ _ = False++instance Eq (Path i) where+ p == q = case compare p q of+ EQ -> True+ _ -> False++-- Internally, this is only used to define compareMPath, which+-- is only used here to define this.+comparePath :: Path i -> Path j -> Ordering+comparePath V V = EQ+comparePath V _ = LT+comparePath L V = GT+comparePath L L = EQ+comparePath L _ = LT+comparePath (R _) V = GT+comparePath (R _) L = GT+comparePath (R m) (R n) = comparePath m n+comparePath (R _) (C _) = LT+comparePath (C p) (C q) = compareMPath p q+comparePath (C _) _ = GT++instance Ord (Path i) where+ compare V y = case (y :: Path 'VarI) of V -> EQ+ compare L y = cpL y+ where+ cpL :: Path ('AsI a) -> Ordering+ cpL L = EQ+ cpL (R _) = LT+ compare (R r) y = cpR r y+ where+ cpR :: Path a -> Path ('AsI a) -> Ordering+ cpR _ L = GT+ cpR m (R n) = compare m n+ compare (C c) y = cpC c y+ where+ cpC :: MPath as -> Path ('ConI as) -> Ordering+ cpC p (C q) = compare p q++instance Show (Path i) where+ showsPrec _ V = showString "V"+ showsPrec _ L = showString "L"+ showsPrec d (R m) = showParen (d > 10) $ showString "R " . showsPrec 11 m+ showsPrec d (C p) = showParen (d > 10) $ showString "C " . showsPrec 11 p++-- |+-- >>> let_ [("x",Var "y"),("y",Var "x" :@ Var "y")] $ lam (varp "z") (Var "z" :@ Var "y")+-- Let (fromList [Scope (Var (B 1)),Scope (Var (B 0) :@ Var (B 1))]) (Scope (Lam VarP (Scope (Var (B V) :@ Var (F (Var (B 1)))))))+--+-- >>> lam (varp "x") (Var "x")+-- Lam VarP (Scope (Var (B V)))+--+-- >>> lam (conp "Hello" [varp "x", wildp]) (Var "y")+-- Lam (ConP "Hello" (VarP :> WildP :> NilP)) (Scope (Var (F (Var "y"))))+main :: IO ()+main = return ()
examples/Simple.hs view
@@ -1,183 +1,183 @@-{-# LANGUAGE CPP, TemplateHaskell #-} -module Main where - --- this is a simple example where lambdas only bind a single variable at a time --- this directly corresponds to the usual de bruijn presentation - -import Data.List (elemIndex) -import Data.Foldable hiding (notElem) -import Data.Maybe (fromJust) -import Data.Traversable -import Control.Monad -import Control.Applicative -import Prelude hiding (foldr,abs) -import Data.Deriving (deriveEq1, deriveOrd1, deriveRead1, deriveShow1) -import Data.Functor.Classes -import Bound -import System.Exit - - -infixl 9 :@ - -data Exp a - = V a - | Exp a :@ Exp a - | Lam (Scope () Exp a) - | Let [Scope Int Exp a] (Scope Int Exp a) - --- | A smart constructor for Lam --- --- >>> lam "y" (lam "x" (V "x" :@ V "y")) --- Lam (Scope (Lam (Scope (V (B ()) :@ V (F (V (B ()))))))) -lam :: Eq a => a -> Exp a -> Exp a -lam v b = Lam (abstract1 v b) - --- | A smart constructor for Let bindings - -let_ :: Eq a => [(a,Exp a)] -> Exp a -> Exp a -let_ [] b = b -let_ bs b = Let (map (abstr . snd) bs) (abstr b) - where abstr = abstract (`elemIndex` map fst bs) - -instance Functor Exp where fmap = fmapDefault -instance Foldable Exp where foldMap = foldMapDefault - -instance Applicative Exp where - pure = V - (<*>) = ap - -instance Traversable Exp where - traverse f (V a) = V <$> f a - traverse f (x :@ y) = (:@) <$> traverse f x <*> traverse f y - traverse f (Lam e) = Lam <$> traverse f e - traverse f (Let bs b) = Let <$> traverse (traverse f) bs <*> traverse f b - -instance Monad Exp where -#if !(MIN_VERSION_base(4,11,0)) - return = V -#endif - V a >>= f = f a - (x :@ y) >>= f = (x >>= f) :@ (y >>= f) - Lam e >>= f = Lam (e >>>= f) - Let bs b >>= f = Let (map (>>>= f) bs) (b >>>= f) - -fmap concat $ sequence - [ deriveEq1 ''Exp - , deriveOrd1 ''Exp - , deriveRead1 ''Exp - , deriveShow1 ''Exp - , [d| instance Eq a => Eq (Exp a) where (==) = eq1 - instance Ord a => Ord (Exp a) where compare = compare1 - instance Show a => Show (Exp a) where showsPrec = showsPrec1 - instance Read a => Read (Exp a) where readsPrec = readsPrec1 - |] - ] - --- | Compute the normal form of an expression -nf :: Exp a -> Exp a -nf e@V{} = e -nf (Lam b) = Lam $ toScope $ nf $ fromScope b -nf (f :@ a) = case whnf f of - Lam b -> nf (instantiate1 a b) - f' -> nf f' :@ nf a -nf (Let bs b) = nf (inst b) - where es = map inst bs - inst = instantiate (es !!) - --- | Reduce a term to weak head normal form -whnf :: Exp a -> Exp a -whnf e@V{} = e -whnf e@Lam{} = e -whnf (f :@ a) = case whnf f of - Lam b -> whnf (instantiate1 a b) - f' -> f' :@ a -whnf (Let bs b) = whnf (inst b) - where es = map inst bs - inst = instantiate (es !!) - -infixr 0 ! -(!) :: Eq a => a -> Exp a -> Exp a -(!) = lam - --- | Lennart Augustsson's example from "The Lambda Calculus Cooked 4 Ways" --- --- Modified to use recursive let, because we can. --- --- >>> nf cooked == true --- True - -true :: Exp String -true = lam "F" $ lam "T" $ V"T" - -cooked :: Exp a -cooked = fromJust $ closed $ let_ - [ ("False", "f" ! "t" ! V"f") - , ("True", "f" ! "t" ! V"t") - , ("if", "b" ! "t" ! "f" ! V"b" :@ V"f" :@ V"t") - , ("Zero", "z" ! "s" ! V"z") - , ("Succ", "n" ! "z" ! "s" ! V"s" :@ V"n") - , ("one", V"Succ" :@ V"Zero") - , ("two", V"Succ" :@ V"one") - , ("three", V"Succ" :@ V"two") - , ("isZero", "n" ! V"n" :@ V"True" :@ ("m" ! V"False")) - , ("const", "x" ! "y" ! V"x") - , ("Pair", "a" ! "b" ! "p" ! V"p" :@ V"a" :@ V"b") - , ("fst", "ab" ! V"ab" :@ ("a" ! "b" ! V"a")) - , ("snd", "ab" ! V"ab" :@ ("a" ! "b" ! V"b")) - -- we have a lambda calculus extended with recursive bindings, so we don't need to use fix - , ("add", "x" ! "y" ! V"x" :@ V"y" :@ ("n" ! V"Succ" :@ (V"add" :@ V"n" :@ V"y"))) - , ("mul", "x" ! "y" ! V"x" :@ V"Zero" :@ ("n" ! V"add" :@ V"y" :@ (V"mul" :@ V"n" :@ V"y"))) - , ("fac", "x" ! V"x" :@ V"one" :@ ("n" ! V"mul" :@ V"x" :@ (V"fac" :@ V"n"))) - , ("eqnat", "x" ! "y" ! V"x" :@ (V"y" :@ V"True" :@ (V"const" :@ V"False")) :@ ("x1" ! V"y" :@ V"False" :@ ("y1" ! V"eqnat" :@ V"x1" :@ V"y1"))) - , ("sumto", "x" ! V"x" :@ V"Zero" :@ ("n" ! V"add" :@ V"x" :@ (V"sumto" :@ V"n"))) - -- but we could if we wanted to - -- , ("fix", "g" ! ("x" ! V"g":@ (V"x":@V"x")) :@ ("x" ! V"g":@ (V"x":@V"x"))) - -- , ("add", V"fix" :@ ("radd" ! "x" ! "y" ! V"x" :@ V"y" :@ ("n" ! V"Succ" :@ (V"radd" :@ V"n" :@ V"y")))) - -- , ("mul", V"fix" :@ ("rmul" ! "x" ! "y" ! V"x" :@ V"Zero" :@ ("n" ! V"add" :@ V"y" :@ (V"rmul" :@ V"n" :@ V"y")))) - -- , ("fac", V"fix" :@ ("rfac" ! "x" ! V"x" :@ V"one" :@ ("n" ! V"mul" :@ V"x" :@ (V"rfac" :@ V"n")))) - -- , ("eqnat", V"fix" :@ ("reqnat" ! "x" ! "y" ! V"x" :@ (V"y" :@ V"True" :@ (V"const" :@ V"False")) :@ ("x1" ! V"y" :@ V"False" :@ ("y1" ! V"reqnat" :@ V"x1" :@ V"y1")))) - -- , ("sumto", V"fix" :@ ("rsumto" ! "x" ! V"x" :@ V"Zero" :@ ("n" ! V"add" :@ V"x" :@ (V"rsumto" :@ V"n")))) - , ("n5", V"add" :@ V"two" :@ V"three") - , ("n6", V"add" :@ V"three" :@ V"three") - , ("n17", V"add" :@ V"n6" :@ (V"add" :@ V"n6" :@ V"n5")) - , ("n37", V"Succ" :@ (V"mul" :@ V"n6" :@ V"n6")) - , ("n703", V"sumto" :@ V"n37") - , ("n720", V"fac" :@ V"n6") - ] (V"eqnat" :@ V"n720" :@ (V"add" :@ V"n703" :@ V"n17")) - --- TODO: use a real pretty printer - -prettyPrec :: [String] -> Bool -> Int -> Exp String -> ShowS -prettyPrec _ _ _ (V a) = showString a -prettyPrec vs d n (x :@ y) = showParen d $ - prettyPrec vs False n x . showChar ' ' . prettyPrec vs True n y -prettyPrec (v:vs) d n (Lam b) = showParen d $ - showString v . showString ". " . prettyPrec vs False n (instantiate1 (V v) b) -prettyPrec [] _ _ (Lam _) = error "Ran out of variable names" -prettyPrec vs d n (Let bs b) = showParen d $ - showString "let" . foldr (.) id (zipWith showBinding xs bs) . - showString " in " . indent . prettyPrec ys False n (inst b) - where (xs,ys) = splitAt (length bs) vs - inst = instantiate (\n' -> V (xs !! n')) - indent = showString ('\n' : replicate (n + 4) ' ') - showBinding x b' = indent . showString x . showString " = " . prettyPrec ys False (n + 4) (inst b') - -prettyWith :: [String] -> Exp String -> String -prettyWith vs t = prettyPrec (filter (`notElem` toList t) vs) False 0 t "" - -pretty :: Exp String -> String -pretty = prettyWith $ [ [i] | i <- ['a'..'z']] ++ [i : show j | j <- [1 :: Int ..], i <- ['a'..'z'] ] - -pp :: Exp String -> IO () -pp = putStrLn . pretty - -main :: IO () -main = do - pp cooked - let result = nf cooked - if result == true - then putStrLn "Result correct." - else do - putStrLn "Unexpected result:" - pp result - exitFailure +{-# LANGUAGE CPP, TemplateHaskell #-}+module Main where++-- this is a simple example where lambdas only bind a single variable at a time+-- this directly corresponds to the usual de bruijn presentation++import Data.List (elemIndex)+import Data.Foldable hiding (notElem)+import Data.Maybe (fromJust)+import Data.Traversable+import Control.Monad+import Control.Applicative+import Prelude hiding (foldr,abs)+import Data.Deriving (deriveEq1, deriveOrd1, deriveRead1, deriveShow1)+import Data.Functor.Classes+import Bound+import System.Exit+++infixl 9 :@++data Exp a+ = V a+ | Exp a :@ Exp a+ | Lam (Scope () Exp a)+ | Let [Scope Int Exp a] (Scope Int Exp a)++-- | A smart constructor for Lam+--+-- >>> lam "y" (lam "x" (V "x" :@ V "y"))+-- Lam (Scope (Lam (Scope (V (B ()) :@ V (F (V (B ())))))))+lam :: Eq a => a -> Exp a -> Exp a+lam v b = Lam (abstract1 v b)++-- | A smart constructor for Let bindings++let_ :: Eq a => [(a,Exp a)] -> Exp a -> Exp a+let_ [] b = b+let_ bs b = Let (map (abstr . snd) bs) (abstr b)+ where abstr = abstract (`elemIndex` map fst bs)++instance Functor Exp where fmap = fmapDefault+instance Foldable Exp where foldMap = foldMapDefault++instance Applicative Exp where+ pure = V+ (<*>) = ap++instance Traversable Exp where+ traverse f (V a) = V <$> f a+ traverse f (x :@ y) = (:@) <$> traverse f x <*> traverse f y+ traverse f (Lam e) = Lam <$> traverse f e+ traverse f (Let bs b) = Let <$> traverse (traverse f) bs <*> traverse f b++instance Monad Exp where+#if !(MIN_VERSION_base(4,11,0))+ return = V+#endif+ V a >>= f = f a+ (x :@ y) >>= f = (x >>= f) :@ (y >>= f)+ Lam e >>= f = Lam (e >>>= f)+ Let bs b >>= f = Let (map (>>>= f) bs) (b >>>= f)++fmap concat $ sequence+ [ deriveEq1 ''Exp+ , deriveOrd1 ''Exp+ , deriveRead1 ''Exp+ , deriveShow1 ''Exp+ , [d| instance Eq a => Eq (Exp a) where (==) = eq1+ instance Ord a => Ord (Exp a) where compare = compare1+ instance Show a => Show (Exp a) where showsPrec = showsPrec1+ instance Read a => Read (Exp a) where readsPrec = readsPrec1+ |]+ ]++-- | Compute the normal form of an expression+nf :: Exp a -> Exp a+nf e@V{} = e+nf (Lam b) = Lam $ toScope $ nf $ fromScope b+nf (f :@ a) = case whnf f of+ Lam b -> nf (instantiate1 a b)+ f' -> nf f' :@ nf a+nf (Let bs b) = nf (inst b)+ where es = map inst bs+ inst = instantiate (es !!)++-- | Reduce a term to weak head normal form+whnf :: Exp a -> Exp a+whnf e@V{} = e+whnf e@Lam{} = e+whnf (f :@ a) = case whnf f of+ Lam b -> whnf (instantiate1 a b)+ f' -> f' :@ a+whnf (Let bs b) = whnf (inst b)+ where es = map inst bs+ inst = instantiate (es !!)++infixr 0 !+(!) :: Eq a => a -> Exp a -> Exp a+(!) = lam++-- | Lennart Augustsson's example from "The Lambda Calculus Cooked 4 Ways"+--+-- Modified to use recursive let, because we can.+--+-- >>> nf cooked == true+-- True++true :: Exp String+true = lam "F" $ lam "T" $ V"T"++cooked :: Exp a+cooked = fromJust $ closed $ let_+ [ ("False", "f" ! "t" ! V"f")+ , ("True", "f" ! "t" ! V"t")+ , ("if", "b" ! "t" ! "f" ! V"b" :@ V"f" :@ V"t")+ , ("Zero", "z" ! "s" ! V"z")+ , ("Succ", "n" ! "z" ! "s" ! V"s" :@ V"n")+ , ("one", V"Succ" :@ V"Zero")+ , ("two", V"Succ" :@ V"one")+ , ("three", V"Succ" :@ V"two")+ , ("isZero", "n" ! V"n" :@ V"True" :@ ("m" ! V"False"))+ , ("const", "x" ! "y" ! V"x")+ , ("Pair", "a" ! "b" ! "p" ! V"p" :@ V"a" :@ V"b")+ , ("fst", "ab" ! V"ab" :@ ("a" ! "b" ! V"a"))+ , ("snd", "ab" ! V"ab" :@ ("a" ! "b" ! V"b"))+ -- we have a lambda calculus extended with recursive bindings, so we don't need to use fix+ , ("add", "x" ! "y" ! V"x" :@ V"y" :@ ("n" ! V"Succ" :@ (V"add" :@ V"n" :@ V"y")))+ , ("mul", "x" ! "y" ! V"x" :@ V"Zero" :@ ("n" ! V"add" :@ V"y" :@ (V"mul" :@ V"n" :@ V"y")))+ , ("fac", "x" ! V"x" :@ V"one" :@ ("n" ! V"mul" :@ V"x" :@ (V"fac" :@ V"n")))+ , ("eqnat", "x" ! "y" ! V"x" :@ (V"y" :@ V"True" :@ (V"const" :@ V"False")) :@ ("x1" ! V"y" :@ V"False" :@ ("y1" ! V"eqnat" :@ V"x1" :@ V"y1")))+ , ("sumto", "x" ! V"x" :@ V"Zero" :@ ("n" ! V"add" :@ V"x" :@ (V"sumto" :@ V"n")))+ -- but we could if we wanted to+ -- , ("fix", "g" ! ("x" ! V"g":@ (V"x":@V"x")) :@ ("x" ! V"g":@ (V"x":@V"x")))+ -- , ("add", V"fix" :@ ("radd" ! "x" ! "y" ! V"x" :@ V"y" :@ ("n" ! V"Succ" :@ (V"radd" :@ V"n" :@ V"y"))))+ -- , ("mul", V"fix" :@ ("rmul" ! "x" ! "y" ! V"x" :@ V"Zero" :@ ("n" ! V"add" :@ V"y" :@ (V"rmul" :@ V"n" :@ V"y"))))+ -- , ("fac", V"fix" :@ ("rfac" ! "x" ! V"x" :@ V"one" :@ ("n" ! V"mul" :@ V"x" :@ (V"rfac" :@ V"n"))))+ -- , ("eqnat", V"fix" :@ ("reqnat" ! "x" ! "y" ! V"x" :@ (V"y" :@ V"True" :@ (V"const" :@ V"False")) :@ ("x1" ! V"y" :@ V"False" :@ ("y1" ! V"reqnat" :@ V"x1" :@ V"y1"))))+ -- , ("sumto", V"fix" :@ ("rsumto" ! "x" ! V"x" :@ V"Zero" :@ ("n" ! V"add" :@ V"x" :@ (V"rsumto" :@ V"n"))))+ , ("n5", V"add" :@ V"two" :@ V"three")+ , ("n6", V"add" :@ V"three" :@ V"three")+ , ("n17", V"add" :@ V"n6" :@ (V"add" :@ V"n6" :@ V"n5"))+ , ("n37", V"Succ" :@ (V"mul" :@ V"n6" :@ V"n6"))+ , ("n703", V"sumto" :@ V"n37")+ , ("n720", V"fac" :@ V"n6")+ ] (V"eqnat" :@ V"n720" :@ (V"add" :@ V"n703" :@ V"n17"))++-- TODO: use a real pretty printer++prettyPrec :: [String] -> Bool -> Int -> Exp String -> ShowS+prettyPrec _ _ _ (V a) = showString a+prettyPrec vs d n (x :@ y) = showParen d $+ prettyPrec vs False n x . showChar ' ' . prettyPrec vs True n y+prettyPrec (v:vs) d n (Lam b) = showParen d $+ showString v . showString ". " . prettyPrec vs False n (instantiate1 (V v) b)+prettyPrec [] _ _ (Lam _) = error "Ran out of variable names"+prettyPrec vs d n (Let bs b) = showParen d $+ showString "let" . foldr (.) id (zipWith showBinding xs bs) .+ showString " in " . indent . prettyPrec ys False n (inst b)+ where (xs,ys) = splitAt (length bs) vs+ inst = instantiate (\n' -> V (xs !! n'))+ indent = showString ('\n' : replicate (n + 4) ' ')+ showBinding x b' = indent . showString x . showString " = " . prettyPrec ys False (n + 4) (inst b')++prettyWith :: [String] -> Exp String -> String+prettyWith vs t = prettyPrec (filter (`notElem` toList t) vs) False 0 t ""++pretty :: Exp String -> String+pretty = prettyWith $ [ [i] | i <- ['a'..'z']] ++ [i : show j | j <- [1 :: Int ..], i <- ['a'..'z'] ]++pp :: Exp String -> IO ()+pp = putStrLn . pretty++main :: IO ()+main = do+ pp cooked+ let result = nf cooked+ if result == true+ then putStrLn "Result correct."+ else do+ putStrLn "Unexpected result:"+ pp result+ exitFailure
src/Bound.hs view
@@ -1,146 +1,146 @@-{-# LANGUAGE CPP #-} - ------------------------------------------------------------------------------ --- | --- Copyright : (C) 2012 Edward Kmett --- License : BSD-style (see the file LICENSE) --- --- Maintainer : Edward Kmett <ekmett@gmail.com> --- Stability : experimental --- Portability : portable --- --- We represent the target language itself as an ideal monad supplied by the --- user, and provide a 'Scope' monad transformer for introducing bound --- variables in user supplied terms. Users supply a 'Monad' and 'Traversable' --- instance, and we traverse to find free variables, and use the 'Monad' to --- perform substitution that avoids bound variables. --- --- An untyped lambda calculus: --- --- @ --- {-\# LANGUAGE DeriveFunctor, DeriveFoldable, DeriveTraversable, TemplateHaskell \#-} --- import Bound --- import Control.Applicative --- import Control.Monad ('Control.Monad.ap') --- import Data.Functor.Classes --- import Data.Foldable --- import Data.Traversable --- -- This is from deriving-compat package --- import Data.Deriving (deriveEq1, deriveOrd1, deriveRead1, deriveShow1) --- @ --- --- @ --- infixl 9 :\@ --- data Exp a = V a | Exp a :\@ Exp a | Lam ('Scope' () Exp a) --- deriving ('Functor','Data.Foldable.Foldable','Data.Foldable.Traversable') --- @ --- --- @ --- instance 'Control.Applicative.Applicative' Exp where 'Control.Applicative.pure' = V; ('<*>') = 'Control.Monad.ap' --- instance 'Monad' Exp where --- 'return' = V --- V a '>>=' f = f a --- (x :\@ y) '>>=' f = (x '>>=' f) :\@ (y '>>=' f) --- Lam e '>>=' f = Lam (e '>>>=' f) --- @ --- --- @ --- concat <$> sequence --- [ deriveEq1 ''Exp --- , deriveOrd1 ''Exp --- , deriveRead1 ''Exp --- , deriveShow1 ''Exp --- --- , [d| instance 'Eq' a => 'Eq' (Exp a) where (==) = eq1 --- instance 'Ord' a => 'Ord' (Exp a) where compare = compare1 --- instance 'Show' a => 'Show' (Exp a) where showsPrec = showsPrec1 --- instance 'Read' a => 'Read' (Exp a) where readsPrec = readsPrec1 --- |] --- ] --- @ --- --- @ --- lam :: 'Eq' a => a -> 'Exp' a -> 'Exp' a --- lam v b = Lam ('abstract1' v b) --- @ --- --- @ --- whnf :: 'Exp' a -> 'Exp' a --- whnf (f :\@ a) = case whnf f of --- Lam b -> whnf ('instantiate1' a b) --- f' -> f' :\@ a --- whnf e = e --- @ --- --- More exotic combinators for manipulating a 'Scope' can be imported from --- "Bound.Scope". --- --- You can also retain names in your bound variables by using 'Bound.Name.Name' --- and the related combinators from "Bound.Name". They are not re-exported --- from this module by default. --- --- The approach used in this package was first elaborated upon by Richard Bird --- and Ross Patterson --- in \"de Bruijn notation as a nested data type\", available from --- <http://www.cs.uwyo.edu/~jlc/courses/5000_fall_08/debruijn_as_nested_datatype.pdf> --- --- However, the combinators they used required higher rank types. Here we --- demonstrate that the higher rank @gfold@ combinator they used isn't necessary --- to build the monad and use a monad transformer to encapsulate the novel --- recursion pattern in their generalized de Bruijn representation. It is named --- 'Scope' to match up with the terminology and usage pattern from Conor McBride --- and James McKinna's \"I am not a number: I am a free variable\", available --- from <http://www.cs.ru.nl/~james/RESEARCH/haskell2004.pdf>, but since --- the set of variables is visible in the type, we can provide stronger type --- safety guarantees. --- --- There are longer examples in the @examples/@ folder: --- --- <https://github.com/ekmett/bound/tree/master/examples> --- --- (1) /Simple.hs/ provides an untyped lambda calculus with recursive let --- bindings and includes an evaluator for the untyped lambda calculus and a --- longer example taken from Lennart Augustsson's "λ-calculus cooked four --- ways" available from <http://foswiki.cs.uu.nl/foswiki/pub/USCS/InterestingPapers/AugustsonLambdaCalculus.pdf> --- --- 2. /Derived.hs/ shows how much of the API can be automated with --- DeriveTraversable and adds combinators for building binders that support --- pattern matching. --- --- 3. /Overkill.hs/ provides very strongly typed pattern matching many modern --- language extensions, including polymorphic kinds to ensure type safety. --- In general, the approach taken by Derived seems to deliver a better power --- to weight ratio. ----------------------------------------------------------------------------- -module Bound - ( - -- * Manipulating user terms - substitute - , isClosed - , closed - -- * Scopes introduce bound variables - , Scope(..) - -- ** Abstraction over bound variables - , abstract, abstract1 - -- ** Instantiation of bound variables - , instantiate, instantiate1 - -- * Structures permitting substitution - , Bound(..) - , (=<<<) - -- * Conversion to Traditional de Bruijn - , Var(..) - , fromScope - , toScope -#ifdef MIN_VERSION_template_haskell - -- * Deriving instances - , makeBound -#endif - ) where - -import Bound.Var -import Bound.Class -import Bound.Scope -import Bound.Term -#ifdef MIN_VERSION_template_haskell -import Bound.TH -#endif +{-# LANGUAGE CPP #-}++-----------------------------------------------------------------------------+-- |+-- Copyright : (C) 2012 Edward Kmett+-- License : BSD-style (see the file LICENSE)+--+-- Maintainer : Edward Kmett <ekmett@gmail.com>+-- Stability : experimental+-- Portability : portable+--+-- We represent the target language itself as an ideal monad supplied by the+-- user, and provide a 'Scope' monad transformer for introducing bound+-- variables in user supplied terms. Users supply a 'Monad' and 'Traversable'+-- instance, and we traverse to find free variables, and use the 'Monad' to+-- perform substitution that avoids bound variables.+--+-- An untyped lambda calculus:+--+-- @+-- {-\# LANGUAGE DeriveFunctor, DeriveFoldable, DeriveTraversable, TemplateHaskell \#-}+-- import Bound+-- import Control.Applicative+-- import Control.Monad ('Control.Monad.ap')+-- import Data.Functor.Classes+-- import Data.Foldable+-- import Data.Traversable+-- -- This is from deriving-compat package+-- import Data.Deriving (deriveEq1, deriveOrd1, deriveRead1, deriveShow1)+-- @+--+-- @+-- infixl 9 :\@+-- data Exp a = V a | Exp a :\@ Exp a | Lam ('Scope' () Exp a)+-- deriving ('Functor','Data.Foldable.Foldable','Data.Foldable.Traversable')+-- @+--+-- @+-- instance 'Control.Applicative.Applicative' Exp where 'Control.Applicative.pure' = V; ('<*>') = 'Control.Monad.ap'+-- instance 'Monad' Exp where+-- 'return' = V+-- V a '>>=' f = f a+-- (x :\@ y) '>>=' f = (x '>>=' f) :\@ (y '>>=' f)+-- Lam e '>>=' f = Lam (e '>>>=' f)+-- @+--+-- @+-- concat <$> sequence+-- [ deriveEq1 ''Exp+-- , deriveOrd1 ''Exp+-- , deriveRead1 ''Exp+-- , deriveShow1 ''Exp+--+-- , [d| instance 'Eq' a => 'Eq' (Exp a) where (==) = eq1+-- instance 'Ord' a => 'Ord' (Exp a) where compare = compare1+-- instance 'Show' a => 'Show' (Exp a) where showsPrec = showsPrec1+-- instance 'Read' a => 'Read' (Exp a) where readsPrec = readsPrec1+-- |]+-- ]+-- @+--+-- @+-- lam :: 'Eq' a => a -> 'Exp' a -> 'Exp' a+-- lam v b = Lam ('abstract1' v b)+-- @+--+-- @+-- whnf :: 'Exp' a -> 'Exp' a+-- whnf (f :\@ a) = case whnf f of+-- Lam b -> whnf ('instantiate1' a b)+-- f' -> f' :\@ a+-- whnf e = e+-- @+--+-- More exotic combinators for manipulating a 'Scope' can be imported from+-- "Bound.Scope".+--+-- You can also retain names in your bound variables by using 'Bound.Name.Name'+-- and the related combinators from "Bound.Name". They are not re-exported+-- from this module by default.+--+-- The approach used in this package was first elaborated upon by Richard Bird+-- and Ross Patterson+-- in \"de Bruijn notation as a nested data type\", available from+-- <http://www.cs.uwyo.edu/~jlc/courses/5000_fall_08/debruijn_as_nested_datatype.pdf>+--+-- However, the combinators they used required higher rank types. Here we+-- demonstrate that the higher rank @gfold@ combinator they used isn't necessary+-- to build the monad and use a monad transformer to encapsulate the novel+-- recursion pattern in their generalized de Bruijn representation. It is named+-- 'Scope' to match up with the terminology and usage pattern from Conor McBride+-- and James McKinna's \"I am not a number: I am a free variable\", available+-- from <http://www.cs.ru.nl/~james/RESEARCH/haskell2004.pdf>, but since+-- the set of variables is visible in the type, we can provide stronger type+-- safety guarantees.+--+-- There are longer examples in the @examples/@ folder:+--+-- <https://github.com/ekmett/bound/tree/master/examples>+--+-- (1) /Simple.hs/ provides an untyped lambda calculus with recursive let+-- bindings and includes an evaluator for the untyped lambda calculus and a+-- longer example taken from Lennart Augustsson's "λ-calculus cooked four+-- ways" available from <http://foswiki.cs.uu.nl/foswiki/pub/USCS/InterestingPapers/AugustsonLambdaCalculus.pdf>+--+-- 2. /Derived.hs/ shows how much of the API can be automated with+-- DeriveTraversable and adds combinators for building binders that support+-- pattern matching.+--+-- 3. /Overkill.hs/ provides very strongly typed pattern matching many modern+-- language extensions, including polymorphic kinds to ensure type safety.+-- In general, the approach taken by Derived seems to deliver a better power+-- to weight ratio.+----------------------------------------------------------------------------+module Bound+ (+ -- * Manipulating user terms+ substitute+ , isClosed+ , closed+ -- * Scopes introduce bound variables+ , Scope(..)+ -- ** Abstraction over bound variables+ , abstract, abstract1+ -- ** Instantiation of bound variables+ , instantiate, instantiate1+ -- * Structures permitting substitution+ , Bound(..)+ , (=<<<)+ -- * Conversion to Traditional de Bruijn+ , Var(..)+ , fromScope+ , toScope+#ifdef MIN_VERSION_template_haskell+ -- * Deriving instances+ , makeBound+#endif+ ) where++import Bound.Var+import Bound.Class+import Bound.Scope+import Bound.Term+#ifdef MIN_VERSION_template_haskell+import Bound.TH+#endif
src/Bound/Class.hs view
@@ -1,118 +1,118 @@-{-# LANGUAGE CPP #-} -#if defined(__GLASGOW_HASKELL__) -{-# LANGUAGE DefaultSignatures #-} -#endif -{-# OPTIONS -Wno-deprecations #-} ------------------------------------------------------------------------------ --- | --- Copyright : (C) 2012-2015 Edward Kmett --- License : BSD-style (see the file LICENSE) --- --- Maintainer : Edward Kmett <ekmett@gmail.com> --- Stability : experimental --- Portability : portable --- --- This module provides the 'Bound' class, for performing substitution into --- things that are not necessarily full monad transformers. ----------------------------------------------------------------------------- -module Bound.Class - ( Bound(..) - , (=<<<) - ) where - -import Control.Monad.Trans.Class -import Control.Monad.Trans.Cont -import Control.Monad.Trans.Identity -import Control.Monad.Trans.Maybe -import Control.Monad.Trans.RWS -import Control.Monad.Trans.Reader -import Control.Monad.Trans.State -import Control.Monad.Trans.Writer -#if !(MIN_VERSION_transformers(0,6,0)) -import Control.Monad.Trans.Error -import Control.Monad.Trans.List -#endif - -infixl 1 >>>= - --- | Instances of 'Bound' generate left modules over monads. --- --- This means they should satisfy the following laws: --- --- @ --- m '>>>=' 'return' ≡ m --- m '>>>=' (λ x → k x '>>=' h) ≡ (m '>>>=' k) '>>>=' h --- @ --- --- This guarantees that a typical Monad instance for an expression type --- where Bound instances appear will satisfy the Monad laws (see doc/BoundLaws.hs). --- --- If instances of 'Bound' are monad transformers, then @m '>>>=' f ≡ m '>>=' 'lift' '.' f@ --- implies the above laws, and is in fact the default definition. --- --- This is useful for types like expression lists, case alternatives, --- schemas, etc. that may not be expressions in their own right, but often --- contain expressions. --- --- /Note:/ 'Control.Monad.Free.Free' isn't "really" a monad transformer, even if --- the kind matches. Therefore there isn't @'Bound' 'Control.Monad.Free.Free'@ instance. -class Bound t where - -- | Perform substitution - -- - -- If @t@ is an instance of @MonadTrans@ and you are compiling on GHC >= 7.4, then this - -- gets the default definition: - -- - -- @m '>>>=' f = m '>>=' 'lift' '.' f@ - (>>>=) :: Monad f => t f a -> (a -> f c) -> t f c -#if defined(__GLASGOW_HASKELL__) - default (>>>=) :: (MonadTrans t, Monad f, Monad (t f)) => - t f a -> (a -> f c) -> t f c - m >>>= f = m >>= lift . f - {-# INLINE (>>>=) #-} -#endif - -instance Bound (ContT c) where - m >>>= f = m >>= lift . f - {-# INLINE (>>>=) #-} - -instance Bound IdentityT where - m >>>= f = m >>= lift . f - {-# INLINE (>>>=) #-} - -instance Bound MaybeT where - m >>>= f = m >>= lift . f - {-# INLINE (>>>=) #-} - -instance Monoid w => Bound (RWST r w s) where - m >>>= f = m >>= lift . f - {-# INLINE (>>>=) #-} - -instance Bound (ReaderT r) where - m >>>= f = m >>= lift . f - {-# INLINE (>>>=) #-} - -instance Bound (StateT s) where - m >>>= f = m >>= lift . f - {-# INLINE (>>>=) #-} - -instance Monoid w => Bound (WriterT w) where - m >>>= f = m >>= lift . f - {-# INLINE (>>>=) #-} - -#if !(MIN_VERSION_transformers(0,6,0)) -instance Error e => Bound (ErrorT e) where - m >>>= f = m >>= lift . f - {-# INLINE (>>>=) #-} - -instance Bound ListT where - m >>>= f = m >>= lift . f - {-# INLINE (>>>=) #-} -#endif - -infixr 1 =<<< --- | A flipped version of ('>>>='). --- --- @('=<<<') = 'flip' ('>>>=')@ -(=<<<) :: (Bound t, Monad f) => (a -> f c) -> t f a -> t f c -(=<<<) = flip (>>>=) -{-# INLINE (=<<<) #-} +{-# LANGUAGE CPP #-}+#if defined(__GLASGOW_HASKELL__)+{-# LANGUAGE DefaultSignatures #-}+#endif+{-# OPTIONS -Wno-deprecations #-}+-----------------------------------------------------------------------------+-- |+-- Copyright : (C) 2012-2015 Edward Kmett+-- License : BSD-style (see the file LICENSE)+--+-- Maintainer : Edward Kmett <ekmett@gmail.com>+-- Stability : experimental+-- Portability : portable+--+-- This module provides the 'Bound' class, for performing substitution into+-- things that are not necessarily full monad transformers.+----------------------------------------------------------------------------+module Bound.Class+ ( Bound(..)+ , (=<<<)+ ) where++import Control.Monad.Trans.Class+import Control.Monad.Trans.Cont+import Control.Monad.Trans.Identity+import Control.Monad.Trans.Maybe+import Control.Monad.Trans.RWS+import Control.Monad.Trans.Reader+import Control.Monad.Trans.State+import Control.Monad.Trans.Writer+#if !(MIN_VERSION_transformers(0,6,0))+import Control.Monad.Trans.Error+import Control.Monad.Trans.List+#endif++infixl 1 >>>=++-- | Instances of 'Bound' generate left modules over monads.+--+-- This means they should satisfy the following laws:+--+-- @+-- m '>>>=' 'return' ≡ m+-- m '>>>=' (λ x → k x '>>=' h) ≡ (m '>>>=' k) '>>>=' h+-- @+--+-- This guarantees that a typical Monad instance for an expression type+-- where Bound instances appear will satisfy the Monad laws (see doc/BoundLaws.hs).+--+-- If instances of 'Bound' are monad transformers, then @m '>>>=' f ≡ m '>>=' 'lift' '.' f@+-- implies the above laws, and is in fact the default definition.+--+-- This is useful for types like expression lists, case alternatives,+-- schemas, etc. that may not be expressions in their own right, but often+-- contain expressions.+--+-- /Note:/ 'Control.Monad.Free.Free' isn't "really" a monad transformer, even if+-- the kind matches. Therefore there isn't @'Bound' 'Control.Monad.Free.Free'@ instance.+class Bound t where+ -- | Perform substitution+ --+ -- If @t@ is an instance of @MonadTrans@ and you are compiling on GHC >= 7.4, then this+ -- gets the default definition:+ --+ -- @m '>>>=' f = m '>>=' 'lift' '.' f@+ (>>>=) :: Monad f => t f a -> (a -> f c) -> t f c+#if defined(__GLASGOW_HASKELL__)+ default (>>>=) :: (MonadTrans t, Monad f, Monad (t f)) =>+ t f a -> (a -> f c) -> t f c+ m >>>= f = m >>= lift . f+ {-# INLINE (>>>=) #-}+#endif++instance Bound (ContT c) where+ m >>>= f = m >>= lift . f+ {-# INLINE (>>>=) #-}++instance Bound IdentityT where+ m >>>= f = m >>= lift . f+ {-# INLINE (>>>=) #-}++instance Bound MaybeT where+ m >>>= f = m >>= lift . f+ {-# INLINE (>>>=) #-}++instance Monoid w => Bound (RWST r w s) where+ m >>>= f = m >>= lift . f+ {-# INLINE (>>>=) #-}++instance Bound (ReaderT r) where+ m >>>= f = m >>= lift . f+ {-# INLINE (>>>=) #-}++instance Bound (StateT s) where+ m >>>= f = m >>= lift . f+ {-# INLINE (>>>=) #-}++instance Monoid w => Bound (WriterT w) where+ m >>>= f = m >>= lift . f+ {-# INLINE (>>>=) #-}++#if !(MIN_VERSION_transformers(0,6,0))+instance Error e => Bound (ErrorT e) where+ m >>>= f = m >>= lift . f+ {-# INLINE (>>>=) #-}++instance Bound ListT where+ m >>>= f = m >>= lift . f+ {-# INLINE (>>>=) #-}+#endif++infixr 1 =<<<+-- | A flipped version of ('>>>=').+--+-- @('=<<<') = 'flip' ('>>>=')@+(=<<<) :: (Bound t, Monad f) => (a -> f c) -> t f a -> t f c+(=<<<) = flip (>>>=)+{-# INLINE (=<<<) #-}
src/Bound/Name.hs view
@@ -1,254 +1,254 @@-{-# LANGUAGE CPP #-} -#ifdef __GLASGOW_HASKELL__ -{-# LANGUAGE DeriveDataTypeable #-} -{-# LANGUAGE DeriveGeneric #-} -{-# LANGUAGE Trustworthy #-} -#endif - ------------------------------------------------------------------------------ --- | --- Copyright : (C) 2012 Edward Kmett --- License : BSD-style (see the file LICENSE) --- --- Maintainer : Edward Kmett <ekmett@gmail.com> --- Stability : experimental --- Portability : portable --- --- The problem with locally nameless approaches is that original names are --- often useful for error reporting, or to allow for the user in an interactive --- theorem prover to convey some hint about the domain. A @'Name' n b@ is a value --- @b@ supplemented with a (discardable) name that may be useful for error --- reporting purposes. In particular, this name does not participate in --- comparisons for equality. --- --- This module is /not/ exported from "Bound" by default. You need to explicitly --- import it, due to the fact that 'Name' is a pretty common term in other --- people's code. ----------------------------------------------------------------------------- -module Bound.Name - ( Name(..) - , _Name - , name - , abstractName - , abstract1Name - , abstractEitherName - , instantiateName - , instantiate1Name - , instantiateEitherName - ) where - -import Bound.Scope -import Bound.Var -import Control.Comonad -import Control.DeepSeq -import Control.Monad (liftM, liftM2) -import Data.Bifunctor -import Data.Bifoldable -import qualified Data.Binary as Binary -import Data.Binary (Binary) -import Data.Bitraversable -import Data.Bytes.Serial -import Data.Functor.Classes -#ifdef __GLASGOW_HASKELL__ -import Data.Data -import GHC.Generics -#endif -import Data.Hashable (Hashable(..)) -import Data.Hashable.Lifted (Hashable1(..), Hashable2(..)) -import Data.Profunctor -import qualified Data.Serialize as Serialize -import Data.Serialize (Serialize) - -------------------------------------------------------------------------------- --- Names -------------------------------------------------------------------------------- - --- | --- We track the choice of 'Name' @n@ as a forgettable property that does /not/ affect --- the result of ('==') or 'compare'. --- --- To compare names rather than values, use @('Data.Function.on' 'compare' 'name')@ instead. -data Name n b = Name n b deriving - ( Show - , Read -#ifdef __GLASGOW_HASKELL__ - , Data - , Generic - , Generic1 -#endif - ) - --- | Extract the 'name'. -name :: Name n b -> n -name (Name n _) = n -{-# INLINE name #-} - --- | --- --- This provides an 'Iso' that can be used to access the parts of a 'Name'. --- --- @ --- '_Name' :: Iso ('Name' n a) ('Name' m b) (n, a) (m, b) --- @ -_Name :: (Profunctor p, Functor f) => p (n, a) (f (m,b)) -> p (Name n a) (f (Name m b)) -_Name = dimap (\(Name n a) -> (n, a)) (fmap (uncurry Name)) -{-# INLINE _Name #-} - -------------------------------------------------------------------------------- --- Instances -------------------------------------------------------------------------------- - -instance Eq b => Eq (Name n b) where - Name _ a == Name _ b = a == b - {-# INLINE (==) #-} - -instance Hashable2 Name where - liftHashWithSalt2 _ h s (Name _ a) = h s a - {-# INLINE liftHashWithSalt2 #-} - -instance Hashable1 (Name n) where - liftHashWithSalt h s (Name _ a) = h s a - {-# INLINE liftHashWithSalt #-} - -instance Hashable a => Hashable (Name n a) where - hashWithSalt m (Name _ a) = hashWithSalt m a - {-# INLINE hashWithSalt #-} - -instance Ord b => Ord (Name n b) where - Name _ a `compare` Name _ b = compare a b - {-# INLINE compare #-} - -instance Functor (Name n) where - fmap f (Name n a) = Name n (f a) - {-# INLINE fmap #-} - -instance Foldable (Name n) where - foldMap f (Name _ a) = f a - {-# INLINE foldMap #-} - -instance Traversable (Name n) where - traverse f (Name n a) = Name n <$> f a - {-# INLINE traverse #-} - -instance Bifunctor Name where - bimap f g (Name n a) = Name (f n) (g a) - {-# INLINE bimap #-} - -instance Bifoldable Name where - bifoldMap f g (Name n a) = f n `mappend` g a - {-# INLINE bifoldMap #-} - -instance Bitraversable Name where - bitraverse f g (Name n a) = Name <$> f n <*> g a - {-# INLINE bitraverse #-} - -instance Comonad (Name n) where - extract (Name _ b) = b - {-# INLINE extract #-} - extend f w@(Name n _) = Name n (f w) - {-# INLINE extend #-} - -instance Eq2 Name where - liftEq2 _ g (Name _ b) (Name _ d) = g b d - -instance Ord2 Name where - liftCompare2 _ g (Name _ b) (Name _ d) = g b d - -instance Show2 Name where - liftShowsPrec2 f _ h _ d (Name a b) = showsBinaryWith f h "Name" d a b - -instance Read2 Name where - liftReadsPrec2 f _ h _ = readsData $ readsBinaryWith f h "Name" Name - -instance Eq1 (Name b) where - liftEq f (Name _ b) (Name _ d) = f b d - -instance Ord1 (Name b) where - liftCompare f (Name _ b) (Name _ d) = f b d - -instance Show b => Show1 (Name b) where - liftShowsPrec f _ d (Name a b) = showsBinaryWith showsPrec f "Name" d a b - -instance Read b => Read1 (Name b) where - liftReadsPrec f _ = readsData $ readsBinaryWith readsPrec f "Name" Name - -instance Serial2 Name where - serializeWith2 pb pf (Name b a) = pb b >> pf a - {-# INLINE serializeWith2 #-} - - deserializeWith2 = liftM2 Name - {-# INLINE deserializeWith2 #-} - -instance Serial b => Serial1 (Name b) where - serializeWith = serializeWith2 serialize - {-# INLINE serializeWith #-} - deserializeWith = deserializeWith2 deserialize - {-# INLINE deserializeWith #-} - -instance (Serial b, Serial a) => Serial (Name b a) where - serialize = serializeWith2 serialize serialize - {-# INLINE serialize #-} - deserialize = deserializeWith2 deserialize deserialize - {-# INLINE deserialize #-} - -instance (Binary b, Binary a) => Binary (Name b a) where - put = serializeWith2 Binary.put Binary.put - get = deserializeWith2 Binary.get Binary.get - -instance (Serialize b, Serialize a) => Serialize (Name b a) where - put = serializeWith2 Serialize.put Serialize.put - get = deserializeWith2 Serialize.get Serialize.get - -instance (NFData b, NFData a) => NFData (Name b a) where - rnf (Name a b) = rnf a `seq` rnf b - -------------------------------------------------------------------------------- --- Abstraction -------------------------------------------------------------------------------- - --- | Abstraction, capturing named bound variables. -abstractName :: Monad f => (a -> Maybe b) -> f a -> Scope (Name a b) f a -abstractName f t = Scope (liftM k t) where - k a = case f a of - Just b -> B (Name a b) - Nothing -> F (return a) -{-# INLINE abstractName #-} - --- | Abstract over a single variable -abstract1Name :: (Monad f, Eq a) => a -> f a -> Scope (Name a ()) f a -abstract1Name a = abstractName (\b -> if a == b then Just () else Nothing) -{-# INLINE abstract1Name #-} - --- | Capture some free variables in an expression to yield --- a 'Scope' with named bound variables. Optionally change the --- types of the remaining free variables. -abstractEitherName :: Monad f => (a -> Either b c) -> f a -> Scope (Name a b) f c -abstractEitherName f e = Scope (liftM k e) where - k y = case f y of - Left z -> B (Name y z) - Right y' -> F (return y') - -------------------------------------------------------------------------------- --- Instantiation -------------------------------------------------------------------------------- - --- | Enter a scope, instantiating all bound variables, but discarding (comonadic) --- meta data, like its name -instantiateName :: (Monad f, Comonad n) => (b -> f a) -> Scope (n b) f a -> f a -instantiateName k e = unscope e >>= \v -> case v of - B b -> k (extract b) - F a -> a -{-# INLINE instantiateName #-} - --- | Enter a 'Scope' that binds one (named) variable, instantiating it. --- --- @'instantiate1Name' = 'instantiate1'@ -instantiate1Name :: Monad f => f a -> Scope n f a -> f a -instantiate1Name = instantiate1 -{-# INLINE instantiate1Name #-} - -instantiateEitherName :: (Monad f, Comonad n) => (Either b a -> f c) -> Scope (n b) f a -> f c -instantiateEitherName k e = unscope e >>= \v -> case v of - B b -> k (Left (extract b)) - F a -> a >>= k . Right -{-# INLINE instantiateEitherName #-} +{-# LANGUAGE CPP #-}+#ifdef __GLASGOW_HASKELL__+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE Trustworthy #-}+#endif++-----------------------------------------------------------------------------+-- |+-- Copyright : (C) 2012 Edward Kmett+-- License : BSD-style (see the file LICENSE)+--+-- Maintainer : Edward Kmett <ekmett@gmail.com>+-- Stability : experimental+-- Portability : portable+--+-- The problem with locally nameless approaches is that original names are+-- often useful for error reporting, or to allow for the user in an interactive+-- theorem prover to convey some hint about the domain. A @'Name' n b@ is a value+-- @b@ supplemented with a (discardable) name that may be useful for error+-- reporting purposes. In particular, this name does not participate in+-- comparisons for equality.+--+-- This module is /not/ exported from "Bound" by default. You need to explicitly+-- import it, due to the fact that 'Name' is a pretty common term in other+-- people's code.+----------------------------------------------------------------------------+module Bound.Name+ ( Name(..)+ , _Name+ , name+ , abstractName+ , abstract1Name+ , abstractEitherName+ , instantiateName+ , instantiate1Name+ , instantiateEitherName+ ) where++import Bound.Scope+import Bound.Var+import Control.Comonad+import Control.DeepSeq+import Control.Monad (liftM, liftM2)+import Data.Bifunctor+import Data.Bifoldable+import qualified Data.Binary as Binary+import Data.Binary (Binary)+import Data.Bitraversable+import Data.Bytes.Serial+import Data.Functor.Classes+#ifdef __GLASGOW_HASKELL__+import Data.Data+import GHC.Generics+#endif+import Data.Hashable (Hashable(..))+import Data.Hashable.Lifted (Hashable1(..), Hashable2(..))+import Data.Profunctor+import qualified Data.Serialize as Serialize+import Data.Serialize (Serialize)++-------------------------------------------------------------------------------+-- Names+-------------------------------------------------------------------------------++-- |+-- We track the choice of 'Name' @n@ as a forgettable property that does /not/ affect+-- the result of ('==') or 'compare'.+--+-- To compare names rather than values, use @('Data.Function.on' 'compare' 'name')@ instead.+data Name n b = Name n b deriving+ ( Show+ , Read+#ifdef __GLASGOW_HASKELL__+ , Data+ , Generic+ , Generic1+#endif+ )++-- | Extract the 'name'.+name :: Name n b -> n+name (Name n _) = n+{-# INLINE name #-}++-- |+--+-- This provides an 'Iso' that can be used to access the parts of a 'Name'.+--+-- @+-- '_Name' :: Iso ('Name' n a) ('Name' m b) (n, a) (m, b)+-- @+_Name :: (Profunctor p, Functor f) => p (n, a) (f (m,b)) -> p (Name n a) (f (Name m b))+_Name = dimap (\(Name n a) -> (n, a)) (fmap (uncurry Name))+{-# INLINE _Name #-}++-------------------------------------------------------------------------------+-- Instances+-------------------------------------------------------------------------------++instance Eq b => Eq (Name n b) where+ Name _ a == Name _ b = a == b+ {-# INLINE (==) #-}++instance Hashable2 Name where+ liftHashWithSalt2 _ h s (Name _ a) = h s a+ {-# INLINE liftHashWithSalt2 #-}++instance Hashable1 (Name n) where+ liftHashWithSalt h s (Name _ a) = h s a+ {-# INLINE liftHashWithSalt #-}++instance Hashable a => Hashable (Name n a) where+ hashWithSalt m (Name _ a) = hashWithSalt m a+ {-# INLINE hashWithSalt #-}++instance Ord b => Ord (Name n b) where+ Name _ a `compare` Name _ b = compare a b+ {-# INLINE compare #-}++instance Functor (Name n) where+ fmap f (Name n a) = Name n (f a)+ {-# INLINE fmap #-}++instance Foldable (Name n) where+ foldMap f (Name _ a) = f a+ {-# INLINE foldMap #-}++instance Traversable (Name n) where+ traverse f (Name n a) = Name n <$> f a+ {-# INLINE traverse #-}++instance Bifunctor Name where+ bimap f g (Name n a) = Name (f n) (g a)+ {-# INLINE bimap #-}++instance Bifoldable Name where+ bifoldMap f g (Name n a) = f n `mappend` g a+ {-# INLINE bifoldMap #-}++instance Bitraversable Name where+ bitraverse f g (Name n a) = Name <$> f n <*> g a+ {-# INLINE bitraverse #-}++instance Comonad (Name n) where+ extract (Name _ b) = b+ {-# INLINE extract #-}+ extend f w@(Name n _) = Name n (f w)+ {-# INLINE extend #-}++instance Eq2 Name where+ liftEq2 _ g (Name _ b) (Name _ d) = g b d++instance Ord2 Name where+ liftCompare2 _ g (Name _ b) (Name _ d) = g b d++instance Show2 Name where+ liftShowsPrec2 f _ h _ d (Name a b) = showsBinaryWith f h "Name" d a b++instance Read2 Name where+ liftReadsPrec2 f _ h _ = readsData $ readsBinaryWith f h "Name" Name++instance Eq1 (Name b) where+ liftEq f (Name _ b) (Name _ d) = f b d++instance Ord1 (Name b) where+ liftCompare f (Name _ b) (Name _ d) = f b d++instance Show b => Show1 (Name b) where+ liftShowsPrec f _ d (Name a b) = showsBinaryWith showsPrec f "Name" d a b++instance Read b => Read1 (Name b) where+ liftReadsPrec f _ = readsData $ readsBinaryWith readsPrec f "Name" Name++instance Serial2 Name where+ serializeWith2 pb pf (Name b a) = pb b >> pf a+ {-# INLINE serializeWith2 #-}++ deserializeWith2 = liftM2 Name+ {-# INLINE deserializeWith2 #-}++instance Serial b => Serial1 (Name b) where+ serializeWith = serializeWith2 serialize+ {-# INLINE serializeWith #-}+ deserializeWith = deserializeWith2 deserialize+ {-# INLINE deserializeWith #-}++instance (Serial b, Serial a) => Serial (Name b a) where+ serialize = serializeWith2 serialize serialize+ {-# INLINE serialize #-}+ deserialize = deserializeWith2 deserialize deserialize+ {-# INLINE deserialize #-}++instance (Binary b, Binary a) => Binary (Name b a) where+ put = serializeWith2 Binary.put Binary.put+ get = deserializeWith2 Binary.get Binary.get++instance (Serialize b, Serialize a) => Serialize (Name b a) where+ put = serializeWith2 Serialize.put Serialize.put+ get = deserializeWith2 Serialize.get Serialize.get++instance (NFData b, NFData a) => NFData (Name b a) where+ rnf (Name a b) = rnf a `seq` rnf b++-------------------------------------------------------------------------------+-- Abstraction+-------------------------------------------------------------------------------++-- | Abstraction, capturing named bound variables.+abstractName :: Monad f => (a -> Maybe b) -> f a -> Scope (Name a b) f a+abstractName f t = Scope (liftM k t) where+ k a = case f a of+ Just b -> B (Name a b)+ Nothing -> F (return a)+{-# INLINE abstractName #-}++-- | Abstract over a single variable+abstract1Name :: (Monad f, Eq a) => a -> f a -> Scope (Name a ()) f a+abstract1Name a = abstractName (\b -> if a == b then Just () else Nothing)+{-# INLINE abstract1Name #-}++-- | Capture some free variables in an expression to yield+-- a 'Scope' with named bound variables. Optionally change the+-- types of the remaining free variables.+abstractEitherName :: Monad f => (a -> Either b c) -> f a -> Scope (Name a b) f c+abstractEitherName f e = Scope (liftM k e) where+ k y = case f y of+ Left z -> B (Name y z)+ Right y' -> F (return y')++-------------------------------------------------------------------------------+-- Instantiation+-------------------------------------------------------------------------------++-- | Enter a scope, instantiating all bound variables, but discarding (comonadic)+-- meta data, like its name+instantiateName :: (Monad f, Comonad n) => (b -> f a) -> Scope (n b) f a -> f a+instantiateName k e = unscope e >>= \v -> case v of+ B b -> k (extract b)+ F a -> a+{-# INLINE instantiateName #-}++-- | Enter a 'Scope' that binds one (named) variable, instantiating it.+--+-- @'instantiate1Name' = 'instantiate1'@+instantiate1Name :: Monad f => f a -> Scope n f a -> f a+instantiate1Name = instantiate1+{-# INLINE instantiate1Name #-}++instantiateEitherName :: (Monad f, Comonad n) => (Either b a -> f c) -> Scope (n b) f a -> f c+instantiateEitherName k e = unscope e >>= \v -> case v of+ B b -> k (Left (extract b))+ F a -> a >>= k . Right+{-# INLINE instantiateEitherName #-}
src/Bound/Scope.hs view
@@ -1,465 +1,465 @@-{-# LANGUAGE CPP #-} -{-# LANGUAGE Rank2Types #-} -#ifdef __GLASGOW_HASKELL__ -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE StandaloneDeriving #-} -{-# LANGUAGE DeriveDataTypeable #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE UndecidableInstances #-} -{-# LANGUAGE Trustworthy #-} -{-# LANGUAGE DeriveGeneric #-} -#endif - ------------------------------------------------------------------------------ --- | --- Copyright : (C) 2012-2013 Edward Kmett --- License : BSD-style (see the file LICENSE) --- --- Maintainer : Edward Kmett <ekmett@gmail.com> --- Stability : experimental --- Portability : portable --- --- This is the work-horse of the @bound@ library. --- --- 'Scope' provides a single generalized de Bruijn level --- and is often used inside of the definition of binders. ----------------------------------------------------------------------------- -module Bound.Scope - ( Scope(..) - -- * Abstraction - , abstract, abstract1, abstractEither - -- * Instantiation - , instantiate, instantiate1, instantiateEither - -- * Traditional de Bruijn - , fromScope - , toScope - -- * Bound variable manipulation - , splat - , bindings - , mapBound - , mapScope - , liftMBound - , liftMScope - , foldMapBound - , foldMapScope - , traverseBound_ - , traverseScope_ - , mapMBound_ - , mapMScope_ - , traverseBound - , traverseScope - , mapMBound - , mapMScope - , serializeScope - , deserializeScope - , hoistScope - , bitraverseScope - , bitransverseScope - , transverseScope - , instantiateVars - ) where - -import Bound.Class -import Bound.Var -import Control.Applicative -import Control.DeepSeq -import Control.Monad hiding (mapM, mapM_) -import Control.Monad.Morph -import Data.Bifunctor -import Data.Bifoldable -import qualified Data.Binary as Binary -import Data.Binary (Binary) -import Data.Bitraversable -import Data.Bytes.Get -import Data.Bytes.Put -import Data.Bytes.Serial -import Data.Foldable -import Data.Functor.Classes -import Data.Hashable (Hashable (..)) -import Data.Hashable.Lifted (Hashable1(..), hashWithSalt1) -import Data.Monoid -import qualified Data.Serialize as Serialize -import Data.Serialize (Serialize) -import Data.Traversable -import Prelude hiding (foldr, mapM, mapM_) -import Data.Data -#if defined(__GLASGOW_HASKELL__) -import GHC.Generics ( Generic, Generic1 ) -#endif - --- $setup --- >>> import Bound.Var - -------------------------------------------------------------------------------- --- Scopes -------------------------------------------------------------------------------- - --- | @'Scope' b f a@ is an @f@ expression with bound variables in @b@, --- and free variables in @a@ --- --- We store bound variables as their generalized de Bruijn --- representation in that we're allowed to 'lift' (using 'F') an entire --- tree rather than only succ individual variables, but we're still --- only allowed to do so once per 'Scope'. Weakening trees permits --- /O(1)/ weakening and permits more sharing opportunities. Here the --- deBruijn 0 is represented by the 'B' constructor of 'Var', while the --- de Bruijn 'succ' (which may be applied to an entire tree!) is handled --- by 'F'. --- --- NB: equality and comparison quotient out the distinct 'F' placements --- allowed by the generalized de Bruijn representation and return the --- same result as a traditional de Bruijn representation would. --- --- Logically you can think of this as if the shape were the traditional --- @f (Var b a)@, but the extra @f a@ inside permits us a cheaper 'lift'. --- -newtype Scope b f a = Scope { unscope :: f (Var b (f a)) } -#if defined(__GLASGOW_HASKELL__) - deriving (Generic) -#endif -deriving instance Functor f => Generic1 (Scope b f) - -------------------------------------------------------------------------------- --- Instances -------------------------------------------------------------------------------- - -instance Functor f => Functor (Scope b f) where - fmap f (Scope a) = Scope (fmap (fmap (fmap f)) a) - {-# INLINE fmap #-} - --- | @'toList'@ is provides a list (with duplicates) of the free variables -instance Foldable f => Foldable (Scope b f) where - foldMap f (Scope a) = foldMap (foldMap (foldMap f)) a - {-# INLINE foldMap #-} - -instance Traversable f => Traversable (Scope b f) where - traverse f (Scope a) = Scope <$> traverse (traverse (traverse f)) a - {-# INLINE traverse #-} - -instance (Functor f, Monad f) => Applicative (Scope b f) where - pure a = Scope (return (F (return a))) - {-# INLINE pure #-} - (<*>) = ap - {-# INLINE (<*>) #-} - --- | The monad permits substitution on free variables, while preserving --- bound variables -instance Monad f => Monad (Scope b f) where - Scope e >>= f = Scope $ e >>= \v -> case v of - B b -> return (B b) - F ea -> ea >>= unscope . f - {-# INLINE (>>=) #-} - -instance MonadTrans (Scope b) where - lift m = Scope (return (F m)) - {-# INLINE lift #-} - -instance MFunctor (Scope b) where - hoist = hoistScope - {-# INLINE hoist #-} - -instance (Monad f, Eq b, Eq1 f, Eq a) => Eq (Scope b f a) where (==) = eq1 -instance (Monad f, Ord b, Ord1 f, Ord a) => Ord (Scope b f a) where compare = compare1 - --------------------------------------------------------------------------------- --- * transformers 0.5 Data.Functor.Classes --------------------------------------------------------------------------------- - -instance (Read b, Read1 f, Read a) => Read (Scope b f a) where readsPrec = readsPrec1 -instance (Show b, Show1 f, Show a) => Show (Scope b f a) where showsPrec = showsPrec1 - -instance (Monad f, Eq b, Eq1 f) => Eq1 (Scope b f) where - liftEq f m n = liftEq (liftEq f) (fromScope m) (fromScope n) - -instance (Monad f, Ord b, Ord1 f) => Ord1 (Scope b f) where - liftCompare f m n = liftCompare (liftCompare f) (fromScope m) (fromScope n) - -instance (Show b, Show1 f) => Show1 (Scope b f) where - liftShowsPrec f g d m = showsUnaryWith (liftShowsPrec (liftShowsPrec f' g') (liftShowList f' g')) "Scope" d (unscope m) where - f' = liftShowsPrec f g - g' = liftShowList f g - -instance (Read b, Read1 f) => Read1 (Scope b f) where - liftReadsPrec f g = readsData $ readsUnaryWith (liftReadsPrec (liftReadsPrec f' g') (liftReadList f' g')) "Scope" Scope where - f' = liftReadsPrec f g - g' = liftReadList f g - -instance Bound (Scope b) where - Scope m >>>= f = Scope (liftM (fmap (>>= f)) m) - {-# INLINE (>>>=) #-} - --- {-# INLINE hashWithSalt1 #-} - -instance (Hashable b, Monad f, Hashable1 f) => Hashable1 (Scope b f) where - liftHashWithSalt h s m = liftHashWithSalt (liftHashWithSalt h) s (fromScope m) - {-# INLINE liftHashWithSalt #-} - -instance (Hashable b, Monad f, Hashable1 f, Hashable a) => Hashable (Scope b f a) where - hashWithSalt n m = hashWithSalt1 n (fromScope m) - {-# INLINE hashWithSalt #-} - -instance NFData (f (Var b (f a))) => NFData (Scope b f a) where - rnf scope = rnf (unscope scope) - -------------------------------------------------------------------------------- --- Abstraction -------------------------------------------------------------------------------- - --- | Capture some free variables in an expression to yield --- a 'Scope' with bound variables in @b@ --- --- >>> :m + Data.List --- >>> abstract (`elemIndex` "bar") "barry" --- Scope [B 0,B 1,B 2,B 2,F "y"] -abstract :: Monad f => (a -> Maybe b) -> f a -> Scope b f a -abstract f e = Scope (liftM k e) where - k y = case f y of - Just z -> B z - Nothing -> F (return y) -{-# INLINE abstract #-} - --- | Abstract over a single variable --- --- >>> abstract1 'x' "xyz" --- Scope [B (),F "y",F "z"] -abstract1 :: (Monad f, Eq a) => a -> f a -> Scope () f a -abstract1 a = abstract (\b -> if a == b then Just () else Nothing) -{-# INLINE abstract1 #-} - --- | Capture some free variables in an expression to yield --- a 'Scope' with bound variables in @b@. Optionally change the --- types of the remaining free variables. -abstractEither :: Monad f => (a -> Either b c) -> f a -> Scope b f c -abstractEither f e = Scope (liftM k e) where - k y = case f y of - Left z -> B z - Right y' -> F (return y') - -------------------------------------------------------------------------------- --- Instantiation -------------------------------------------------------------------------------- - --- | Enter a scope, instantiating all bound variables --- --- >>> :m + Data.List --- >>> instantiate (\x -> [toEnum (97 + x)]) $ abstract (`elemIndex` "bar") "barry" --- "abccy" -instantiate :: Monad f => (b -> f a) -> Scope b f a -> f a -instantiate k e = unscope e >>= \v -> case v of - B b -> k b - F a -> a -{-# INLINE instantiate #-} - --- | Enter a 'Scope' that binds one variable, instantiating it --- --- >>> instantiate1 "x" $ Scope [B (),F "y",F "z"] --- "xyz" -instantiate1 :: Monad f => f a -> Scope n f a -> f a -instantiate1 e = instantiate (const e) -{-# INLINE instantiate1 #-} - --- | Enter a scope, and instantiate all bound and free variables in one go. -instantiateEither :: Monad f => (Either b a -> f c) -> Scope b f a -> f c -instantiateEither f s = unscope s >>= \v -> case v of - B b -> f (Left b) - F ea -> ea >>= f . Right -{-# INLINE instantiateEither #-} - -------------------------------------------------------------------------------- --- Traditional de Bruijn -------------------------------------------------------------------------------- - --- | @'fromScope'@ quotients out the possible placements of 'F' in 'Scope' --- by distributing them all to the leaves. This yields a more traditional --- de Bruijn indexing scheme for bound variables. --- --- Since, --- --- @'fromScope' '.' 'toScope' ≡ 'id'@ --- --- we know that --- --- @'fromScope' '.' 'toScope' '.' 'fromScope' ≡ 'fromScope'@ --- --- and therefore @('toScope' . 'fromScope')@ is idempotent. -fromScope :: Monad f => Scope b f a -> f (Var b a) -fromScope (Scope s) = s >>= \v -> case v of - F e -> liftM F e - B b -> return (B b) -{-# INLINE fromScope #-} - --- | Convert from traditional de Bruijn to generalized de Bruijn indices. --- --- This requires a full tree traversal -toScope :: Monad f => f (Var b a) -> Scope b f a -toScope e = Scope (liftM (fmap return) e) -{-# INLINE toScope #-} - -------------------------------------------------------------------------------- --- Exotic Traversals of Bound Variables (not exported by default) -------------------------------------------------------------------------------- - --- | Perform substitution on both bound and free variables in a 'Scope'. -splat :: Monad f => (a -> f c) -> (b -> f c) -> Scope b f a -> f c -splat f unbind s = unscope s >>= \v -> case v of - B b -> unbind b - F ea -> ea >>= f -{-# INLINE splat #-} - --- | Return a list of occurences of the variables bound by this 'Scope'. -bindings :: Foldable f => Scope b f a -> [b] -bindings (Scope s) = foldr f [] s where - f (B v) vs = v : vs - f _ vs = vs -{-# INLINE bindings #-} - --- | Perform a change of variables on bound variables. -mapBound :: Functor f => (b -> b') -> Scope b f a -> Scope b' f a -mapBound f (Scope s) = Scope (fmap f' s) where - f' (B b) = B (f b) - f' (F a) = F a -{-# INLINE mapBound #-} - --- | Perform a change of variables, reassigning both bound and free variables. -mapScope :: Functor f => (b -> d) -> (a -> c) -> Scope b f a -> Scope d f c -mapScope f g (Scope s) = Scope $ fmap (bimap f (fmap g)) s -{-# INLINE mapScope #-} - --- | Perform a change of variables on bound variables given only a 'Monad' --- instance -liftMBound :: Monad m => (b -> b') -> Scope b m a -> Scope b' m a -liftMBound f (Scope s) = Scope (liftM f' s) where - f' (B b) = B (f b) - f' (F a) = F a -{-# INLINE liftMBound #-} - --- | A version of 'mapScope' that can be used when you only have the 'Monad' --- instance -liftMScope :: Monad m => (b -> d) -> (a -> c) -> Scope b m a -> Scope d m c -liftMScope f g (Scope s) = Scope $ liftM (bimap f (liftM g)) s -{-# INLINE liftMScope #-} - --- | Obtain a result by collecting information from bound variables -foldMapBound :: (Foldable f, Monoid r) => (b -> r) -> Scope b f a -> r -foldMapBound f (Scope s) = foldMap f' s where - f' (B a) = f a - f' _ = mempty -{-# INLINE foldMapBound #-} - --- | Obtain a result by collecting information from both bound and free --- variables -foldMapScope :: (Foldable f, Monoid r) => - (b -> r) -> (a -> r) -> Scope b f a -> r -foldMapScope f g (Scope s) = foldMap (bifoldMap f (foldMap g)) s -{-# INLINE foldMapScope #-} - --- | 'traverse_' the bound variables in a 'Scope'. -traverseBound_ :: (Applicative g, Foldable f) => - (b -> g d) -> Scope b f a -> g () -traverseBound_ f (Scope s) = traverse_ f' s - where f' (B a) = () <$ f a - f' _ = pure () -{-# INLINE traverseBound_ #-} - --- | 'traverse' both the variables bound by this scope and any free variables. -traverseScope_ :: (Applicative g, Foldable f) => - (b -> g d) -> (a -> g c) -> Scope b f a -> g () -traverseScope_ f g (Scope s) = traverse_ (bitraverse_ f (traverse_ g)) s -{-# INLINE traverseScope_ #-} - --- | mapM_ over the variables bound by this scope -mapMBound_ :: (Monad g, Foldable f) => (b -> g d) -> Scope b f a -> g () -mapMBound_ f (Scope s) = mapM_ f' s where - f' (B a) = do _ <- f a; return () - f' _ = return () -{-# INLINE mapMBound_ #-} - --- | A 'traverseScope_' that can be used when you only have a 'Monad' --- instance -mapMScope_ :: (Monad m, Foldable f) => - (b -> m d) -> (a -> m c) -> Scope b f a -> m () -mapMScope_ f g (Scope s) = mapM_ (bimapM_ f (mapM_ g)) s -{-# INLINE mapMScope_ #-} - --- | 'traverse' the bound variables in a 'Scope'. -traverseBound :: (Applicative g, Traversable f) => - (b -> g c) -> Scope b f a -> g (Scope c f a) -traverseBound f (Scope s) = Scope <$> traverse f' s where - f' (B b) = B <$> f b - f' (F a) = pure (F a) -{-# INLINE traverseBound #-} - --- | Traverse both bound and free variables -traverseScope :: (Applicative g, Traversable f) => - (b -> g d) -> (a -> g c) -> Scope b f a -> g (Scope d f c) -traverseScope f g (Scope s) = Scope <$> traverse (bitraverse f (traverse g)) s -{-# INLINE traverseScope #-} - --- | mapM over both bound and free variables -mapMBound :: (Monad m, Traversable f) => - (b -> m c) -> Scope b f a -> m (Scope c f a) -mapMBound f (Scope s) = liftM Scope (mapM f' s) where - f' (B b) = liftM B (f b) - f' (F a) = return (F a) -{-# INLINE mapMBound #-} - --- | A 'traverseScope' that can be used when you only have a 'Monad' --- instance -mapMScope :: (Monad m, Traversable f) => - (b -> m d) -> (a -> m c) -> Scope b f a -> m (Scope d f c) -mapMScope f g (Scope s) = liftM Scope (mapM (bimapM f (mapM g)) s) -{-# INLINE mapMScope #-} - -serializeScope :: (Serial1 f, MonadPut m) => (b -> m ()) -> (v -> m ()) -> Scope b f v -> m () -serializeScope pb pv (Scope body) = serializeWith (serializeWith2 pb $ serializeWith pv) body -{-# INLINE serializeScope #-} - -deserializeScope :: (Serial1 f, MonadGet m) => m b -> m v -> m (Scope b f v) -deserializeScope gb gv = liftM Scope $ deserializeWith (deserializeWith2 gb $ deserializeWith gv) -{-# INLINE deserializeScope #-} - --- | This allows you to 'bitraverse' a 'Scope'. -bitraverseScope :: (Bitraversable t, Applicative f) => (k -> f k') -> (a -> f a') -> Scope b (t k) a -> f (Scope b (t k') a') -bitraverseScope f = bitransverseScope (bitraverse f) -{-# INLINE bitraverseScope #-} - --- | This is a higher-order analogue of 'traverse'. -transverseScope :: (Applicative f, Monad f, Traversable g) - => (forall r. g r -> f (h r)) - -> Scope b g a -> f (Scope b h a) -transverseScope tau (Scope e) = Scope <$> (tau =<< traverse (traverse tau) e) - -bitransverseScope :: Applicative f => (forall a a'. (a -> f a') -> t a -> f (u a')) -> (c -> f c') -> Scope b t c -> f (Scope b u c') -bitransverseScope tau f = fmap Scope . tau (_F (tau f)) . unscope -{-# INLINE bitransverseScope #-} - --- | instantiate bound variables using a list of new variables -instantiateVars :: Monad t => [a] -> Scope Int t a -> t a -instantiateVars as = instantiate (vs !!) where - vs = map return as -{-# INLINE instantiateVars #-} - --- | Lift a natural transformation from @f@ to @g@ into one between scopes. -hoistScope :: Functor f => (forall x. f x -> g x) -> Scope b f a -> Scope b g a -hoistScope t (Scope b) = Scope $ t (fmap t <$> b) -{-# INLINE hoistScope #-} - -instance (Serial b, Serial1 f) => Serial1 (Scope b f) where - serializeWith = serializeScope serialize - deserializeWith = deserializeScope deserialize - -instance (Serial b, Serial1 f, Serial a) => Serial (Scope b f a) where - serialize = serializeScope serialize serialize - deserialize = deserializeScope deserialize deserialize - -instance (Binary b, Serial1 f, Binary a) => Binary (Scope b f a) where - put = serializeScope Binary.put Binary.put - get = deserializeScope Binary.get Binary.get - -instance (Serialize b, Serial1 f, Serialize a) => Serialize (Scope b f a) where - put = serializeScope Serialize.put Serialize.put - get = deserializeScope Serialize.get Serialize.get - -#ifdef __GLASGOW_HASKELL__ -deriving instance (Typeable b, Typeable f, Data a, Data (f (Var b (f a)))) => Data (Scope b f a) -#endif +{-# LANGUAGE CPP #-}+{-# LANGUAGE Rank2Types #-}+#ifdef __GLASGOW_HASKELL__+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE Trustworthy #-}+{-# LANGUAGE DeriveGeneric #-}+#endif++-----------------------------------------------------------------------------+-- |+-- Copyright : (C) 2012-2013 Edward Kmett+-- License : BSD-style (see the file LICENSE)+--+-- Maintainer : Edward Kmett <ekmett@gmail.com>+-- Stability : experimental+-- Portability : portable+--+-- This is the work-horse of the @bound@ library.+--+-- 'Scope' provides a single generalized de Bruijn level+-- and is often used inside of the definition of binders.+----------------------------------------------------------------------------+module Bound.Scope+ ( Scope(..)+ -- * Abstraction+ , abstract, abstract1, abstractEither+ -- * Instantiation+ , instantiate, instantiate1, instantiateEither+ -- * Traditional de Bruijn+ , fromScope+ , toScope+ -- * Bound variable manipulation+ , splat+ , bindings+ , mapBound+ , mapScope+ , liftMBound+ , liftMScope+ , foldMapBound+ , foldMapScope+ , traverseBound_+ , traverseScope_+ , mapMBound_+ , mapMScope_+ , traverseBound+ , traverseScope+ , mapMBound+ , mapMScope+ , serializeScope+ , deserializeScope+ , hoistScope+ , bitraverseScope+ , bitransverseScope+ , transverseScope+ , instantiateVars+ ) where++import Bound.Class+import Bound.Var+import Control.Applicative+import Control.DeepSeq+import Control.Monad hiding (mapM, mapM_)+import Control.Monad.Morph+import Data.Bifunctor+import Data.Bifoldable+import qualified Data.Binary as Binary+import Data.Binary (Binary)+import Data.Bitraversable+import Data.Bytes.Get+import Data.Bytes.Put+import Data.Bytes.Serial+import Data.Foldable+import Data.Functor.Classes+import Data.Hashable (Hashable (..))+import Data.Hashable.Lifted (Hashable1(..), hashWithSalt1)+import Data.Monoid+import qualified Data.Serialize as Serialize+import Data.Serialize (Serialize)+import Data.Traversable+import Prelude hiding (foldr, mapM, mapM_)+import Data.Data+#if defined(__GLASGOW_HASKELL__)+import GHC.Generics ( Generic, Generic1 )+#endif++-- $setup+-- >>> import Bound.Var++-------------------------------------------------------------------------------+-- Scopes+-------------------------------------------------------------------------------++-- | @'Scope' b f a@ is an @f@ expression with bound variables in @b@,+-- and free variables in @a@+--+-- We store bound variables as their generalized de Bruijn+-- representation in that we're allowed to 'lift' (using 'F') an entire+-- tree rather than only succ individual variables, but we're still+-- only allowed to do so once per 'Scope'. Weakening trees permits+-- /O(1)/ weakening and permits more sharing opportunities. Here the+-- deBruijn 0 is represented by the 'B' constructor of 'Var', while the+-- de Bruijn 'succ' (which may be applied to an entire tree!) is handled+-- by 'F'.+--+-- NB: equality and comparison quotient out the distinct 'F' placements+-- allowed by the generalized de Bruijn representation and return the+-- same result as a traditional de Bruijn representation would.+--+-- Logically you can think of this as if the shape were the traditional+-- @f (Var b a)@, but the extra @f a@ inside permits us a cheaper 'lift'.+--+newtype Scope b f a = Scope { unscope :: f (Var b (f a)) }+#if defined(__GLASGOW_HASKELL__)+ deriving (Generic)+#endif+deriving instance Functor f => Generic1 (Scope b f)++-------------------------------------------------------------------------------+-- Instances+-------------------------------------------------------------------------------++instance Functor f => Functor (Scope b f) where+ fmap f (Scope a) = Scope (fmap (fmap (fmap f)) a)+ {-# INLINE fmap #-}++-- | @'toList'@ is provides a list (with duplicates) of the free variables+instance Foldable f => Foldable (Scope b f) where+ foldMap f (Scope a) = foldMap (foldMap (foldMap f)) a+ {-# INLINE foldMap #-}++instance Traversable f => Traversable (Scope b f) where+ traverse f (Scope a) = Scope <$> traverse (traverse (traverse f)) a+ {-# INLINE traverse #-}++instance (Functor f, Monad f) => Applicative (Scope b f) where+ pure a = Scope (return (F (return a)))+ {-# INLINE pure #-}+ (<*>) = ap+ {-# INLINE (<*>) #-}++-- | The monad permits substitution on free variables, while preserving+-- bound variables+instance Monad f => Monad (Scope b f) where+ Scope e >>= f = Scope $ e >>= \v -> case v of+ B b -> return (B b)+ F ea -> ea >>= unscope . f+ {-# INLINE (>>=) #-}++instance MonadTrans (Scope b) where+ lift m = Scope (return (F m))+ {-# INLINE lift #-}++instance MFunctor (Scope b) where+ hoist = hoistScope+ {-# INLINE hoist #-}++instance (Monad f, Eq b, Eq1 f, Eq a) => Eq (Scope b f a) where (==) = eq1+instance (Monad f, Ord b, Ord1 f, Ord a) => Ord (Scope b f a) where compare = compare1++--------------------------------------------------------------------------------+-- * transformers 0.5 Data.Functor.Classes+--------------------------------------------------------------------------------++instance (Read b, Read1 f, Read a) => Read (Scope b f a) where readsPrec = readsPrec1+instance (Show b, Show1 f, Show a) => Show (Scope b f a) where showsPrec = showsPrec1++instance (Monad f, Eq b, Eq1 f) => Eq1 (Scope b f) where+ liftEq f m n = liftEq (liftEq f) (fromScope m) (fromScope n)++instance (Monad f, Ord b, Ord1 f) => Ord1 (Scope b f) where+ liftCompare f m n = liftCompare (liftCompare f) (fromScope m) (fromScope n)++instance (Show b, Show1 f) => Show1 (Scope b f) where+ liftShowsPrec f g d m = showsUnaryWith (liftShowsPrec (liftShowsPrec f' g') (liftShowList f' g')) "Scope" d (unscope m) where+ f' = liftShowsPrec f g+ g' = liftShowList f g++instance (Read b, Read1 f) => Read1 (Scope b f) where+ liftReadsPrec f g = readsData $ readsUnaryWith (liftReadsPrec (liftReadsPrec f' g') (liftReadList f' g')) "Scope" Scope where+ f' = liftReadsPrec f g+ g' = liftReadList f g++instance Bound (Scope b) where+ Scope m >>>= f = Scope (liftM (fmap (>>= f)) m)+ {-# INLINE (>>>=) #-}++-- {-# INLINE hashWithSalt1 #-}++instance (Hashable b, Monad f, Hashable1 f) => Hashable1 (Scope b f) where+ liftHashWithSalt h s m = liftHashWithSalt (liftHashWithSalt h) s (fromScope m)+ {-# INLINE liftHashWithSalt #-}++instance (Hashable b, Monad f, Hashable1 f, Hashable a) => Hashable (Scope b f a) where+ hashWithSalt n m = hashWithSalt1 n (fromScope m)+ {-# INLINE hashWithSalt #-}++instance NFData (f (Var b (f a))) => NFData (Scope b f a) where+ rnf scope = rnf (unscope scope)++-------------------------------------------------------------------------------+-- Abstraction+-------------------------------------------------------------------------------++-- | Capture some free variables in an expression to yield+-- a 'Scope' with bound variables in @b@+--+-- >>> :m + Data.List+-- >>> abstract (`elemIndex` "bar") "barry"+-- Scope [B 0,B 1,B 2,B 2,F "y"]+abstract :: Monad f => (a -> Maybe b) -> f a -> Scope b f a+abstract f e = Scope (liftM k e) where+ k y = case f y of+ Just z -> B z+ Nothing -> F (return y)+{-# INLINE abstract #-}++-- | Abstract over a single variable+--+-- >>> abstract1 'x' "xyz"+-- Scope [B (),F "y",F "z"]+abstract1 :: (Monad f, Eq a) => a -> f a -> Scope () f a+abstract1 a = abstract (\b -> if a == b then Just () else Nothing)+{-# INLINE abstract1 #-}++-- | Capture some free variables in an expression to yield+-- a 'Scope' with bound variables in @b@. Optionally change the+-- types of the remaining free variables.+abstractEither :: Monad f => (a -> Either b c) -> f a -> Scope b f c+abstractEither f e = Scope (liftM k e) where+ k y = case f y of+ Left z -> B z+ Right y' -> F (return y')++-------------------------------------------------------------------------------+-- Instantiation+-------------------------------------------------------------------------------++-- | Enter a scope, instantiating all bound variables+--+-- >>> :m + Data.List+-- >>> instantiate (\x -> [toEnum (97 + x)]) $ abstract (`elemIndex` "bar") "barry"+-- "abccy"+instantiate :: Monad f => (b -> f a) -> Scope b f a -> f a+instantiate k e = unscope e >>= \v -> case v of+ B b -> k b+ F a -> a+{-# INLINE instantiate #-}++-- | Enter a 'Scope' that binds one variable, instantiating it+--+-- >>> instantiate1 "x" $ Scope [B (),F "y",F "z"]+-- "xyz"+instantiate1 :: Monad f => f a -> Scope n f a -> f a+instantiate1 e = instantiate (const e)+{-# INLINE instantiate1 #-}++-- | Enter a scope, and instantiate all bound and free variables in one go.+instantiateEither :: Monad f => (Either b a -> f c) -> Scope b f a -> f c+instantiateEither f s = unscope s >>= \v -> case v of+ B b -> f (Left b)+ F ea -> ea >>= f . Right+{-# INLINE instantiateEither #-}++-------------------------------------------------------------------------------+-- Traditional de Bruijn+-------------------------------------------------------------------------------++-- | @'fromScope'@ quotients out the possible placements of 'F' in 'Scope'+-- by distributing them all to the leaves. This yields a more traditional+-- de Bruijn indexing scheme for bound variables.+--+-- Since,+--+-- @'fromScope' '.' 'toScope' ≡ 'id'@+--+-- we know that+--+-- @'fromScope' '.' 'toScope' '.' 'fromScope' ≡ 'fromScope'@+--+-- and therefore @('toScope' . 'fromScope')@ is idempotent.+fromScope :: Monad f => Scope b f a -> f (Var b a)+fromScope (Scope s) = s >>= \v -> case v of+ F e -> liftM F e+ B b -> return (B b)+{-# INLINE fromScope #-}++-- | Convert from traditional de Bruijn to generalized de Bruijn indices.+--+-- This requires a full tree traversal+toScope :: Monad f => f (Var b a) -> Scope b f a+toScope e = Scope (liftM (fmap return) e)+{-# INLINE toScope #-}++-------------------------------------------------------------------------------+-- Exotic Traversals of Bound Variables (not exported by default)+-------------------------------------------------------------------------------++-- | Perform substitution on both bound and free variables in a 'Scope'.+splat :: Monad f => (a -> f c) -> (b -> f c) -> Scope b f a -> f c+splat f unbind s = unscope s >>= \v -> case v of+ B b -> unbind b+ F ea -> ea >>= f+{-# INLINE splat #-}++-- | Return a list of occurences of the variables bound by this 'Scope'.+bindings :: Foldable f => Scope b f a -> [b]+bindings (Scope s) = foldr f [] s where+ f (B v) vs = v : vs+ f _ vs = vs+{-# INLINE bindings #-}++-- | Perform a change of variables on bound variables.+mapBound :: Functor f => (b -> b') -> Scope b f a -> Scope b' f a+mapBound f (Scope s) = Scope (fmap f' s) where+ f' (B b) = B (f b)+ f' (F a) = F a+{-# INLINE mapBound #-}++-- | Perform a change of variables, reassigning both bound and free variables.+mapScope :: Functor f => (b -> d) -> (a -> c) -> Scope b f a -> Scope d f c+mapScope f g (Scope s) = Scope $ fmap (bimap f (fmap g)) s+{-# INLINE mapScope #-}++-- | Perform a change of variables on bound variables given only a 'Monad'+-- instance+liftMBound :: Monad m => (b -> b') -> Scope b m a -> Scope b' m a+liftMBound f (Scope s) = Scope (liftM f' s) where+ f' (B b) = B (f b)+ f' (F a) = F a+{-# INLINE liftMBound #-}++-- | A version of 'mapScope' that can be used when you only have the 'Monad'+-- instance+liftMScope :: Monad m => (b -> d) -> (a -> c) -> Scope b m a -> Scope d m c+liftMScope f g (Scope s) = Scope $ liftM (bimap f (liftM g)) s+{-# INLINE liftMScope #-}++-- | Obtain a result by collecting information from bound variables+foldMapBound :: (Foldable f, Monoid r) => (b -> r) -> Scope b f a -> r+foldMapBound f (Scope s) = foldMap f' s where+ f' (B a) = f a+ f' _ = mempty+{-# INLINE foldMapBound #-}++-- | Obtain a result by collecting information from both bound and free+-- variables+foldMapScope :: (Foldable f, Monoid r) =>+ (b -> r) -> (a -> r) -> Scope b f a -> r+foldMapScope f g (Scope s) = foldMap (bifoldMap f (foldMap g)) s+{-# INLINE foldMapScope #-}++-- | 'traverse_' the bound variables in a 'Scope'.+traverseBound_ :: (Applicative g, Foldable f) =>+ (b -> g d) -> Scope b f a -> g ()+traverseBound_ f (Scope s) = traverse_ f' s+ where f' (B a) = () <$ f a+ f' _ = pure ()+{-# INLINE traverseBound_ #-}++-- | 'traverse' both the variables bound by this scope and any free variables.+traverseScope_ :: (Applicative g, Foldable f) =>+ (b -> g d) -> (a -> g c) -> Scope b f a -> g ()+traverseScope_ f g (Scope s) = traverse_ (bitraverse_ f (traverse_ g)) s+{-# INLINE traverseScope_ #-}++-- | mapM_ over the variables bound by this scope+mapMBound_ :: (Monad g, Foldable f) => (b -> g d) -> Scope b f a -> g ()+mapMBound_ f (Scope s) = mapM_ f' s where+ f' (B a) = do _ <- f a; return ()+ f' _ = return ()+{-# INLINE mapMBound_ #-}++-- | A 'traverseScope_' that can be used when you only have a 'Monad'+-- instance+mapMScope_ :: (Monad m, Foldable f) =>+ (b -> m d) -> (a -> m c) -> Scope b f a -> m ()+mapMScope_ f g (Scope s) = mapM_ (bimapM_ f (mapM_ g)) s+{-# INLINE mapMScope_ #-}++-- | 'traverse' the bound variables in a 'Scope'.+traverseBound :: (Applicative g, Traversable f) =>+ (b -> g c) -> Scope b f a -> g (Scope c f a)+traverseBound f (Scope s) = Scope <$> traverse f' s where+ f' (B b) = B <$> f b+ f' (F a) = pure (F a)+{-# INLINE traverseBound #-}++-- | Traverse both bound and free variables+traverseScope :: (Applicative g, Traversable f) =>+ (b -> g d) -> (a -> g c) -> Scope b f a -> g (Scope d f c)+traverseScope f g (Scope s) = Scope <$> traverse (bitraverse f (traverse g)) s+{-# INLINE traverseScope #-}++-- | mapM over both bound and free variables+mapMBound :: (Monad m, Traversable f) =>+ (b -> m c) -> Scope b f a -> m (Scope c f a)+mapMBound f (Scope s) = liftM Scope (mapM f' s) where+ f' (B b) = liftM B (f b)+ f' (F a) = return (F a)+{-# INLINE mapMBound #-}++-- | A 'traverseScope' that can be used when you only have a 'Monad'+-- instance+mapMScope :: (Monad m, Traversable f) =>+ (b -> m d) -> (a -> m c) -> Scope b f a -> m (Scope d f c)+mapMScope f g (Scope s) = liftM Scope (mapM (bimapM f (mapM g)) s)+{-# INLINE mapMScope #-}++serializeScope :: (Serial1 f, MonadPut m) => (b -> m ()) -> (v -> m ()) -> Scope b f v -> m ()+serializeScope pb pv (Scope body) = serializeWith (serializeWith2 pb $ serializeWith pv) body+{-# INLINE serializeScope #-}++deserializeScope :: (Serial1 f, MonadGet m) => m b -> m v -> m (Scope b f v)+deserializeScope gb gv = liftM Scope $ deserializeWith (deserializeWith2 gb $ deserializeWith gv)+{-# INLINE deserializeScope #-}++-- | This allows you to 'bitraverse' a 'Scope'.+bitraverseScope :: (Bitraversable t, Applicative f) => (k -> f k') -> (a -> f a') -> Scope b (t k) a -> f (Scope b (t k') a')+bitraverseScope f = bitransverseScope (bitraverse f)+{-# INLINE bitraverseScope #-}++-- | This is a higher-order analogue of 'traverse'.+transverseScope :: (Applicative f, Monad f, Traversable g)+ => (forall r. g r -> f (h r))+ -> Scope b g a -> f (Scope b h a)+transverseScope tau (Scope e) = Scope <$> (tau =<< traverse (traverse tau) e)++bitransverseScope :: Applicative f => (forall a a'. (a -> f a') -> t a -> f (u a')) -> (c -> f c') -> Scope b t c -> f (Scope b u c')+bitransverseScope tau f = fmap Scope . tau (_F (tau f)) . unscope+{-# INLINE bitransverseScope #-}++-- | instantiate bound variables using a list of new variables+instantiateVars :: Monad t => [a] -> Scope Int t a -> t a+instantiateVars as = instantiate (vs !!) where+ vs = map return as+{-# INLINE instantiateVars #-}++-- | Lift a natural transformation from @f@ to @g@ into one between scopes.+hoistScope :: Functor f => (forall x. f x -> g x) -> Scope b f a -> Scope b g a+hoistScope t (Scope b) = Scope $ t (fmap t <$> b)+{-# INLINE hoistScope #-}++instance (Serial b, Serial1 f) => Serial1 (Scope b f) where+ serializeWith = serializeScope serialize+ deserializeWith = deserializeScope deserialize++instance (Serial b, Serial1 f, Serial a) => Serial (Scope b f a) where+ serialize = serializeScope serialize serialize+ deserialize = deserializeScope deserialize deserialize++instance (Binary b, Serial1 f, Binary a) => Binary (Scope b f a) where+ put = serializeScope Binary.put Binary.put+ get = deserializeScope Binary.get Binary.get++instance (Serialize b, Serial1 f, Serialize a) => Serialize (Scope b f a) where+ put = serializeScope Serialize.put Serialize.put+ get = deserializeScope Serialize.get Serialize.get++#ifdef __GLASGOW_HASKELL__+deriving instance (Typeable b, Typeable f, Data a, Data (f (Var b (f a)))) => Data (Scope b f a)+#endif
src/Bound/Scope/Simple.hs view
@@ -1,434 +1,434 @@-{-# LANGUAGE CPP #-} -{-# LANGUAGE Rank2Types #-} -#if defined(__GLASGOW_HASKELL__) -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE StandaloneDeriving #-} -{-# LANGUAGE DeriveDataTypeable #-} -{-# LANGUAGE DeriveGeneric #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE UndecidableInstances #-} -{-# LANGUAGE Trustworthy #-} -#endif - ------------------------------------------------------------------------------ --- | --- Copyright : (C) 2013 Edward Kmett --- License : BSD-style (see the file LICENSE) --- --- Maintainer : Edward Kmett <ekmett@gmail.com> --- Stability : experimental --- Portability : portable --- --- 'Scope' provides a single traditional de Bruijn level --- and is often used inside of the definition of binders. --- ----------------------------------------------------------------------------- -module Bound.Scope.Simple - (Scope(..) - -- * Abstraction - , abstract, abstract1 - -- * Instantiation - , instantiate, instantiate1 - -- * Alternative names for 'unscope'/'Scope' - , fromScope - , toScope - -- * Bound variable manipulation - , splat - , bindings - , mapBound - , mapScope - , liftMBound - , liftMScope - , foldMapBound - , foldMapScope - , traverseBound_ - , traverseScope_ - , mapMBound_ - , mapMScope_ - , traverseBound - , traverseScope - , mapMBound - , mapMScope - , serializeScope - , deserializeScope - , hoistScope - , bitraverseScope - , bitransverseScope - , transverseScope - , instantiateVars - ) where - -import Bound.Class -import Bound.Var -import Control.Applicative -import Control.DeepSeq -import Control.Monad hiding (mapM, mapM_) -import Control.Monad.Morph -import Data.Bifunctor -import Data.Bifoldable -import qualified Data.Binary as Binary -import Data.Binary (Binary) -import Data.Bitraversable -import Data.Bytes.Get -import Data.Bytes.Put -import Data.Bytes.Serial -import Data.Data -import Data.Foldable -import Data.Functor.Classes -import Data.Hashable (Hashable(..)) -import Data.Hashable.Lifted (Hashable1(..), hashWithSalt1) -import Data.Monoid -import qualified Data.Serialize as Serialize -import Data.Serialize (Serialize) -import Data.Traversable -import Prelude hiding (foldr, mapM, mapM_) -#if defined(__GLASGOW_HASKELL__) -import GHC.Generics (Generic, Generic1) -#endif - --- $setup --- >>> import Bound.Var - -------------------------------------------------------------------------------- --- Scopes -------------------------------------------------------------------------------- - --- | @'Scope' b f a@ is an @f@ expression with bound variables in @b@, --- and free variables in @a@ --- --- This implements traditional de Bruijn indices, while 'Bound.Scope' --- implements generalized de Bruijn indices. --- --- These traditional indices can be used to test the performance gain --- of generalized indices. --- --- While this type 'Scope' is identical to 'Control.Monad.Trans.EitherT' --- this module focuses on a drop-in replacement for 'Bound.Scope'. --- --- Another use case is for syntaxes not stable under substitution, --- therefore with only a 'Functor' instance and no 'Monad' instance. -newtype Scope b f a = Scope { unscope :: f (Var b a) } -#if defined(__GLASGOW_HASKELL__) - deriving Generic -#endif -deriving instance Functor f => Generic1 (Scope b f) - -------------------------------------------------------------------------------- --- Instances -------------------------------------------------------------------------------- - -instance NFData (f (Var b a)) => NFData (Scope b f a) where - rnf (Scope x) = rnf x - -instance Functor f => Functor (Scope b f) where - fmap f (Scope a) = Scope (fmap (fmap f) a) - {-# INLINE fmap #-} - --- | @'toList'@ is provides a list (with duplicates) of the free variables -instance Foldable f => Foldable (Scope b f) where - foldMap f (Scope a) = foldMap (foldMap f) a - {-# INLINE foldMap #-} - -instance Traversable f => Traversable (Scope b f) where - traverse f (Scope a) = Scope <$> traverse (traverse f) a - {-# INLINE traverse #-} - -instance Monad f => Applicative (Scope b f) where - pure a = Scope (return (F a)) - {-# INLINE pure #-} - (<*>) = ap - {-# INLINE (<*>) #-} - --- | The monad permits substitution on free variables, while preserving --- bound variables -instance Monad f => Monad (Scope b f) where - Scope e >>= f = Scope $ e >>= \v -> case v of - B b -> return (B b) - F a -> unscope (f a) - {-# INLINE (>>=) #-} - -instance MonadTrans (Scope b) where - lift ma = Scope (liftM F ma) - {-# INLINE lift #-} - -instance MFunctor (Scope b) where - hoist f = hoistScope f - {-# INLINE hoist #-} - -instance (Eq b, Eq1 f) => Eq1 (Scope b f) where - liftEq f m n = liftEq (liftEq f) (unscope m) (unscope n) - -instance (Ord b, Ord1 f) => Ord1 (Scope b f) where - liftCompare f m n = liftCompare (liftCompare f) (unscope m) (unscope n) - -instance (Show b, Show1 f) => Show1 (Scope b f) where - liftShowsPrec f g d m = showParen (d > 10) $ - showString "Scope " . liftShowsPrec (liftShowsPrec f g) (liftShowList f g) 11 (unscope m) - -instance (Read b, Read1 f) => Read1 (Scope b f) where - liftReadsPrec f g d = readParen (d > 10) $ \r -> do - ("Scope", r') <- lex r - (s, r'') <- liftReadsPrec (liftReadsPrec f g) (liftReadList f g) 11 r' - return (Scope s, r'') - -instance (Eq b, Eq1 f, Eq a) => Eq (Scope b f a) where - (==) = eq1 - -instance (Ord b, Ord1 f, Ord a) => Ord (Scope b f a) where - compare = compare1 - -instance (Show b, Show1 f, Show a) => Show (Scope b f a) where - showsPrec = showsPrec1 - -instance (Read b, Read1 f, Read a) => Read (Scope b f a) where - readsPrec = readsPrec1 - -instance Bound (Scope b) where - Scope m >>>= f = Scope $ m >>= \v -> case v of - B b -> return (B b) - F a -> liftM F (f a) - {-# INLINE (>>>=) #-} - -instance (Hashable b, Hashable1 f) => Hashable1 (Scope b f) where - liftHashWithSalt h n m = liftHashWithSalt (liftHashWithSalt h) n (unscope m) - {-# INLINE liftHashWithSalt #-} - -instance (Hashable b, Hashable1 f, Hashable a) => Hashable (Scope b f a) where - hashWithSalt n m = hashWithSalt1 n (unscope m) - {-# INLINE hashWithSalt #-} - -------------------------------------------------------------------------------- --- Abstraction -------------------------------------------------------------------------------- - --- | Capture some free variables in an expression to yield --- a 'Scope' with bound variables in @b@ --- --- >>> :m + Data.List --- >>> abstract (`elemIndex` "bar") "barry" --- Scope [B 0,B 1,B 2,B 2,F 'y'] -abstract :: Functor f => (a -> Maybe b) -> f a -> Scope b f a -abstract f e = Scope (fmap k e) where - k y = case f y of - Just z -> B z - Nothing -> F y -{-# INLINE abstract #-} - --- | Abstract over a single variable --- --- >>> abstract1 'x' "xyz" --- Scope [B (),F 'y',F 'z'] -abstract1 :: (Functor f, Eq a) => a -> f a -> Scope () f a -abstract1 a = abstract (\b -> if a == b then Just () else Nothing) -{-# INLINE abstract1 #-} - -------------------------------------------------------------------------------- --- Instantiation -------------------------------------------------------------------------------- - --- | Enter a scope, instantiating all bound variables --- --- >>> :m + Data.List --- >>> instantiate (\x -> [toEnum (97 + x)]) $ abstract (`elemIndex` "bar") "barry" --- "abccy" -instantiate :: Monad f => (b -> f a) -> Scope b f a -> f a -instantiate k e = unscope e >>= \v -> case v of - B b -> k b - F a -> return a -{-# INLINE instantiate #-} - --- | Enter a 'Scope' that binds one variable, instantiating it --- --- >>> instantiate1 "x" $ Scope [B (),F 'y',F 'z'] --- "xyz" -instantiate1 :: Monad f => f a -> Scope n f a -> f a -instantiate1 e = instantiate (const e) -{-# INLINE instantiate1 #-} - -hoistScope :: (f (Var b a) -> g (Var b a)) -> Scope b f a -> Scope b g a -hoistScope f = Scope . f . unscope -{-# INLINE hoistScope #-} - -------------------------------------------------------------------------------- --- Compatibility with Bound.Scope -------------------------------------------------------------------------------- - --- | @'fromScope'@ is just another name for 'unscope' and is exported --- to mimick 'Bound.Scope.fromScope'. --- In particular no 'Monad' constraint is required. -fromScope :: Scope b f a -> f (Var b a) -fromScope = unscope -{-# INLINE fromScope #-} - --- | @'toScope'@ is just another name for 'Scope' and is exported --- to mimick 'Bound.Scope.toScope'. --- In particular no 'Monad' constraint is required. -toScope :: f (Var b a) -> Scope b f a -toScope = Scope -{-# INLINE toScope #-} - -------------------------------------------------------------------------------- --- Exotic Traversals of Bound Variables (not exported by default) -------------------------------------------------------------------------------- - --- | Perform substitution on both bound and free variables in a 'Scope'. -splat :: Monad f => (a -> f c) -> (b -> f c) -> Scope b f a -> f c -splat f unbind s = unscope s >>= \v -> case v of - B b -> unbind b - F a -> f a -{-# INLINE splat #-} - --- | Return a list of occurences of the variables bound by this 'Scope'. -bindings :: Foldable f => Scope b f a -> [b] -bindings (Scope s) = foldr f [] s where - f (B v) vs = v : vs - f _ vs = vs -{-# INLINE bindings #-} - --- | Perform a change of variables on bound variables. -mapBound :: Functor f => (b -> b') -> Scope b f a -> Scope b' f a -mapBound f (Scope s) = Scope (fmap f' s) where - f' (B b) = B (f b) - f' (F a) = F a -{-# INLINE mapBound #-} - --- | Perform a change of variables, reassigning both bound and free variables. -mapScope :: Functor f => (b -> d) -> (a -> c) -> Scope b f a -> Scope d f c -mapScope f g (Scope s) = Scope $ fmap (bimap f g) s -{-# INLINE mapScope #-} - --- | Perform a change of variables on bound variables given only a 'Monad' --- instance -liftMBound :: Monad m => (b -> b') -> Scope b m a -> Scope b' m a -liftMBound f (Scope s) = Scope (liftM f' s) where - f' (B b) = B (f b) - f' (F a) = F a -{-# INLINE liftMBound #-} - --- | A version of 'mapScope' that can be used when you only have the 'Monad' --- instance -liftMScope :: Monad m => (b -> d) -> (a -> c) -> Scope b m a -> Scope d m c -liftMScope f g (Scope s) = Scope $ liftM (bimap f g) s -{-# INLINE liftMScope #-} - --- | Obtain a result by collecting information from both bound and free --- variables -foldMapBound :: (Foldable f, Monoid r) => (b -> r) -> Scope b f a -> r -foldMapBound f (Scope s) = foldMap f' s where - f' (B a) = f a - f' _ = mempty -{-# INLINE foldMapBound #-} - --- | Obtain a result by collecting information from both bound and free --- variables -foldMapScope :: (Foldable f, Monoid r) => - (b -> r) -> (a -> r) -> Scope b f a -> r -foldMapScope f g (Scope s) = foldMap (bifoldMap f g) s -{-# INLINE foldMapScope #-} - --- | 'traverse_' the bound variables in a 'Scope'. -traverseBound_ :: (Applicative g, Foldable f) => - (b -> g d) -> Scope b f a -> g () -traverseBound_ f (Scope s) = traverse_ f' s - where f' (B a) = () <$ f a - f' _ = pure () -{-# INLINE traverseBound_ #-} - --- | 'traverse' both the variables bound by this scope and any free variables. -traverseScope_ :: (Applicative g, Foldable f) => - (b -> g d) -> (a -> g c) -> Scope b f a -> g () -traverseScope_ f g (Scope s) = traverse_ (bitraverse_ f g) s -{-# INLINE traverseScope_ #-} - --- | mapM_ over the variables bound by this scope -mapMBound_ :: (Monad g, Foldable f) => (b -> g d) -> Scope b f a -> g () -mapMBound_ f (Scope s) = mapM_ f' s where - f' (B a) = do _ <- f a; return () - f' _ = return () -{-# INLINE mapMBound_ #-} - --- | A 'traverseScope_' that can be used when you only have a 'Monad' --- instance -mapMScope_ :: (Monad m, Foldable f) => - (b -> m d) -> (a -> m c) -> Scope b f a -> m () -mapMScope_ f g (Scope s) = mapM_ (bimapM_ f g) s -{-# INLINE mapMScope_ #-} - --- | Traverse both bound and free variables -traverseBound :: (Applicative g, Traversable f) => - (b -> g c) -> Scope b f a -> g (Scope c f a) -traverseBound f (Scope s) = Scope <$> traverse f' s where - f' (B b) = B <$> f b - f' (F a) = pure (F a) -{-# INLINE traverseBound #-} - --- | Traverse both bound and free variables -traverseScope :: (Applicative g, Traversable f) => - (b -> g d) -> (a -> g c) -> Scope b f a -> g (Scope d f c) -traverseScope f g (Scope s) = Scope <$> traverse (bitraverse f g) s -{-# INLINE traverseScope #-} - --- | This allows you to 'bitraverse' a 'Scope'. -bitraverseScope :: (Bitraversable t, Applicative f) => (k -> f k') -> (a -> f a') -> Scope b (t k) a -> f (Scope b (t k') a') -bitraverseScope f = bitransverseScope (bitraverse f) -{-# INLINE bitraverseScope #-} - --- | This is a higher-order analogue of 'traverse'. -transverseScope :: (Functor f) - => (forall r. g r -> f (h r)) - -> Scope b g a -> f (Scope b h a) -transverseScope tau (Scope s) = Scope <$> tau s - --- | instantiate bound variables using a list of new variables -instantiateVars :: Monad t => [a] -> Scope Int t a -> t a -instantiateVars as = instantiate (vs !!) where - vs = map return as -{-# INLINE instantiateVars #-} - -bitransverseScope :: Applicative f => (forall a a'. (a -> f a') -> t a -> f (u a')) - -> forall a a'. (a -> f a') -> Scope b t a -> f (Scope b u a') -bitransverseScope tau f (Scope s) = Scope <$> tau (traverse f) s -{-# INLINE bitransverseScope #-} - --- | mapM over both bound and free variables -mapMBound :: (Monad m, Traversable f) => - (b -> m c) -> Scope b f a -> m (Scope c f a) -mapMBound f (Scope s) = liftM Scope (mapM f' s) where - f' (B b) = liftM B (f b) - f' (F a) = return (F a) -{-# INLINE mapMBound #-} - --- | A 'traverseScope' that can be used when you only have a 'Monad' --- instance -mapMScope :: (Monad m, Traversable f) => - (b -> m d) -> (a -> m c) -> Scope b f a -> m (Scope d f c) -mapMScope f g (Scope s) = liftM Scope (mapM (bimapM f g) s) -{-# INLINE mapMScope #-} - -serializeScope :: (Serial1 f, MonadPut m) => (b -> m ()) -> (v -> m ()) -> Scope b f v -> m () -serializeScope pb pv (Scope body) = serializeWith (serializeWith2 pb pv) body -{-# INLINE serializeScope #-} - -deserializeScope :: (Serial1 f, MonadGet m) => m b -> m v -> m (Scope b f v) -deserializeScope gb gv = liftM Scope $ deserializeWith (deserializeWith2 gb gv) -{-# INLINE deserializeScope #-} - -instance (Serial b, Serial1 f) => Serial1 (Scope b f) where - serializeWith = serializeScope serialize - deserializeWith = deserializeScope deserialize - -instance (Serial b, Serial1 f, Serial a) => Serial (Scope b f a) where - serialize = serializeScope serialize serialize - deserialize = deserializeScope deserialize deserialize - -instance (Binary b, Serial1 f, Binary a) => Binary (Scope b f a) where - put = serializeScope Binary.put Binary.put - get = deserializeScope Binary.get Binary.get - -instance (Serialize b, Serial1 f, Serialize a) => Serialize (Scope b f a) where - put = serializeScope Serialize.put Serialize.put - get = deserializeScope Serialize.get Serialize.get - -#ifdef __GLASGOW_HASKELL__ -deriving instance (Typeable b, Typeable f, Data a, Data (f (Var b a))) => Data (Scope b f a) -#endif +{-# LANGUAGE CPP #-}+{-# LANGUAGE Rank2Types #-}+#if defined(__GLASGOW_HASKELL__)+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE Trustworthy #-}+#endif++-----------------------------------------------------------------------------+-- |+-- Copyright : (C) 2013 Edward Kmett+-- License : BSD-style (see the file LICENSE)+--+-- Maintainer : Edward Kmett <ekmett@gmail.com>+-- Stability : experimental+-- Portability : portable+--+-- 'Scope' provides a single traditional de Bruijn level+-- and is often used inside of the definition of binders.+--+----------------------------------------------------------------------------+module Bound.Scope.Simple+ (Scope(..)+ -- * Abstraction+ , abstract, abstract1+ -- * Instantiation+ , instantiate, instantiate1+ -- * Alternative names for 'unscope'/'Scope'+ , fromScope+ , toScope+ -- * Bound variable manipulation+ , splat+ , bindings+ , mapBound+ , mapScope+ , liftMBound+ , liftMScope+ , foldMapBound+ , foldMapScope+ , traverseBound_+ , traverseScope_+ , mapMBound_+ , mapMScope_+ , traverseBound+ , traverseScope+ , mapMBound+ , mapMScope+ , serializeScope+ , deserializeScope+ , hoistScope+ , bitraverseScope+ , bitransverseScope+ , transverseScope+ , instantiateVars+ ) where++import Bound.Class+import Bound.Var+import Control.Applicative+import Control.DeepSeq+import Control.Monad hiding (mapM, mapM_)+import Control.Monad.Morph+import Data.Bifunctor+import Data.Bifoldable+import qualified Data.Binary as Binary+import Data.Binary (Binary)+import Data.Bitraversable+import Data.Bytes.Get+import Data.Bytes.Put+import Data.Bytes.Serial+import Data.Data+import Data.Foldable+import Data.Functor.Classes+import Data.Hashable (Hashable(..))+import Data.Hashable.Lifted (Hashable1(..), hashWithSalt1)+import Data.Monoid+import qualified Data.Serialize as Serialize+import Data.Serialize (Serialize)+import Data.Traversable+import Prelude hiding (foldr, mapM, mapM_)+#if defined(__GLASGOW_HASKELL__)+import GHC.Generics (Generic, Generic1)+#endif++-- $setup+-- >>> import Bound.Var++-------------------------------------------------------------------------------+-- Scopes+-------------------------------------------------------------------------------++-- | @'Scope' b f a@ is an @f@ expression with bound variables in @b@,+-- and free variables in @a@+--+-- This implements traditional de Bruijn indices, while 'Bound.Scope'+-- implements generalized de Bruijn indices.+--+-- These traditional indices can be used to test the performance gain+-- of generalized indices.+--+-- While this type 'Scope' is identical to 'Control.Monad.Trans.EitherT'+-- this module focuses on a drop-in replacement for 'Bound.Scope'.+--+-- Another use case is for syntaxes not stable under substitution,+-- therefore with only a 'Functor' instance and no 'Monad' instance.+newtype Scope b f a = Scope { unscope :: f (Var b a) }+#if defined(__GLASGOW_HASKELL__)+ deriving Generic+#endif+deriving instance Functor f => Generic1 (Scope b f)++-------------------------------------------------------------------------------+-- Instances+-------------------------------------------------------------------------------++instance NFData (f (Var b a)) => NFData (Scope b f a) where+ rnf (Scope x) = rnf x++instance Functor f => Functor (Scope b f) where+ fmap f (Scope a) = Scope (fmap (fmap f) a)+ {-# INLINE fmap #-}++-- | @'toList'@ is provides a list (with duplicates) of the free variables+instance Foldable f => Foldable (Scope b f) where+ foldMap f (Scope a) = foldMap (foldMap f) a+ {-# INLINE foldMap #-}++instance Traversable f => Traversable (Scope b f) where+ traverse f (Scope a) = Scope <$> traverse (traverse f) a+ {-# INLINE traverse #-}++instance Monad f => Applicative (Scope b f) where+ pure a = Scope (return (F a))+ {-# INLINE pure #-}+ (<*>) = ap+ {-# INLINE (<*>) #-}++-- | The monad permits substitution on free variables, while preserving+-- bound variables+instance Monad f => Monad (Scope b f) where+ Scope e >>= f = Scope $ e >>= \v -> case v of+ B b -> return (B b)+ F a -> unscope (f a)+ {-# INLINE (>>=) #-}++instance MonadTrans (Scope b) where+ lift ma = Scope (liftM F ma)+ {-# INLINE lift #-}++instance MFunctor (Scope b) where+ hoist f = hoistScope f+ {-# INLINE hoist #-}++instance (Eq b, Eq1 f) => Eq1 (Scope b f) where+ liftEq f m n = liftEq (liftEq f) (unscope m) (unscope n)++instance (Ord b, Ord1 f) => Ord1 (Scope b f) where+ liftCompare f m n = liftCompare (liftCompare f) (unscope m) (unscope n)++instance (Show b, Show1 f) => Show1 (Scope b f) where+ liftShowsPrec f g d m = showParen (d > 10) $+ showString "Scope " . liftShowsPrec (liftShowsPrec f g) (liftShowList f g) 11 (unscope m)++instance (Read b, Read1 f) => Read1 (Scope b f) where+ liftReadsPrec f g d = readParen (d > 10) $ \r -> do+ ("Scope", r') <- lex r+ (s, r'') <- liftReadsPrec (liftReadsPrec f g) (liftReadList f g) 11 r'+ return (Scope s, r'')++instance (Eq b, Eq1 f, Eq a) => Eq (Scope b f a) where+ (==) = eq1++instance (Ord b, Ord1 f, Ord a) => Ord (Scope b f a) where+ compare = compare1++instance (Show b, Show1 f, Show a) => Show (Scope b f a) where+ showsPrec = showsPrec1++instance (Read b, Read1 f, Read a) => Read (Scope b f a) where+ readsPrec = readsPrec1++instance Bound (Scope b) where+ Scope m >>>= f = Scope $ m >>= \v -> case v of+ B b -> return (B b)+ F a -> liftM F (f a)+ {-# INLINE (>>>=) #-}++instance (Hashable b, Hashable1 f) => Hashable1 (Scope b f) where+ liftHashWithSalt h n m = liftHashWithSalt (liftHashWithSalt h) n (unscope m)+ {-# INLINE liftHashWithSalt #-}++instance (Hashable b, Hashable1 f, Hashable a) => Hashable (Scope b f a) where+ hashWithSalt n m = hashWithSalt1 n (unscope m)+ {-# INLINE hashWithSalt #-}++-------------------------------------------------------------------------------+-- Abstraction+-------------------------------------------------------------------------------++-- | Capture some free variables in an expression to yield+-- a 'Scope' with bound variables in @b@+--+-- >>> :m + Data.List+-- >>> abstract (`elemIndex` "bar") "barry"+-- Scope [B 0,B 1,B 2,B 2,F 'y']+abstract :: Functor f => (a -> Maybe b) -> f a -> Scope b f a+abstract f e = Scope (fmap k e) where+ k y = case f y of+ Just z -> B z+ Nothing -> F y+{-# INLINE abstract #-}++-- | Abstract over a single variable+--+-- >>> abstract1 'x' "xyz"+-- Scope [B (),F 'y',F 'z']+abstract1 :: (Functor f, Eq a) => a -> f a -> Scope () f a+abstract1 a = abstract (\b -> if a == b then Just () else Nothing)+{-# INLINE abstract1 #-}++-------------------------------------------------------------------------------+-- Instantiation+-------------------------------------------------------------------------------++-- | Enter a scope, instantiating all bound variables+--+-- >>> :m + Data.List+-- >>> instantiate (\x -> [toEnum (97 + x)]) $ abstract (`elemIndex` "bar") "barry"+-- "abccy"+instantiate :: Monad f => (b -> f a) -> Scope b f a -> f a+instantiate k e = unscope e >>= \v -> case v of+ B b -> k b+ F a -> return a+{-# INLINE instantiate #-}++-- | Enter a 'Scope' that binds one variable, instantiating it+--+-- >>> instantiate1 "x" $ Scope [B (),F 'y',F 'z']+-- "xyz"+instantiate1 :: Monad f => f a -> Scope n f a -> f a+instantiate1 e = instantiate (const e)+{-# INLINE instantiate1 #-}++hoistScope :: (f (Var b a) -> g (Var b a)) -> Scope b f a -> Scope b g a+hoistScope f = Scope . f . unscope+{-# INLINE hoistScope #-}++-------------------------------------------------------------------------------+-- Compatibility with Bound.Scope+-------------------------------------------------------------------------------++-- | @'fromScope'@ is just another name for 'unscope' and is exported+-- to mimick 'Bound.Scope.fromScope'.+-- In particular no 'Monad' constraint is required.+fromScope :: Scope b f a -> f (Var b a)+fromScope = unscope+{-# INLINE fromScope #-}++-- | @'toScope'@ is just another name for 'Scope' and is exported+-- to mimick 'Bound.Scope.toScope'.+-- In particular no 'Monad' constraint is required.+toScope :: f (Var b a) -> Scope b f a+toScope = Scope+{-# INLINE toScope #-}++-------------------------------------------------------------------------------+-- Exotic Traversals of Bound Variables (not exported by default)+-------------------------------------------------------------------------------++-- | Perform substitution on both bound and free variables in a 'Scope'.+splat :: Monad f => (a -> f c) -> (b -> f c) -> Scope b f a -> f c+splat f unbind s = unscope s >>= \v -> case v of+ B b -> unbind b+ F a -> f a+{-# INLINE splat #-}++-- | Return a list of occurences of the variables bound by this 'Scope'.+bindings :: Foldable f => Scope b f a -> [b]+bindings (Scope s) = foldr f [] s where+ f (B v) vs = v : vs+ f _ vs = vs+{-# INLINE bindings #-}++-- | Perform a change of variables on bound variables.+mapBound :: Functor f => (b -> b') -> Scope b f a -> Scope b' f a+mapBound f (Scope s) = Scope (fmap f' s) where+ f' (B b) = B (f b)+ f' (F a) = F a+{-# INLINE mapBound #-}++-- | Perform a change of variables, reassigning both bound and free variables.+mapScope :: Functor f => (b -> d) -> (a -> c) -> Scope b f a -> Scope d f c+mapScope f g (Scope s) = Scope $ fmap (bimap f g) s+{-# INLINE mapScope #-}++-- | Perform a change of variables on bound variables given only a 'Monad'+-- instance+liftMBound :: Monad m => (b -> b') -> Scope b m a -> Scope b' m a+liftMBound f (Scope s) = Scope (liftM f' s) where+ f' (B b) = B (f b)+ f' (F a) = F a+{-# INLINE liftMBound #-}++-- | A version of 'mapScope' that can be used when you only have the 'Monad'+-- instance+liftMScope :: Monad m => (b -> d) -> (a -> c) -> Scope b m a -> Scope d m c+liftMScope f g (Scope s) = Scope $ liftM (bimap f g) s+{-# INLINE liftMScope #-}++-- | Obtain a result by collecting information from both bound and free+-- variables+foldMapBound :: (Foldable f, Monoid r) => (b -> r) -> Scope b f a -> r+foldMapBound f (Scope s) = foldMap f' s where+ f' (B a) = f a+ f' _ = mempty+{-# INLINE foldMapBound #-}++-- | Obtain a result by collecting information from both bound and free+-- variables+foldMapScope :: (Foldable f, Monoid r) =>+ (b -> r) -> (a -> r) -> Scope b f a -> r+foldMapScope f g (Scope s) = foldMap (bifoldMap f g) s+{-# INLINE foldMapScope #-}++-- | 'traverse_' the bound variables in a 'Scope'.+traverseBound_ :: (Applicative g, Foldable f) =>+ (b -> g d) -> Scope b f a -> g ()+traverseBound_ f (Scope s) = traverse_ f' s+ where f' (B a) = () <$ f a+ f' _ = pure ()+{-# INLINE traverseBound_ #-}++-- | 'traverse' both the variables bound by this scope and any free variables.+traverseScope_ :: (Applicative g, Foldable f) =>+ (b -> g d) -> (a -> g c) -> Scope b f a -> g ()+traverseScope_ f g (Scope s) = traverse_ (bitraverse_ f g) s+{-# INLINE traverseScope_ #-}++-- | mapM_ over the variables bound by this scope+mapMBound_ :: (Monad g, Foldable f) => (b -> g d) -> Scope b f a -> g ()+mapMBound_ f (Scope s) = mapM_ f' s where+ f' (B a) = do _ <- f a; return ()+ f' _ = return ()+{-# INLINE mapMBound_ #-}++-- | A 'traverseScope_' that can be used when you only have a 'Monad'+-- instance+mapMScope_ :: (Monad m, Foldable f) =>+ (b -> m d) -> (a -> m c) -> Scope b f a -> m ()+mapMScope_ f g (Scope s) = mapM_ (bimapM_ f g) s+{-# INLINE mapMScope_ #-}++-- | Traverse both bound and free variables+traverseBound :: (Applicative g, Traversable f) =>+ (b -> g c) -> Scope b f a -> g (Scope c f a)+traverseBound f (Scope s) = Scope <$> traverse f' s where+ f' (B b) = B <$> f b+ f' (F a) = pure (F a)+{-# INLINE traverseBound #-}++-- | Traverse both bound and free variables+traverseScope :: (Applicative g, Traversable f) =>+ (b -> g d) -> (a -> g c) -> Scope b f a -> g (Scope d f c)+traverseScope f g (Scope s) = Scope <$> traverse (bitraverse f g) s+{-# INLINE traverseScope #-}++-- | This allows you to 'bitraverse' a 'Scope'.+bitraverseScope :: (Bitraversable t, Applicative f) => (k -> f k') -> (a -> f a') -> Scope b (t k) a -> f (Scope b (t k') a')+bitraverseScope f = bitransverseScope (bitraverse f)+{-# INLINE bitraverseScope #-}++-- | This is a higher-order analogue of 'traverse'.+transverseScope :: (Functor f)+ => (forall r. g r -> f (h r))+ -> Scope b g a -> f (Scope b h a)+transverseScope tau (Scope s) = Scope <$> tau s++-- | instantiate bound variables using a list of new variables+instantiateVars :: Monad t => [a] -> Scope Int t a -> t a+instantiateVars as = instantiate (vs !!) where+ vs = map return as+{-# INLINE instantiateVars #-}++bitransverseScope :: Applicative f => (forall a a'. (a -> f a') -> t a -> f (u a'))+ -> forall a a'. (a -> f a') -> Scope b t a -> f (Scope b u a')+bitransverseScope tau f (Scope s) = Scope <$> tau (traverse f) s+{-# INLINE bitransverseScope #-}++-- | mapM over both bound and free variables+mapMBound :: (Monad m, Traversable f) =>+ (b -> m c) -> Scope b f a -> m (Scope c f a)+mapMBound f (Scope s) = liftM Scope (mapM f' s) where+ f' (B b) = liftM B (f b)+ f' (F a) = return (F a)+{-# INLINE mapMBound #-}++-- | A 'traverseScope' that can be used when you only have a 'Monad'+-- instance+mapMScope :: (Monad m, Traversable f) =>+ (b -> m d) -> (a -> m c) -> Scope b f a -> m (Scope d f c)+mapMScope f g (Scope s) = liftM Scope (mapM (bimapM f g) s)+{-# INLINE mapMScope #-}++serializeScope :: (Serial1 f, MonadPut m) => (b -> m ()) -> (v -> m ()) -> Scope b f v -> m ()+serializeScope pb pv (Scope body) = serializeWith (serializeWith2 pb pv) body+{-# INLINE serializeScope #-}++deserializeScope :: (Serial1 f, MonadGet m) => m b -> m v -> m (Scope b f v)+deserializeScope gb gv = liftM Scope $ deserializeWith (deserializeWith2 gb gv)+{-# INLINE deserializeScope #-}++instance (Serial b, Serial1 f) => Serial1 (Scope b f) where+ serializeWith = serializeScope serialize+ deserializeWith = deserializeScope deserialize++instance (Serial b, Serial1 f, Serial a) => Serial (Scope b f a) where+ serialize = serializeScope serialize serialize+ deserialize = deserializeScope deserialize deserialize++instance (Binary b, Serial1 f, Binary a) => Binary (Scope b f a) where+ put = serializeScope Binary.put Binary.put+ get = deserializeScope Binary.get Binary.get++instance (Serialize b, Serial1 f, Serialize a) => Serialize (Scope b f a) where+ put = serializeScope Serialize.put Serialize.put+ get = deserializeScope Serialize.get Serialize.get++#ifdef __GLASGOW_HASKELL__+deriving instance (Typeable b, Typeable f, Data a, Data (f (Var b a))) => Data (Scope b f a)+#endif
src/Bound/TH.hs view
@@ -1,341 +1,345 @@-{-# LANGUAGE CPP #-} -{-# LANGUAGE PatternGuards #-} - -#if __GLASGOW_HASKELL__ >= 900 -{-# LANGUAGE TemplateHaskellQuotes #-} -#else -{-# LANGUAGE TemplateHaskell #-} -#endif - ------------------------------------------------------------------------------ --- | --- Copyright : (C) 2012-2013 Edward Kmett --- License : BSD-style (see the file LICENSE) --- --- Maintainer : Edward Kmett <ekmett@gmail.com> --- Stability : experimental --- Portability : portable --- --- This is a Template Haskell module for deriving 'Applicative' and --- 'Monad' instances for data types. ----------------------------------------------------------------------------- - -module Bound.TH - ( -#ifdef MIN_VERSION_template_haskell - makeBound -#endif - ) where - -#ifdef MIN_VERSION_template_haskell -import Data.List (intercalate) -import Data.Traversable (for) -import Control.Monad (foldM, mzero, guard) -import Bound.Class (Bound((>>>=))) -import Language.Haskell.TH -import Language.Haskell.TH.Datatype.TyVarBndr - -import Control.Monad.Trans.Class (lift) -import Control.Monad.Trans.Maybe (MaybeT (..)) - --- | --- Use to automatically derive 'Applicative' and 'Monad' instances for --- your datatype. --- --- Also works for components that are lists or instances of 'Functor', --- but still does not work for a great deal of other things. --- --- The @deriving-compat@ package may be used to derive the 'Show1' and 'Read1' --- instances. Note that due to Template Haskell staging restrictions, we must --- define these instances within the same TH splice as the 'Show' and 'Read' --- instances. (This is needed for GHC 9.6 and later, where 'Show' and 'Read' --- are quantified superclasses of 'Show1' and 'Read1', respectively.) --- --- @ --- {-\# LANGUAGE DeriveFunctor #-} --- {-\# LANGUAGE TemplateHaskell #-} --- --- import Bound (Scope, makeBound) --- import Data.Functor.Classes (Show1, Read1, showsPrec1, readsPrec1) --- import Data.Deriving (deriveShow1, deriveRead1) --- --- data Exp a --- = V a --- | App (Exp a) (Exp a) --- | Lam (Scope () Exp a) --- | ND [Exp a] --- | I Int --- deriving (Functor) --- --- makeBound ''Exp --- --- concat <$> sequence --- [ deriveShow1 ''Exp --- , deriveRead1 ''Exp --- , [d| instance Read a => Read (Exp a) where readsPrec = readsPrec1 --- instance Show a => Show (Exp a) where showsPrec = showsPrec1 --- |] --- ] --- @ --- --- and in GHCi --- --- @ --- ghci> :set -XDeriveFunctor --- ghci> :set -XTemplateHaskell --- ghci> import Bound (Scope, makeBound) --- ghci> import Data.Functor.Classes (Show1, Read1, showsPrec1, readsPrec1) --- ghci> import Data.Deriving (deriveShow1, deriveRead1) --- ghci> :{ --- ghci| data Exp a = V a | App (Exp a) (Exp a) | Lam (Scope () Exp a) | ND [Exp a] | I Int deriving (Functor) --- ghci| makeBound ''Exp --- ghci| fmap concat $ sequence [deriveShow1 ''Exp, deriveRead1 ''Exp, [d| instance Read a => Read (Exp a) where { readsPrec = readsPrec1 }; instance Show a => Show (Exp a) where { showsPrec = showsPrec1 } |]] --- ghci| :} --- @ --- --- The 'Eq' and 'Ord' instances can be derived similarly: --- --- @ --- import Data.Functor.Classes (Eq1, Ord1, eq1, compare1) --- import Data.Deriving (deriveEq1, deriveOrd1) --- --- fmap concat $ sequence --- [ deriveEq1 ''Exp --- , deriveOrd1 ''Exp --- , [d| instance Eq a => Eq (Exp a) where (==) = eq1 --- instance Ord a => Ord (Exp a) where compare = compare1 --- |] --- ] --- @ --- --- or in GHCi: --- --- @ --- ghci> import Data.Functor.Classes (Eq1, Ord1, eq1, compare1) --- ghci> import Data.Deriving (deriveEq1, deriveOrd1) --- ghci> :{ --- ghci| fmap concat $ sequence [deriveEq1 ''Exp, deriveOrd1 ''Exp, [d| instance Eq a => Eq (Exp a) where { (==) = eq1 }; instance Ord a => Ord (Exp a) where { compare = compare1 } |]] --- ghci| :} --- @ --- --- We cannot automatically derive 'Eq' and 'Ord' using the standard GHC mechanism, --- because instances require @Exp@ to be a 'Monad': --- --- @ --- instance (Monad f, Eq b, Eq1 f, Eq a) => Eq (Scope b f a) --- instance (Monad f, Ord b, Ord1 f, Ord a) => Ord (Scope b f a) --- @ - -makeBound :: Name -> DecsQ -makeBound name = do - TyConI dec <- reify name - case dec of - DataD _ _name vars _ cons _ -> makeBound' name vars cons - _ -> fail $ show name ++ " Must be a data type." - -makeBound' :: Name -> [TyVarBndrUnit] -> [Con] -> DecsQ -makeBound' name vars cons = do - let instanceHead :: Type - instanceHead = name `conAppsT` map VarT (typeVars (init vars)) - - var :: ExpQ - var = ConE `fmap` getPure name vars cons - - bind :: ExpQ - bind = constructBind name vars cons - - [d| instance Applicative $(pure instanceHead) where - pure = $var - {-# INLINE pure #-} - - ff <*> fy = do - f <- ff - y <- fy - pure (f y) - {-# INLINE (<*>) #-} - - instance Monad $(pure instanceHead) where - (>>=) = $bind - {-# INLINE (>>=) #-} - |] - --- Internals -data Prop - = Bound - | Konst - | Funktor Int -- ^ number tells how many layers are there - | Exp - deriving Show - -data Components - = Component Name [(Name, Prop)] - | Variable Name - deriving Show - -constructBind :: Name -> [TyVarBndrUnit] -> [Con] -> ExpQ -constructBind name vars cons = do - interpret =<< construct name vars cons - -construct :: Name -> [TyVarBndrUnit] -> [Con] -> Q [Components] -construct name vars constructors = do - var <- getPure name vars constructors - for constructors $ \con -> do - case con of - NormalC conName [(_, _)] - | conName == var - -> pure (Variable conName) - NormalC conName types - -> Component conName `fmap` mapM typeToBnd [ ty | (_, ty) <- types ] - RecC conName types - -> Component conName `fmap` mapM typeToBnd [ ty | (_, _, ty) <- types ] - InfixC (_, a) conName (_, b) - -> do - bndA <- typeToBnd a - bndB <- typeToBnd b - pure (Component conName [bndA, bndB]) - _ -> error "Not implemented." - - where - expa :: Type - expa = name `conAppsT` map VarT (typeVars vars) - - typeToBnd :: Type -> Q (Name, Prop) - typeToBnd ty = do - boundInstance <- isBound ty - functorApp <- isFunctorApp ty - var <- newName "var" - pure $ case () of - _ | ty == expa -> (var, Exp) - | boundInstance -> (var, Bound) - | isKonst ty -> (var, Konst) - | Just n <- functorApp -> (var, Funktor n) - | otherwise -> error $ "This is bad: " - ++ show ty - ++ " " - ++ show boundInstance - - -- Checks whether a type is an instance of Bound by stripping its last - -- two type arguments: - -- isBound (Scope () EXP a) - -- -> isInstance ''Bound [Scope ()] - -- -> True - isBound :: Type -> Q Bool - isBound ty - -- We might fail with kind error, but we don't care - | Just a <- stripLast2 ty = pure False `recover` isInstance ''Bound [a] - | otherwise = return False - - isKonst :: Type -> Bool - isKonst ConT {} = True - isKonst (VarT n) = n /= tvName (last vars) - isKonst (AppT a b) = isKonst a && isKonst b - isKonst _ = False - - isFunctorApp :: Type -> Q (Maybe Int) - isFunctorApp = runMaybeT . go - where - go x | x == expa = pure 0 - go (f `AppT` x) = do - isFunctor <- lift $ isInstance ''Functor [f] - guard isFunctor - n <- go x - pure $ n + 1 - go _ = mzero - -interpret :: [Components] -> ExpQ -interpret bnds = do - x <- newName "x" - f <- newName "f" - - let - bind :: Components -> MatchQ - bind (Variable name) = do - a <- newName "a" - match - (conP name [varP a]) - (normalB (varE f `appE` varE a)) - [] - - bind (Component name bounds) = do - exprs <- foldM bindOne (ConE name) bounds - pure $ - Match - (ConP name -#if MIN_VERSION_template_haskell(2,18,0) - [] -#endif - [ VarP arg | (arg, _) <- bounds ]) - (NormalB - exprs) - [] - - bindOne :: Exp -> (Name, Prop) -> Q Exp - bindOne expr (name, bnd) = case bnd of - Bound -> - pure expr `appE` (varE '(>>>=) `appE` varE name `appE` varE f) - Konst -> - pure expr `appE` varE name - Exp -> - pure expr `appE` (varE '(>>=) `appE` varE name `appE` varE f) - Funktor n -> - pure expr `appE` (pure (fmapN n) `appE` (varE '(>>=) `sectionR` varE f) `appE` varE name) - - fmapN :: Int -> Exp - fmapN n = foldr1 (\a b -> VarE '(.) `AppE` a `AppE` b) $ replicate n (VarE 'fmap) - - matches <- for bnds bind - pure $ LamE [VarP x, VarP f] (CaseE (VarE x) matches) - -stripLast2 :: Type -> Maybe Type -stripLast2 (a `AppT` b `AppT` _ `AppT` d) - | AppT{} <- d = Nothing - | otherwise = Just (a `AppT` b) -stripLast2 _ = Nothing - --- Returns candidate -getPure :: Name -> [TyVarBndrUnit] -> [Con] -> Q Name -getPure _name tyvr cons= do - let - findReturn :: Type -> [(Name, [Type])] -> Name - findReturn ty constrs = - case [ constr | (constr, [ty']) <- constrs, ty' == ty ] of - [] -> error "Too few candidates for a variable constructor." - [x] -> x - -- data Exp a = Var1 a | Var2 a | ... - -- result in - -- Too many candidates: Var1, Var2 - xs -> error ("Too many candidates: " ++ intercalate ", " (map pprint xs)) - - -- Gets the last type variable, given 'data Exp a b c = ...' - -- - -- lastTyVar = c - lastTyVar :: Type - lastTyVar = VarT (last (typeVars tyvr)) - - allTypeArgs :: Con -> (Name, [Type]) - allTypeArgs con = case con of - NormalC conName tys -> - (conName, [ ty | (_, ty) <- tys ]) - RecC conName tys -> - (conName, [ ty | (_, _, ty) <- tys ]) - InfixC (_, t1) conName (_, t2) -> - (conName, [ t1, t2 ]) - ForallC _ _ conName -> - allTypeArgs conName - _ -> error "Not implemented" - - return (findReturn lastTyVar (allTypeArgs `fmap` cons)) - -------------------------------------------------------------------------------- --- Type mangling -------------------------------------------------------------------------------- - --- | Extract type variables -typeVars :: [TyVarBndr_ flag] -> [Name] -typeVars = map tvName - --- | Apply arguments to a type constructor. -conAppsT :: Name -> [Type] -> Type -conAppsT conName = foldl AppT (ConT conName) -#else -#endif +{-# LANGUAGE CPP #-}+{-# LANGUAGE PatternGuards #-}++#if __GLASGOW_HASKELL__ >= 900+{-# LANGUAGE TemplateHaskellQuotes #-}+#else+{-# LANGUAGE TemplateHaskell #-}+#endif++-----------------------------------------------------------------------------+-- |+-- Copyright : (C) 2012-2013 Edward Kmett+-- License : BSD-style (see the file LICENSE)+--+-- Maintainer : Edward Kmett <ekmett@gmail.com>+-- Stability : experimental+-- Portability : portable+--+-- This is a Template Haskell module for deriving 'Applicative' and+-- 'Monad' instances for data types.+----------------------------------------------------------------------------++module Bound.TH+ (+#ifdef MIN_VERSION_template_haskell+ makeBound+#endif+ ) where++#ifdef MIN_VERSION_template_haskell+import Data.List (intercalate)+import Data.Traversable (for)+import Control.Monad (foldM, mzero, guard)+import Bound.Class (Bound((>>>=)))+import Language.Haskell.TH+import Language.Haskell.TH.Datatype.TyVarBndr++import Control.Monad.Trans.Class (lift)+import Control.Monad.Trans.Maybe (MaybeT (..))++-- |+-- Use to automatically derive 'Applicative' and 'Monad' instances for+-- your datatype.+--+-- Also works for components that are lists or instances of 'Functor',+-- but still does not work for a great deal of other things.+--+-- The @deriving-compat@ package may be used to derive the 'Show1' and 'Read1'+-- instances. Note that due to Template Haskell staging restrictions, we must+-- define these instances within the same TH splice as the 'Show' and 'Read'+-- instances. (This is needed for GHC 9.6 and later, where 'Show' and 'Read'+-- are quantified superclasses of 'Show1' and 'Read1', respectively.)+--+-- @+-- {-\# LANGUAGE DeriveFunctor #-}+-- {-\# LANGUAGE TemplateHaskell #-}+--+-- import Bound (Scope, makeBound)+-- import Data.Functor.Classes (Show1, Read1, showsPrec1, readsPrec1)+-- import Data.Deriving (deriveShow1, deriveRead1)+--+-- data Exp a+-- = V a+-- | App (Exp a) (Exp a)+-- | Lam (Scope () Exp a)+-- | ND [Exp a]+-- | I Int+-- deriving (Functor)+--+-- makeBound ''Exp+--+-- concat <$> sequence+-- [ deriveShow1 ''Exp+-- , deriveRead1 ''Exp+-- , [d| instance Read a => Read (Exp a) where readsPrec = readsPrec1+-- instance Show a => Show (Exp a) where showsPrec = showsPrec1+-- |]+-- ]+-- @+--+-- and in GHCi+--+-- @+-- ghci> :set -XDeriveFunctor+-- ghci> :set -XTemplateHaskell+-- ghci> import Bound (Scope, makeBound)+-- ghci> import Data.Functor.Classes (Show1, Read1, showsPrec1, readsPrec1)+-- ghci> import Data.Deriving (deriveShow1, deriveRead1)+-- ghci> :{+-- ghci| data Exp a = V a | App (Exp a) (Exp a) | Lam (Scope () Exp a) | ND [Exp a] | I Int deriving (Functor)+-- ghci| makeBound ''Exp+-- ghci| fmap concat $ sequence [deriveShow1 ''Exp, deriveRead1 ''Exp, [d| instance Read a => Read (Exp a) where { readsPrec = readsPrec1 }; instance Show a => Show (Exp a) where { showsPrec = showsPrec1 } |]]+-- ghci| :}+-- @+--+-- The 'Eq' and 'Ord' instances can be derived similarly:+--+-- @+-- import Data.Functor.Classes (Eq1, Ord1, eq1, compare1)+-- import Data.Deriving (deriveEq1, deriveOrd1)+--+-- fmap concat $ sequence+-- [ deriveEq1 ''Exp+-- , deriveOrd1 ''Exp+-- , [d| instance Eq a => Eq (Exp a) where (==) = eq1+-- instance Ord a => Ord (Exp a) where compare = compare1+-- |]+-- ]+-- @+--+-- or in GHCi:+--+-- @+-- ghci> import Data.Functor.Classes (Eq1, Ord1, eq1, compare1)+-- ghci> import Data.Deriving (deriveEq1, deriveOrd1)+-- ghci> :{+-- ghci| fmap concat $ sequence [deriveEq1 ''Exp, deriveOrd1 ''Exp, [d| instance Eq a => Eq (Exp a) where { (==) = eq1 }; instance Ord a => Ord (Exp a) where { compare = compare1 } |]]+-- ghci| :}+-- @+--+-- We cannot automatically derive 'Eq' and 'Ord' using the standard GHC mechanism,+-- because instances require @Exp@ to be a 'Monad':+--+-- @+-- instance (Monad f, Eq b, Eq1 f, Eq a) => Eq (Scope b f a)+-- instance (Monad f, Ord b, Ord1 f, Ord a) => Ord (Scope b f a)+-- @++makeBound :: Name -> DecsQ+makeBound name = do+ TyConI dec <- reify name+ case dec of+ DataD _ _name vars _ cons _ -> makeBound' name vars cons+ _ -> fail $ show name ++ " Must be a data type."++makeBound' :: Name -> [TyVarBndrVis] -> [Con] -> DecsQ+makeBound' name vars cons = do+ let instanceHead :: Type+ instanceHead = name `conAppsT` map VarT (typeVars (init vars))++ var :: ExpQ+ var = ConE `fmap` getPure name vars cons++ bind :: ExpQ+ bind = constructBind name vars cons++ [d| instance Applicative $(pure instanceHead) where+ pure = $var+ {-# INLINE pure #-}++ ff <*> fy = do+ f <- ff+ y <- fy+ pure (f y)+ {-# INLINE (<*>) #-}++ instance Monad $(pure instanceHead) where+ (>>=) = $bind+ {-# INLINE (>>=) #-}+ |]++-- Internals+data Prop+ = Bound+ | Konst+ | Funktor Int -- ^ number tells how many layers are there+ | Exp+ deriving Show++data Components+ = Component Name [(Name, Prop)]+ | Variable Name+ deriving Show++constructBind :: Name -> [TyVarBndrVis] -> [Con] -> ExpQ+constructBind name vars cons = do+ interpret =<< construct name vars cons++construct :: Name -> [TyVarBndrVis] -> [Con] -> Q [Components]+construct name vars constructors = do+ var <- getPure name vars constructors+ for constructors $ \con -> do+ case con of+ NormalC conName [(_, _)]+ | conName == var+ -> pure (Variable conName)+ NormalC conName types+ -> Component conName `fmap` mapM typeToBnd [ ty | (_, ty) <- types ]+ RecC conName types+ -> Component conName `fmap` mapM typeToBnd [ ty | (_, _, ty) <- types ]+ InfixC (_, a) conName (_, b)+ -> do+ bndA <- typeToBnd a+ bndB <- typeToBnd b+ pure (Component conName [bndA, bndB])+ _ -> error "Not implemented."++ where+ expa :: Type+ expa = name `conAppsT` map VarT (typeVars vars)++ typeToBnd :: Type -> Q (Name, Prop)+ typeToBnd ty = do+ boundInstance <- isBound ty+ functorApp <- isFunctorApp ty+ var <- newName "var"+ pure $ case () of+ _ | ty == expa -> (var, Exp)+ | boundInstance -> (var, Bound)+ | isKonst ty -> (var, Konst)+ | Just n <- functorApp -> (var, Funktor n)+ | otherwise -> error $ "This is bad: "+ ++ show ty+ ++ " "+ ++ show boundInstance++ -- Checks whether a type is an instance of Bound by stripping its last+ -- two type arguments:+ -- isBound (Scope () EXP a)+ -- -> isInstance ''Bound [Scope ()]+ -- -> True+ isBound :: Type -> Q Bool+ isBound ty+ -- We might fail with kind error, but we don't care+ | Just a <- stripLast2 ty = pure False `recover` isInstance ''Bound [a]+ | otherwise = return False++ isKonst :: Type -> Bool+ isKonst ConT {} = True+ isKonst (VarT n) = n /= tvName (last vars)+ isKonst (AppT a b) = isKonst a && isKonst b+ isKonst _ = False++ isFunctorApp :: Type -> Q (Maybe Int)+ isFunctorApp = runMaybeT . go+ where+ go x | x == expa = pure 0+ go (f `AppT` x) = do+ isFunctor <- lift $ isInstance ''Functor [f]+ guard isFunctor+ n <- go x+ pure $ n + 1+ go _ = mzero++interpret :: [Components] -> ExpQ+interpret bnds = do+ x <- newName "x"+ f <- newName "f"++ let+ bind :: Components -> MatchQ+ bind (Variable name) = do+ a <- newName "a"+ match+ (conP name [varP a])+ (normalB (varE f `appE` varE a))+ []++ bind (Component name bounds) = do+ exprs <- foldM bindOne (ConE name) bounds+ pure $+ Match+ (ConP name+#if MIN_VERSION_template_haskell(2,18,0)+ []+#endif+ [ VarP arg | (arg, _) <- bounds ])+ (NormalB+ exprs)+ []++ bindOne :: Exp -> (Name, Prop) -> Q Exp+ bindOne expr (name, bnd) = case bnd of+ Bound ->+ pure expr `appE` (varE '(>>>=) `appE` varE name `appE` varE f)+ Konst ->+ pure expr `appE` varE name+ Exp ->+ pure expr `appE` (varE '(>>=) `appE` varE name `appE` varE f)+ Funktor n ->+ pure expr `appE` (pure (fmapN n) `appE` (varE '(>>=) `sectionR` varE f) `appE` varE name)++ fmapN :: Int -> Exp+ fmapN n = foldr1 (\a b -> VarE '(.) `AppE` a `AppE` b) $ replicate n (VarE 'fmap)++ matches <- for bnds bind+ pure $ LamE [VarP x, VarP f] (CaseE (VarE x) matches)++stripLast2 :: Type -> Maybe Type+stripLast2 (a `AppT` b `AppT` _ `AppT` d)+ | AppT{} <- d = Nothing+ | otherwise = Just (a `AppT` b)+stripLast2 _ = Nothing++-- Returns candidate+getPure :: Name -> [TyVarBndrVis] -> [Con] -> Q Name+getPure _name tyvr cons= do+ let+ findReturn :: Type -> [(Name, [Type])] -> Name+ findReturn ty constrs =+ case [ constr | (constr, [ty']) <- constrs, ty' == ty ] of+ [] -> error "Too few candidates for a variable constructor."+ [x] -> x+ -- data Exp a = Var1 a | Var2 a | ...+ -- result in+ -- Too many candidates: Var1, Var2+ xs -> error ("Too many candidates: " ++ intercalate ", " (map pprint xs))++ -- Gets the last type variable, given 'data Exp a b c = ...'+ --+ -- lastTyVar = c+ lastTyVar :: Type+ lastTyVar = VarT (last (typeVars tyvr))++ allTypeArgs :: Con -> (Name, [Type])+ allTypeArgs con = case con of+ NormalC conName tys ->+ (conName, [ ty | (_, ty) <- tys ])+ RecC conName tys ->+ (conName, [ ty | (_, _, ty) <- tys ])+ InfixC (_, t1) conName (_, t2) ->+ (conName, [ t1, t2 ])+ ForallC _ _ conName ->+ allTypeArgs conName+ _ -> error "Not implemented"++ return (findReturn lastTyVar (allTypeArgs `fmap` cons))++-------------------------------------------------------------------------------+-- Type mangling+-------------------------------------------------------------------------------++-- | Extract type variables+typeVars :: [TyVarBndr_ flag] -> [Name]+typeVars = map tvName++-- | Apply arguments to a type constructor.+conAppsT :: Name -> [Type] -> Type+conAppsT conName = foldl AppT (ConT conName)++# if !MIN_VERSION_template_haskell(2,21,0) && !MIN_VERSION_th_abstraction(0,6,0)+type TyVarBndrVis = TyVarBndrUnit+# endif+#else+#endif
src/Bound/Term.hs view
@@ -1,62 +1,62 @@------------------------------------------------------------------------------ --- | --- Copyright : (C) 2012 Edward Kmett --- License : BSD-style (see the file LICENSE) --- --- Maintainer : Edward Kmett <ekmett@gmail.com> --- Stability : experimental --- Portability : portable --- ----------------------------------------------------------------------------- -module Bound.Term - ( substitute - , substituteVar - , isClosed - , closed - ) where - -import Data.Foldable -import Data.Traversable -import Prelude hiding (all) - --- | @'substitute' a p w@ replaces the free variable @a@ with @p@ in @w@. --- --- >>> substitute "hello" ["goodnight","Gracie"] ["hello","!!!"] --- ["goodnight","Gracie","!!!"] -substitute :: (Monad f, Eq a) => a -> f a -> f a -> f a -substitute a p w = w >>= \b -> if a == b then p else return b -{-# INLINE substitute #-} - --- | @'substituteVar' a b w@ replaces a free variable @a@ with another free variable @b@ in @w@. --- --- >>> substituteVar "Alice" "Bob" ["Alice","Bob","Charlie"] --- ["Bob","Bob","Charlie"] -substituteVar :: (Functor f, Eq a) => a -> a -> f a -> f a -substituteVar a p = fmap (\b -> if a == b then p else b) -{-# INLINE substituteVar #-} - --- | If a term has no free variables, you can freely change the type of --- free variables it is parameterized on. --- --- >>> closed [12] --- Nothing --- --- >>> closed "" --- Just [] --- --- >>> :t closed "" --- closed "" :: Maybe [b] -closed :: Traversable f => f a -> Maybe (f b) -closed = traverse (const Nothing) -{-# INLINE closed #-} - --- | A closed term has no free variables. --- --- >>> isClosed [] --- True --- --- >>> isClosed [1,2,3] --- False -isClosed :: Foldable f => f a -> Bool -isClosed = all (const False) -{-# INLINE isClosed #-} +-----------------------------------------------------------------------------+-- |+-- Copyright : (C) 2012 Edward Kmett+-- License : BSD-style (see the file LICENSE)+--+-- Maintainer : Edward Kmett <ekmett@gmail.com>+-- Stability : experimental+-- Portability : portable+--+----------------------------------------------------------------------------+module Bound.Term+ ( substitute+ , substituteVar+ , isClosed+ , closed+ ) where++import Data.Foldable+import Data.Traversable+import Prelude hiding (all)++-- | @'substitute' a p w@ replaces the free variable @a@ with @p@ in @w@.+--+-- >>> substitute "hello" ["goodnight","Gracie"] ["hello","!!!"]+-- ["goodnight","Gracie","!!!"]+substitute :: (Monad f, Eq a) => a -> f a -> f a -> f a+substitute a p w = w >>= \b -> if a == b then p else return b+{-# INLINE substitute #-}++-- | @'substituteVar' a b w@ replaces a free variable @a@ with another free variable @b@ in @w@.+--+-- >>> substituteVar "Alice" "Bob" ["Alice","Bob","Charlie"]+-- ["Bob","Bob","Charlie"]+substituteVar :: (Functor f, Eq a) => a -> a -> f a -> f a+substituteVar a p = fmap (\b -> if a == b then p else b)+{-# INLINE substituteVar #-}++-- | If a term has no free variables, you can freely change the type of+-- free variables it is parameterized on.+--+-- >>> closed [12]+-- Nothing+--+-- >>> closed ""+-- Just []+--+-- >>> :t closed ""+-- closed "" :: Maybe [b]+closed :: Traversable f => f a -> Maybe (f b)+closed = traverse (const Nothing)+{-# INLINE closed #-}++-- | A closed term has no free variables.+--+-- >>> isClosed []+-- True+--+-- >>> isClosed [1,2,3]+-- False+isClosed :: Foldable f => f a -> Bool+isClosed = all (const False)+{-# INLINE isClosed #-}
src/Bound/Var.hs view
@@ -1,221 +1,221 @@-{-# LANGUAGE CPP #-} - -#ifdef __GLASGOW_HASKELL__ -{-# LANGUAGE DeriveDataTypeable #-} -{-# LANGUAGE DeriveGeneric #-} -{-# LANGUAGE Trustworthy #-} -#endif ------------------------------------------------------------------------------ --- | --- Copyright : (C) 2012 Edward Kmett --- License : BSD-style (see the file LICENSE) --- --- Maintainer : Edward Kmett <ekmett@gmail.com> --- Stability : experimental --- Portability : portable --- ----------------------------------------------------------------------------- -module Bound.Var - ( Var(..) - , unvar - , _B - , _F - ) where - -import Control.DeepSeq -import Control.Monad (liftM, ap) -import Data.Hashable (Hashable(..)) -import Data.Hashable.Lifted (Hashable1(..), Hashable2(..)) -import Data.Bifunctor -import Data.Bifoldable -import qualified Data.Binary as Binary -import Data.Binary (Binary) -import Data.Bitraversable -import Data.Bytes.Get -import Data.Bytes.Put -import Data.Bytes.Serial -import Data.Functor.Classes -import Data.Profunctor -import qualified Data.Serialize as Serialize -import Data.Serialize (Serialize) -#ifdef __GLASGOW_HASKELL__ -import Data.Data -import GHC.Generics -#endif - ----------------------------------------------------------------------------- --- Bound and Free Variables ----------------------------------------------------------------------------- - --- | \"I am not a number, I am a /free monad/!\" --- --- A @'Var' b a@ is a variable that may either be \"bound\" ('B') or \"free\" ('F'). --- --- (It is also technically a free monad in the same near-trivial sense as --- 'Either'.) -data Var b a - = B b -- ^ this is a bound variable - | F a -- ^ this is a free variable - deriving - ( Eq - , Ord - , Show - , Read -#ifdef __GLASGOW_HASKELL__ - , Data - , Generic - , Generic1 -#endif - ) - -distinguisher :: Int -distinguisher = fromIntegral $ (maxBound :: Word) `quot` 3 - -instance Hashable2 Var where - liftHashWithSalt2 h _ s (B b) = h s b - liftHashWithSalt2 _ h s (F a) = h s a `hashWithSalt` distinguisher - {-# INLINE liftHashWithSalt2 #-} -instance Hashable b => Hashable1 (Var b) where - liftHashWithSalt = liftHashWithSalt2 hashWithSalt - {-# INLINE liftHashWithSalt #-} -instance (Hashable b, Hashable a) => Hashable (Var b a) where - hashWithSalt s (B b) = hashWithSalt s b - hashWithSalt s (F a) = hashWithSalt s a `hashWithSalt` distinguisher - {-# INLINE hashWithSalt #-} - -instance Serial2 Var where - serializeWith2 pb _ (B b) = putWord8 0 >> pb b - serializeWith2 _ pf (F f) = putWord8 1 >> pf f - {-# INLINE serializeWith2 #-} - - deserializeWith2 gb gf = getWord8 >>= \b -> case b of - 0 -> liftM B gb - 1 -> liftM F gf - _ -> fail $ "getVar: Unexpected constructor code: " ++ show b - {-# INLINE deserializeWith2 #-} - -instance Serial b => Serial1 (Var b) where - serializeWith = serializeWith2 serialize - {-# INLINE serializeWith #-} - deserializeWith = deserializeWith2 deserialize - {-# INLINE deserializeWith #-} - -instance (Serial b, Serial a) => Serial (Var b a) where - serialize = serializeWith2 serialize serialize - {-# INLINE serialize #-} - deserialize = deserializeWith2 deserialize deserialize - {-# INLINE deserialize #-} - -instance (Binary b, Binary a) => Binary (Var b a) where - put = serializeWith2 Binary.put Binary.put - get = deserializeWith2 Binary.get Binary.get - -instance (Serialize b, Serialize a) => Serialize (Var b a) where - put = serializeWith2 Serialize.put Serialize.put - get = deserializeWith2 Serialize.get Serialize.get - -unvar :: (b -> r) -> (a -> r) -> Var b a -> r -unvar f _ (B b) = f b -unvar _ g (F a) = g a -{-# INLINE unvar #-} - --- | --- This provides a @Prism@ that can be used with @lens@ library to access a bound 'Var'. --- --- @ --- '_B' :: 'Prism' (Var b a) (Var b' a) b b'@ --- @ -_B :: (Choice p, Applicative f) => p b (f b') -> p (Var b a) (f (Var b' a)) -_B = dimap (unvar Right (Left . F)) (either pure (fmap B)) . right' -{-# INLINE _B #-} - --- | --- This provides a @Prism@ that can be used with @lens@ library to access a free 'Var'. --- --- @ --- '_F' :: 'Prism' (Var b a) (Var b a') a a'@ --- @ -_F :: (Choice p, Applicative f) => p a (f a') -> p (Var b a) (f (Var b a')) -_F = dimap (unvar (Left . B) Right) (either pure (fmap F)) . right' -{-# INLINE _F #-} - ----------------------------------------------------------------------------- --- Instances ----------------------------------------------------------------------------- - -instance Functor (Var b) where - fmap _ (B b) = B b - fmap f (F a) = F (f a) - {-# INLINE fmap #-} - -instance Foldable (Var b) where - foldMap f (F a) = f a - foldMap _ _ = mempty - {-# INLINE foldMap #-} - -instance Traversable (Var b) where - traverse f (F a) = F <$> f a - traverse _ (B b) = pure (B b) - {-# INLINE traverse #-} - -instance Applicative (Var b) where - pure = F - {-# INLINE pure #-} - (<*>) = ap - {-# INLINE (<*>) #-} - -instance Monad (Var b) where - return = pure - {-# INLINE return #-} - F a >>= f = f a - B b >>= _ = B b - {-# INLINE (>>=) #-} - -instance Bifunctor Var where - bimap f _ (B b) = B (f b) - bimap _ g (F a) = F (g a) - {-# INLINE bimap #-} - -instance Bifoldable Var where - bifoldMap f _ (B b) = f b - bifoldMap _ g (F a) = g a - {-# INLINE bifoldMap #-} - -instance Bitraversable Var where - bitraverse f _ (B b) = B <$> f b - bitraverse _ g (F a) = F <$> g a - {-# INLINE bitraverse #-} - -instance Eq2 Var where - liftEq2 f _ (B a) (B c) = f a c - liftEq2 _ g (F b) (F d) = g b d - liftEq2 _ _ _ _ = False - -instance Ord2 Var where - liftCompare2 f _ (B a) (B c) = f a c - liftCompare2 _ _ B{} F{} = LT - liftCompare2 _ _ F{} B{} = GT - liftCompare2 _ g (F b) (F d) = g b d - -instance Show2 Var where - liftShowsPrec2 f _ _ _ d (B a) = showsUnaryWith f "B" d a - liftShowsPrec2 _ _ h _ d (F a) = showsUnaryWith h "F" d a - -instance Read2 Var where - liftReadsPrec2 f _ h _ = readsData $ readsUnaryWith f "B" B `mappend` readsUnaryWith h "F" F - -instance Eq b => Eq1 (Var b) where - liftEq = liftEq2 (==) - -instance Ord b => Ord1 (Var b) where - liftCompare = liftCompare2 compare - -instance Show b => Show1 (Var b) where - liftShowsPrec = liftShowsPrec2 showsPrec showList - -instance Read b => Read1 (Var b) where - liftReadsPrec = liftReadsPrec2 readsPrec readList - -instance (NFData a, NFData b) => NFData (Var b a) where - rnf (B b) = rnf b - rnf (F f) = rnf f +{-# LANGUAGE CPP #-}++#ifdef __GLASGOW_HASKELL__+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE Trustworthy #-}+#endif+-----------------------------------------------------------------------------+-- |+-- Copyright : (C) 2012 Edward Kmett+-- License : BSD-style (see the file LICENSE)+--+-- Maintainer : Edward Kmett <ekmett@gmail.com>+-- Stability : experimental+-- Portability : portable+--+----------------------------------------------------------------------------+module Bound.Var+ ( Var(..)+ , unvar+ , _B+ , _F+ ) where++import Control.DeepSeq+import Control.Monad (liftM, ap)+import Data.Hashable (Hashable(..))+import Data.Hashable.Lifted (Hashable1(..), Hashable2(..))+import Data.Bifunctor+import Data.Bifoldable+import qualified Data.Binary as Binary+import Data.Binary (Binary)+import Data.Bitraversable+import Data.Bytes.Get+import Data.Bytes.Put+import Data.Bytes.Serial+import Data.Functor.Classes+import Data.Profunctor+import qualified Data.Serialize as Serialize+import Data.Serialize (Serialize)+#ifdef __GLASGOW_HASKELL__+import Data.Data+import GHC.Generics+#endif++----------------------------------------------------------------------------+-- Bound and Free Variables+----------------------------------------------------------------------------++-- | \"I am not a number, I am a /free monad/!\"+--+-- A @'Var' b a@ is a variable that may either be \"bound\" ('B') or \"free\" ('F').+--+-- (It is also technically a free monad in the same near-trivial sense as+-- 'Either'.)+data Var b a+ = B b -- ^ this is a bound variable+ | F a -- ^ this is a free variable+ deriving+ ( Eq+ , Ord+ , Show+ , Read+#ifdef __GLASGOW_HASKELL__+ , Data+ , Generic+ , Generic1+#endif+ )++distinguisher :: Int+distinguisher = fromIntegral $ (maxBound :: Word) `quot` 3++instance Hashable2 Var where+ liftHashWithSalt2 h _ s (B b) = h s b+ liftHashWithSalt2 _ h s (F a) = h s a `hashWithSalt` distinguisher+ {-# INLINE liftHashWithSalt2 #-}+instance Hashable b => Hashable1 (Var b) where+ liftHashWithSalt = liftHashWithSalt2 hashWithSalt+ {-# INLINE liftHashWithSalt #-}+instance (Hashable b, Hashable a) => Hashable (Var b a) where+ hashWithSalt s (B b) = hashWithSalt s b+ hashWithSalt s (F a) = hashWithSalt s a `hashWithSalt` distinguisher+ {-# INLINE hashWithSalt #-}++instance Serial2 Var where+ serializeWith2 pb _ (B b) = putWord8 0 >> pb b+ serializeWith2 _ pf (F f) = putWord8 1 >> pf f+ {-# INLINE serializeWith2 #-}++ deserializeWith2 gb gf = getWord8 >>= \b -> case b of+ 0 -> liftM B gb+ 1 -> liftM F gf+ _ -> fail $ "getVar: Unexpected constructor code: " ++ show b+ {-# INLINE deserializeWith2 #-}++instance Serial b => Serial1 (Var b) where+ serializeWith = serializeWith2 serialize+ {-# INLINE serializeWith #-}+ deserializeWith = deserializeWith2 deserialize+ {-# INLINE deserializeWith #-}++instance (Serial b, Serial a) => Serial (Var b a) where+ serialize = serializeWith2 serialize serialize+ {-# INLINE serialize #-}+ deserialize = deserializeWith2 deserialize deserialize+ {-# INLINE deserialize #-}++instance (Binary b, Binary a) => Binary (Var b a) where+ put = serializeWith2 Binary.put Binary.put+ get = deserializeWith2 Binary.get Binary.get++instance (Serialize b, Serialize a) => Serialize (Var b a) where+ put = serializeWith2 Serialize.put Serialize.put+ get = deserializeWith2 Serialize.get Serialize.get++unvar :: (b -> r) -> (a -> r) -> Var b a -> r+unvar f _ (B b) = f b+unvar _ g (F a) = g a+{-# INLINE unvar #-}++-- |+-- This provides a @Prism@ that can be used with @lens@ library to access a bound 'Var'.+--+-- @+-- '_B' :: 'Prism' (Var b a) (Var b' a) b b'@+-- @+_B :: (Choice p, Applicative f) => p b (f b') -> p (Var b a) (f (Var b' a))+_B = dimap (unvar Right (Left . F)) (either pure (fmap B)) . right'+{-# INLINE _B #-}++-- |+-- This provides a @Prism@ that can be used with @lens@ library to access a free 'Var'.+--+-- @+-- '_F' :: 'Prism' (Var b a) (Var b a') a a'@+-- @+_F :: (Choice p, Applicative f) => p a (f a') -> p (Var b a) (f (Var b a'))+_F = dimap (unvar (Left . B) Right) (either pure (fmap F)) . right'+{-# INLINE _F #-}++----------------------------------------------------------------------------+-- Instances+----------------------------------------------------------------------------++instance Functor (Var b) where+ fmap _ (B b) = B b+ fmap f (F a) = F (f a)+ {-# INLINE fmap #-}++instance Foldable (Var b) where+ foldMap f (F a) = f a+ foldMap _ _ = mempty+ {-# INLINE foldMap #-}++instance Traversable (Var b) where+ traverse f (F a) = F <$> f a+ traverse _ (B b) = pure (B b)+ {-# INLINE traverse #-}++instance Applicative (Var b) where+ pure = F+ {-# INLINE pure #-}+ (<*>) = ap+ {-# INLINE (<*>) #-}++instance Monad (Var b) where+ return = pure+ {-# INLINE return #-}+ F a >>= f = f a+ B b >>= _ = B b+ {-# INLINE (>>=) #-}++instance Bifunctor Var where+ bimap f _ (B b) = B (f b)+ bimap _ g (F a) = F (g a)+ {-# INLINE bimap #-}++instance Bifoldable Var where+ bifoldMap f _ (B b) = f b+ bifoldMap _ g (F a) = g a+ {-# INLINE bifoldMap #-}++instance Bitraversable Var where+ bitraverse f _ (B b) = B <$> f b+ bitraverse _ g (F a) = F <$> g a+ {-# INLINE bitraverse #-}++instance Eq2 Var where+ liftEq2 f _ (B a) (B c) = f a c+ liftEq2 _ g (F b) (F d) = g b d+ liftEq2 _ _ _ _ = False++instance Ord2 Var where+ liftCompare2 f _ (B a) (B c) = f a c+ liftCompare2 _ _ B{} F{} = LT+ liftCompare2 _ _ F{} B{} = GT+ liftCompare2 _ g (F b) (F d) = g b d++instance Show2 Var where+ liftShowsPrec2 f _ _ _ d (B a) = showsUnaryWith f "B" d a+ liftShowsPrec2 _ _ h _ d (F a) = showsUnaryWith h "F" d a++instance Read2 Var where+ liftReadsPrec2 f _ h _ = readsData $ readsUnaryWith f "B" B `mappend` readsUnaryWith h "F" F++instance Eq b => Eq1 (Var b) where+ liftEq = liftEq2 (==)++instance Ord b => Ord1 (Var b) where+ liftCompare = liftCompare2 compare++instance Show b => Show1 (Var b) where+ liftShowsPrec = liftShowsPrec2 showsPrec showList++instance Read b => Read1 (Var b) where+ liftReadsPrec = liftReadsPrec2 readsPrec readList++instance (NFData a, NFData b) => NFData (Var b a) where+ rnf (B b) = rnf b+ rnf (F f) = rnf f