bound 2.0.5 → 2.0.6
raw patch · 23 files changed
+3618/−3604 lines, 23 filesdep ~th-abstractionsetup-changedPVP ok
version bump matches the API change (PVP)
Dependency ranges changed: th-abstraction
API changes (from Hackage documentation)
Files
- .gitignore +32/−32
- .vim.custom +31/−31
- AUTHORS.markdown +10/−10
- CHANGELOG.markdown +126/−122
- LICENSE +30/−30
- README.markdown +71/−71
- Setup.lhs +7/−7
- bound.cabal +156/−156
- doc/BoundLaws.hs +102/−102
- doc/LICENSE +30/−30
- doc/bound-laws.cabal +38/−38
- examples/Deriving.hs +131/−131
- examples/Imperative.hs +286/−286
- examples/Overkill.hs +344/−344
- examples/Simple.hs +183/−181
- src/Bound.hs +146/−143
- 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 +341/−336
- 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,122 +1,126 @@-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.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,156 @@-name: bound-category: Language, Compilers/Interpreters-version: 2.0.5-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.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
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,38 @@-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.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
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,181 +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)--deriveEq1 ''Exp-deriveOrd1 ''Exp-deriveRead1 ''Exp-deriveShow1 ''Exp--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,143 +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)--- @------ @--- deriveEq1 ''Exp--- deriveOrd1 ''Exp--- deriveRead1 ''Exp--- deriveShow1 ''Exp------ 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,336 +1,341 @@-{-# 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.------ @deriving-compat@ package may be used to derive the 'Show1' and 'Read1' instances------ @--- {-\# 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--- deriveShow1 ''Exp--- deriveRead1 ''Exp--- 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| deriveShow1 ''Exp--- ghci| deriveRead1 ''Exp--- ghci| instance Read a => Read (Exp a) where readsPrec = readsPrec1--- ghci| instance Show a => Show (Exp a) where showsPrec = showsPrec1--- ghci| :}--- @------ 'Eq' and 'Ord' instances can be derived similarly------ @--- import Data.Functor.Classes (Eq1, Ord1, eq1, compare1)--- import Data.Deriving (deriveEq1, deriveOrd1)------ deriveEq1 ''Exp--- deriveOrd1 ''Exp--- 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| deriveEq1 ''Exp--- ghci| deriveOrd1 ''Exp--- ghci| instance Eq a => Eq (Exp a) where (==) = eq1--- ghci| 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 -> [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
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