diff --git a/.gitignore b/.gitignore --- a/.gitignore +++ b/.gitignore @@ -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.* diff --git a/.vim.custom b/.vim.custom --- a/.vim.custom +++ b/.vim.custom @@ -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 :exec ":!hasktags -x -c --ignore src" - -" 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 :exec ":!hasktags -x -c --ignore src" + +" 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" diff --git a/AUTHORS.markdown b/AUTHORS.markdown --- a/AUTHORS.markdown +++ b/AUTHORS.markdown @@ -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'. diff --git a/CHANGELOG.markdown b/CHANGELOG.markdown --- a/CHANGELOG.markdown +++ b/CHANGELOG.markdown @@ -1,126 +1,130 @@ -2.0.6 [2023.01.18] ------------------- -* Allow the examples to build with `base-4.18.*` (GHC 9.6). - -2.0.5 [2022.05.07] ------------------- -* Allow building with `transformers-0.6.*`. - -2.0.4 [2021.11.07] ------------------- -* Allow building with `template-haskell-2.18` (GHC 9.2). -* The `Bound.TH` module no longer requires the `TemplateHaskell` extension - (only `TemplateHaskellQuotes`) when building with GHC 9.0 or later. -* Drop support for pre-8.0 versions of GHC. - -2.0.3 [2021.02.05] ------------------- -* Allow the examples to build with `vector-0.12.2` or later. -* The build-type has been changed from `Custom` to `Simple`. - To achieve this, the `doctests` test suite has been removed in favor of using [`cabal-docspec`](https://github.com/phadej/cabal-extras/tree/master/cabal-docspec) to run the doctests. - -2.0.2 [2020.10.01] ------------------- -* Allow building with GHC 9.0. - -2.0.1 ------ -* Add `abstractEither` and `instantiateEither` to `Bound.Scope`, and - add `abstractEitherName` and `instantiateEitherName` to `Bound.Scope.Name` -* Add `Generic(1)` instances for `Name` and `Scope` -* Support `doctest-0.12` - -2 -- -* GHC 8.0 and 8.2 support -* Converted from `prelude-extras` to `transformers` + `transformers-compat` for the `Eq1`, `Ord1`, `Show1`, and `Read1` functionality. -* `makeBound` supports `Functor` components -* Add `MFunctor` instance for `Scope` -* Add `NFData` instances for `Name`, `Scope`, and `Var` -* Revamp `Setup.hs` to use `cabal-doctest`. This makes it build - with `Cabal-1.25`, and makes the `doctest`s work with `cabal new-build` and - sandboxes. - -1.0.7 ------- -* Added an `-f-template-haskell` option to allow disabling `template-haskell` support. This is an unsupported configuration but may be useful for expert users in sandbox configurations. -* Support `cereal` 0.5 - -1.0.6 ------ -* Compiles warning-free on GHC 7.10 - -1.0.5 ------ -* Widened version bound on `bifunctors`. -* Widened version bound on `profunctors`. - -1.0.4 ------ -* Widened version bound on `transformers`. - -1.0.3 ------ -* Added `bitransverseScope`. - -1.0.2 ------ -* Removed unneccesary constraint on `hoistScope`. - -1.0.1 ------ -* Added a monomorphic `hoistScope` for `Bound.Scope.Simple` - -1.0 ---- -* Added instances for `Bound` for all of the `mtl` monads. -* Added `Data` and `Typeable` support to both versions of `Scope` -* Added the missing `Applictive` instance to `Bound.Scope.Simple` -* Moved `hoistScope`, `bitraverseScope`, `transverseScope`, and `instantiateVars` here from the `ermine` compiler. - -0.9.1.1 -------- -* Updated to work with `bifunctors` 4.0 - -0.9.1 ------ -* Updated to work with `comonad` 4.0 and `profunctors` 4.0 - -0.9 ---- -* Added the missing instance for `Applicative (Scope b f)` - -0.8.1 ------ -* SafeHaskell support - -0.8 ---- -* Added `Serial`, `Binary` and `Serialize` instances for `Scope`. - -0.7 ---- -* Added `Hashable`, `Hashable1` and `Hashable2` instances where appropriate for `Name`, `Var` and `Scope`. - -0.6.1 ------ -* More aggressive inlining -* Added `unvar`, `_B`, `_F` to `Bound.Var`. -* Added `_Name` to `Bound.Name`. - -0.6 ---- -* Support for `prelude-extras` 0.3 - -0.5.1 ------ -* Removed my personal inter-package dependency upper bounds -* Updated doctest suite to use exact versions. - -0.5 ---- -* Created a `doctest`-based test suite -* Added many examples -* 100% haddock coverage -* Added the `Name` `Comonad`, to help retain names for bound variables. -* Bumped dependencies +2.0.7 [2023.08.06] +------------------ +* Support building with `template-haskell-2.21.*` (GHC 9.8). + +2.0.6 [2023.01.18] +------------------ +* Allow the examples to build with `base-4.18.*` (GHC 9.6). + +2.0.5 [2022.05.07] +------------------ +* Allow building with `transformers-0.6.*`. + +2.0.4 [2021.11.07] +------------------ +* Allow building with `template-haskell-2.18` (GHC 9.2). +* The `Bound.TH` module no longer requires the `TemplateHaskell` extension + (only `TemplateHaskellQuotes`) when building with GHC 9.0 or later. +* Drop support for pre-8.0 versions of GHC. + +2.0.3 [2021.02.05] +------------------ +* Allow the examples to build with `vector-0.12.2` or later. +* The build-type has been changed from `Custom` to `Simple`. + To achieve this, the `doctests` test suite has been removed in favor of using [`cabal-docspec`](https://github.com/phadej/cabal-extras/tree/master/cabal-docspec) to run the doctests. + +2.0.2 [2020.10.01] +------------------ +* Allow building with GHC 9.0. + +2.0.1 +----- +* Add `abstractEither` and `instantiateEither` to `Bound.Scope`, and + add `abstractEitherName` and `instantiateEitherName` to `Bound.Scope.Name` +* Add `Generic(1)` instances for `Name` and `Scope` +* Support `doctest-0.12` + +2 +- +* GHC 8.0 and 8.2 support +* Converted from `prelude-extras` to `transformers` + `transformers-compat` for the `Eq1`, `Ord1`, `Show1`, and `Read1` functionality. +* `makeBound` supports `Functor` components +* Add `MFunctor` instance for `Scope` +* Add `NFData` instances for `Name`, `Scope`, and `Var` +* Revamp `Setup.hs` to use `cabal-doctest`. This makes it build + with `Cabal-1.25`, and makes the `doctest`s work with `cabal new-build` and + sandboxes. + +1.0.7 +------ +* Added an `-f-template-haskell` option to allow disabling `template-haskell` support. This is an unsupported configuration but may be useful for expert users in sandbox configurations. +* Support `cereal` 0.5 + +1.0.6 +----- +* Compiles warning-free on GHC 7.10 + +1.0.5 +----- +* Widened version bound on `bifunctors`. +* Widened version bound on `profunctors`. + +1.0.4 +----- +* Widened version bound on `transformers`. + +1.0.3 +----- +* Added `bitransverseScope`. + +1.0.2 +----- +* Removed unneccesary constraint on `hoistScope`. + +1.0.1 +----- +* Added a monomorphic `hoistScope` for `Bound.Scope.Simple` + +1.0 +--- +* Added instances for `Bound` for all of the `mtl` monads. +* Added `Data` and `Typeable` support to both versions of `Scope` +* Added the missing `Applictive` instance to `Bound.Scope.Simple` +* Moved `hoistScope`, `bitraverseScope`, `transverseScope`, and `instantiateVars` here from the `ermine` compiler. + +0.9.1.1 +------- +* Updated to work with `bifunctors` 4.0 + +0.9.1 +----- +* Updated to work with `comonad` 4.0 and `profunctors` 4.0 + +0.9 +--- +* Added the missing instance for `Applicative (Scope b f)` + +0.8.1 +----- +* SafeHaskell support + +0.8 +--- +* Added `Serial`, `Binary` and `Serialize` instances for `Scope`. + +0.7 +--- +* Added `Hashable`, `Hashable1` and `Hashable2` instances where appropriate for `Name`, `Var` and `Scope`. + +0.6.1 +----- +* More aggressive inlining +* Added `unvar`, `_B`, `_F` to `Bound.Var`. +* Added `_Name` to `Bound.Name`. + +0.6 +--- +* Support for `prelude-extras` 0.3 + +0.5.1 +----- +* Removed my personal inter-package dependency upper bounds +* Updated doctest suite to use exact versions. + +0.5 +--- +* Created a `doctest`-based test suite +* Added many examples +* 100% haddock coverage +* Added the `Name` `Comonad`, to help retain names for bound variables. +* Bumped dependencies diff --git a/LICENSE b/LICENSE --- a/LICENSE +++ b/LICENSE @@ -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. diff --git a/README.markdown b/README.markdown --- a/README.markdown +++ b/README.markdown @@ -1,71 +1,71 @@ -Bound -===== - -[![Hackage](https://img.shields.io/hackage/v/bound.svg)](https://hackage.haskell.org/package/bound) [![Build Status](https://github.com/ekmett/bound/workflows/Haskell-CI/badge.svg)](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 +===== + +[![Hackage](https://img.shields.io/hackage/v/bound.svg)](https://hackage.haskell.org/package/bound) [![Build Status](https://github.com/ekmett/bound/workflows/Haskell-CI/badge.svg)](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 + diff --git a/Setup.lhs b/Setup.lhs --- a/Setup.lhs +++ b/Setup.lhs @@ -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 diff --git a/bound.cabal b/bound.cabal --- a/bound.cabal +++ b/bound.cabal @@ -1,156 +1,158 @@ -name: bound -category: Language, Compilers/Interpreters -version: 2.0.6 -license: BSD3 -cabal-version: >= 1.10 -license-file: LICENSE -author: Edward A. Kmett -maintainer: Edward A. Kmett -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: - . - - . - The goal of this package is to make it as easy as possible to deal with name - binding without forcing an awkward monadic style on the user. - . - With generalized de Bruijn term you can 'lift' whole trees instead of just - applying 'succ' to individual variables, weakening the all variables bound - by a scope and greatly speeding up instantiation. By giving binders more - structure we permit easy simultaneous substitution and further speed up - instantiation. - -extra-source-files: - .gitignore - .vim.custom - doc/*.hs - doc/bound-laws.cabal - doc/LICENSE - README.markdown - CHANGELOG.markdown - AUTHORS.markdown - -tested-with: - GHC==8.0.2, - GHC==8.2.2, - GHC==8.4.4, - GHC==8.6.5, - GHC==8.8.4, - GHC==8.10.7, - GHC==9.0.1, - GHC==9.2.1 - -flag template-haskell - description: - You can disable the use of the `template-haskell` package using `-f-template-haskell`. - . - Disabling this is an unsupported configuration, but it may be useful for accelerating builds in sandboxes for expert users. - default: True - manual: True - -source-repository head - type: git - location: git://github.com/ekmett/bound.git - -library - hs-source-dirs: src - - exposed-modules: - Bound - Bound.Class - Bound.Name - Bound.Scope - Bound.Scope.Simple - Bound.Term - Bound.TH - Bound.Var - - build-depends: - base >= 4.9 && < 5, - bifunctors >= 5 && < 6, - binary >= 0.8.3 && < 0.9, - bytes >= 0.15.2 && < 1, - cereal >= 0.4.1 && < 0.6, - comonad >= 5 && < 6, - hashable >= 1.2.5.0 && < 1.5, - mmorph >= 1.0 && < 1.3, - deepseq >= 1.4.2 && < 1.5, - profunctors >= 3.3 && < 6, - th-abstraction >= 0.4 && < 0.5, - transformers >= 0.5 && < 0.7, - transformers-compat >= 0.5 && < 1 - - ghc-options: -Wall -O2 -fspec-constr -fdicts-cheap -funbox-strict-fields - - default-language: Haskell2010 - - if flag(template-haskell) && impl(ghc) - build-depends: template-haskell >= 2.11.1 && < 3.0 - -test-suite Simple - type: exitcode-stdio-1.0 - main-is: Simple.hs - hs-source-dirs: examples - buildable: True - - ghc-options: -Wall -threaded - default-language: Haskell2010 - build-depends: - base >= 4.5 && < 5, - bound, - deriving-compat >= 0.3.4 && < 0.7, - transformers, - transformers-compat - -test-suite Overkill - type: exitcode-stdio-1.0 - main-is: Overkill.hs - hs-source-dirs: examples - ghc-options: -Wall -threaded - default-language: Haskell2010 - build-depends: - base >= 4.5 && < 5, - bound, - transformers, - transformers-compat, - vector >= 0.12 - if !impl(ghc >= 7.8) - buildable: False - -test-suite Deriving - type: exitcode-stdio-1.0 - main-is: Deriving.hs - hs-source-dirs: examples - ghc-options: -Wall -threaded - default-language: Haskell2010 - build-depends: - base >= 4.5 && < 5, - bound, - transformers, - transformers-compat - -test-suite Imperative - type: exitcode-stdio-1.0 - main-is: Imperative.hs - hs-source-dirs: examples - ghc-options: -Wall -threaded - default-language: Haskell2010 - build-depends: - base >= 4.5 && < 5, - bound, - transformers, - transformers-compat, - void +name: bound +category: Language, Compilers/Interpreters +version: 2.0.7 +license: BSD3 +cabal-version: >= 1.10 +license-file: LICENSE +author: Edward A. Kmett +maintainer: Edward A. Kmett +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: + . + + . + The goal of this package is to make it as easy as possible to deal with name + binding without forcing an awkward monadic style on the user. + . + With generalized de Bruijn term you can 'lift' whole trees instead of just + applying 'succ' to individual variables, weakening the all variables bound + by a scope and greatly speeding up instantiation. By giving binders more + structure we permit easy simultaneous substitution and further speed up + instantiation. + +extra-source-files: + .gitignore + .vim.custom + doc/*.hs + doc/bound-laws.cabal + doc/LICENSE + README.markdown + CHANGELOG.markdown + AUTHORS.markdown + +tested-with: + GHC==8.0.2, + GHC==8.2.2, + GHC==8.4.4, + GHC==8.6.5, + GHC==8.8.4, + GHC==8.10.7, + GHC==9.0.2, + GHC==9.2.8, + GHC==9.4.5, + GHC==9.6.2 + +flag template-haskell + description: + You can disable the use of the `template-haskell` package using `-f-template-haskell`. + . + Disabling this is an unsupported configuration, but it may be useful for accelerating builds in sandboxes for expert users. + default: True + manual: True + +source-repository head + type: git + location: git://github.com/ekmett/bound.git + +library + hs-source-dirs: src + + exposed-modules: + Bound + Bound.Class + Bound.Name + Bound.Scope + Bound.Scope.Simple + Bound.Term + Bound.TH + Bound.Var + + build-depends: + base >= 4.9 && < 5, + bifunctors >= 5 && < 6, + binary >= 0.8.3 && < 0.9, + bytes >= 0.15.2 && < 1, + cereal >= 0.4.1 && < 0.6, + comonad >= 5 && < 6, + hashable >= 1.2.5.0 && < 1.5, + mmorph >= 1.0 && < 1.3, + deepseq >= 1.4.2 && < 1.6, + profunctors >= 3.3 && < 6, + th-abstraction >= 0.4 && < 0.7, + transformers >= 0.5 && < 0.7, + transformers-compat >= 0.5 && < 1 + + ghc-options: -Wall -O2 -fspec-constr -fdicts-cheap -funbox-strict-fields + + default-language: Haskell2010 + + if flag(template-haskell) && impl(ghc) + build-depends: template-haskell >= 2.11.1 && < 3.0 + +test-suite Simple + type: exitcode-stdio-1.0 + main-is: Simple.hs + hs-source-dirs: examples + buildable: True + + ghc-options: -Wall -threaded + default-language: Haskell2010 + build-depends: + base >= 4.5 && < 5, + bound, + deriving-compat >= 0.3.4 && < 0.7, + transformers, + transformers-compat + +test-suite Overkill + type: exitcode-stdio-1.0 + main-is: Overkill.hs + hs-source-dirs: examples + ghc-options: -Wall -threaded + default-language: Haskell2010 + build-depends: + base >= 4.5 && < 5, + bound, + transformers, + transformers-compat, + vector >= 0.12 + if !impl(ghc >= 7.8) + buildable: False + +test-suite Deriving + type: exitcode-stdio-1.0 + main-is: Deriving.hs + hs-source-dirs: examples + ghc-options: -Wall -threaded + default-language: Haskell2010 + build-depends: + base >= 4.5 && < 5, + bound, + transformers, + transformers-compat + +test-suite Imperative + type: exitcode-stdio-1.0 + main-is: Imperative.hs + hs-source-dirs: examples + ghc-options: -Wall -threaded + default-language: Haskell2010 + build-depends: + base >= 4.5 && < 5, + bound, + transformers, + transformers-compat, + void diff --git a/doc/BoundLaws.hs b/doc/BoundLaws.hs --- a/doc/BoundLaws.hs +++ b/doc/BoundLaws.hs @@ -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 +-} diff --git a/doc/LICENSE b/doc/LICENSE --- a/doc/LICENSE +++ b/doc/LICENSE @@ -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. diff --git a/doc/bound-laws.cabal b/doc/bound-laws.cabal --- a/doc/bound-laws.cabal +++ b/doc/bound-laws.cabal @@ -1,38 +1,40 @@ -name: bound-laws -category: Language, Compilers/Interpreters -version: 0.1 -license: BSD3 -cabal-version: >= 1.10 -license-file: LICENSE -author: Edward A. Kmett -maintainer: Edward A. Kmett -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 +stability: experimental +homepage: http://github.com/ekmett/bound/ +bug-reports: http://github.com/ekmett/bound/issues +copyright: Copyright (C) 2012-2013 Edward A. Kmett +synopsis: Making de Bruijn Succ Less +build-type: Simple +description: Some laws for the @Bound@ class + +tested-with: + GHC==8.0.2, + GHC==8.2.2, + GHC==8.4.4, + GHC==8.6.5, + GHC==8.8.4, + GHC==8.10.7, + GHC==9.0.2, + GHC==9.2.8, + GHC==9.4.5, + GHC==9.6.2 + +source-repository head + type: git + location: git://github.com/ekmett/bound.git + +library + exposed-modules: BoundLaws + hs-source-dirs: . + ghc-options: -Wall + default-language: Haskell2010 + build-depends: + base >= 4.9 && < 5, + bound diff --git a/examples/Deriving.hs b/examples/Deriving.hs --- a/examples/Deriving.hs +++ b/examples/Deriving.hs @@ -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 () diff --git a/examples/Imperative.hs b/examples/Imperative.hs --- a/examples/Imperative.hs +++ b/examples/Imperative.hs @@ -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 () diff --git a/examples/Overkill.hs b/examples/Overkill.hs --- a/examples/Overkill.hs +++ b/examples/Overkill.hs @@ -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 () diff --git a/examples/Simple.hs b/examples/Simple.hs --- a/examples/Simple.hs +++ b/examples/Simple.hs @@ -1,183 +1,183 @@ -{-# LANGUAGE CPP, TemplateHaskell #-} -module Main where - --- this is a simple example where lambdas only bind a single variable at a time --- this directly corresponds to the usual de bruijn presentation - -import Data.List (elemIndex) -import Data.Foldable hiding (notElem) -import Data.Maybe (fromJust) -import Data.Traversable -import Control.Monad -import Control.Applicative -import Prelude hiding (foldr,abs) -import Data.Deriving (deriveEq1, deriveOrd1, deriveRead1, deriveShow1) -import Data.Functor.Classes -import Bound -import System.Exit - - -infixl 9 :@ - -data Exp a - = V a - | Exp a :@ Exp a - | Lam (Scope () Exp a) - | Let [Scope Int Exp a] (Scope Int Exp a) - --- | A smart constructor for Lam --- --- >>> lam "y" (lam "x" (V "x" :@ V "y")) --- Lam (Scope (Lam (Scope (V (B ()) :@ V (F (V (B ()))))))) -lam :: Eq a => a -> Exp a -> Exp a -lam v b = Lam (abstract1 v b) - --- | A smart constructor for Let bindings - -let_ :: Eq a => [(a,Exp a)] -> Exp a -> Exp a -let_ [] b = b -let_ bs b = Let (map (abstr . snd) bs) (abstr b) - where abstr = abstract (`elemIndex` map fst bs) - -instance Functor Exp where fmap = fmapDefault -instance Foldable Exp where foldMap = foldMapDefault - -instance Applicative Exp where - pure = V - (<*>) = ap - -instance Traversable Exp where - traverse f (V a) = V <$> f a - traverse f (x :@ y) = (:@) <$> traverse f x <*> traverse f y - traverse f (Lam e) = Lam <$> traverse f e - traverse f (Let bs b) = Let <$> traverse (traverse f) bs <*> traverse f b - -instance Monad Exp where -#if !(MIN_VERSION_base(4,11,0)) - return = V -#endif - V a >>= f = f a - (x :@ y) >>= f = (x >>= f) :@ (y >>= f) - Lam e >>= f = Lam (e >>>= f) - Let bs b >>= f = Let (map (>>>= f) bs) (b >>>= f) - -fmap concat $ sequence - [ deriveEq1 ''Exp - , deriveOrd1 ''Exp - , deriveRead1 ''Exp - , deriveShow1 ''Exp - , [d| instance Eq a => Eq (Exp a) where (==) = eq1 - instance Ord a => Ord (Exp a) where compare = compare1 - instance Show a => Show (Exp a) where showsPrec = showsPrec1 - instance Read a => Read (Exp a) where readsPrec = readsPrec1 - |] - ] - --- | Compute the normal form of an expression -nf :: Exp a -> Exp a -nf e@V{} = e -nf (Lam b) = Lam $ toScope $ nf $ fromScope b -nf (f :@ a) = case whnf f of - Lam b -> nf (instantiate1 a b) - f' -> nf f' :@ nf a -nf (Let bs b) = nf (inst b) - where es = map inst bs - inst = instantiate (es !!) - --- | Reduce a term to weak head normal form -whnf :: Exp a -> Exp a -whnf e@V{} = e -whnf e@Lam{} = e -whnf (f :@ a) = case whnf f of - Lam b -> whnf (instantiate1 a b) - f' -> f' :@ a -whnf (Let bs b) = whnf (inst b) - where es = map inst bs - inst = instantiate (es !!) - -infixr 0 ! -(!) :: Eq a => a -> Exp a -> Exp a -(!) = lam - --- | Lennart Augustsson's example from "The Lambda Calculus Cooked 4 Ways" --- --- Modified to use recursive let, because we can. --- --- >>> nf cooked == true --- True - -true :: Exp String -true = lam "F" $ lam "T" $ V"T" - -cooked :: Exp a -cooked = fromJust $ closed $ let_ - [ ("False", "f" ! "t" ! V"f") - , ("True", "f" ! "t" ! V"t") - , ("if", "b" ! "t" ! "f" ! V"b" :@ V"f" :@ V"t") - , ("Zero", "z" ! "s" ! V"z") - , ("Succ", "n" ! "z" ! "s" ! V"s" :@ V"n") - , ("one", V"Succ" :@ V"Zero") - , ("two", V"Succ" :@ V"one") - , ("three", V"Succ" :@ V"two") - , ("isZero", "n" ! V"n" :@ V"True" :@ ("m" ! V"False")) - , ("const", "x" ! "y" ! V"x") - , ("Pair", "a" ! "b" ! "p" ! V"p" :@ V"a" :@ V"b") - , ("fst", "ab" ! V"ab" :@ ("a" ! "b" ! V"a")) - , ("snd", "ab" ! V"ab" :@ ("a" ! "b" ! V"b")) - -- we have a lambda calculus extended with recursive bindings, so we don't need to use fix - , ("add", "x" ! "y" ! V"x" :@ V"y" :@ ("n" ! V"Succ" :@ (V"add" :@ V"n" :@ V"y"))) - , ("mul", "x" ! "y" ! V"x" :@ V"Zero" :@ ("n" ! V"add" :@ V"y" :@ (V"mul" :@ V"n" :@ V"y"))) - , ("fac", "x" ! V"x" :@ V"one" :@ ("n" ! V"mul" :@ V"x" :@ (V"fac" :@ V"n"))) - , ("eqnat", "x" ! "y" ! V"x" :@ (V"y" :@ V"True" :@ (V"const" :@ V"False")) :@ ("x1" ! V"y" :@ V"False" :@ ("y1" ! V"eqnat" :@ V"x1" :@ V"y1"))) - , ("sumto", "x" ! V"x" :@ V"Zero" :@ ("n" ! V"add" :@ V"x" :@ (V"sumto" :@ V"n"))) - -- but we could if we wanted to - -- , ("fix", "g" ! ("x" ! V"g":@ (V"x":@V"x")) :@ ("x" ! V"g":@ (V"x":@V"x"))) - -- , ("add", V"fix" :@ ("radd" ! "x" ! "y" ! V"x" :@ V"y" :@ ("n" ! V"Succ" :@ (V"radd" :@ V"n" :@ V"y")))) - -- , ("mul", V"fix" :@ ("rmul" ! "x" ! "y" ! V"x" :@ V"Zero" :@ ("n" ! V"add" :@ V"y" :@ (V"rmul" :@ V"n" :@ V"y")))) - -- , ("fac", V"fix" :@ ("rfac" ! "x" ! V"x" :@ V"one" :@ ("n" ! V"mul" :@ V"x" :@ (V"rfac" :@ V"n")))) - -- , ("eqnat", V"fix" :@ ("reqnat" ! "x" ! "y" ! V"x" :@ (V"y" :@ V"True" :@ (V"const" :@ V"False")) :@ ("x1" ! V"y" :@ V"False" :@ ("y1" ! V"reqnat" :@ V"x1" :@ V"y1")))) - -- , ("sumto", V"fix" :@ ("rsumto" ! "x" ! V"x" :@ V"Zero" :@ ("n" ! V"add" :@ V"x" :@ (V"rsumto" :@ V"n")))) - , ("n5", V"add" :@ V"two" :@ V"three") - , ("n6", V"add" :@ V"three" :@ V"three") - , ("n17", V"add" :@ V"n6" :@ (V"add" :@ V"n6" :@ V"n5")) - , ("n37", V"Succ" :@ (V"mul" :@ V"n6" :@ V"n6")) - , ("n703", V"sumto" :@ V"n37") - , ("n720", V"fac" :@ V"n6") - ] (V"eqnat" :@ V"n720" :@ (V"add" :@ V"n703" :@ V"n17")) - --- TODO: use a real pretty printer - -prettyPrec :: [String] -> Bool -> Int -> Exp String -> ShowS -prettyPrec _ _ _ (V a) = showString a -prettyPrec vs d n (x :@ y) = showParen d $ - prettyPrec vs False n x . showChar ' ' . prettyPrec vs True n y -prettyPrec (v:vs) d n (Lam b) = showParen d $ - showString v . showString ". " . prettyPrec vs False n (instantiate1 (V v) b) -prettyPrec [] _ _ (Lam _) = error "Ran out of variable names" -prettyPrec vs d n (Let bs b) = showParen d $ - showString "let" . foldr (.) id (zipWith showBinding xs bs) . - showString " in " . indent . prettyPrec ys False n (inst b) - where (xs,ys) = splitAt (length bs) vs - inst = instantiate (\n' -> V (xs !! n')) - indent = showString ('\n' : replicate (n + 4) ' ') - showBinding x b' = indent . showString x . showString " = " . prettyPrec ys False (n + 4) (inst b') - -prettyWith :: [String] -> Exp String -> String -prettyWith vs t = prettyPrec (filter (`notElem` toList t) vs) False 0 t "" - -pretty :: Exp String -> String -pretty = prettyWith $ [ [i] | i <- ['a'..'z']] ++ [i : show j | j <- [1 :: Int ..], i <- ['a'..'z'] ] - -pp :: Exp String -> IO () -pp = putStrLn . pretty - -main :: IO () -main = do - pp cooked - let result = nf cooked - if result == true - then putStrLn "Result correct." - else do - putStrLn "Unexpected result:" - pp result - exitFailure +{-# LANGUAGE CPP, TemplateHaskell #-} +module Main where + +-- this is a simple example where lambdas only bind a single variable at a time +-- this directly corresponds to the usual de bruijn presentation + +import Data.List (elemIndex) +import Data.Foldable hiding (notElem) +import Data.Maybe (fromJust) +import Data.Traversable +import Control.Monad +import Control.Applicative +import Prelude hiding (foldr,abs) +import Data.Deriving (deriveEq1, deriveOrd1, deriveRead1, deriveShow1) +import Data.Functor.Classes +import Bound +import System.Exit + + +infixl 9 :@ + +data Exp a + = V a + | Exp a :@ Exp a + | Lam (Scope () Exp a) + | Let [Scope Int Exp a] (Scope Int Exp a) + +-- | A smart constructor for Lam +-- +-- >>> lam "y" (lam "x" (V "x" :@ V "y")) +-- Lam (Scope (Lam (Scope (V (B ()) :@ V (F (V (B ()))))))) +lam :: Eq a => a -> Exp a -> Exp a +lam v b = Lam (abstract1 v b) + +-- | A smart constructor for Let bindings + +let_ :: Eq a => [(a,Exp a)] -> Exp a -> Exp a +let_ [] b = b +let_ bs b = Let (map (abstr . snd) bs) (abstr b) + where abstr = abstract (`elemIndex` map fst bs) + +instance Functor Exp where fmap = fmapDefault +instance Foldable Exp where foldMap = foldMapDefault + +instance Applicative Exp where + pure = V + (<*>) = ap + +instance Traversable Exp where + traverse f (V a) = V <$> f a + traverse f (x :@ y) = (:@) <$> traverse f x <*> traverse f y + traverse f (Lam e) = Lam <$> traverse f e + traverse f (Let bs b) = Let <$> traverse (traverse f) bs <*> traverse f b + +instance Monad Exp where +#if !(MIN_VERSION_base(4,11,0)) + return = V +#endif + V a >>= f = f a + (x :@ y) >>= f = (x >>= f) :@ (y >>= f) + Lam e >>= f = Lam (e >>>= f) + Let bs b >>= f = Let (map (>>>= f) bs) (b >>>= f) + +fmap concat $ sequence + [ deriveEq1 ''Exp + , deriveOrd1 ''Exp + , deriveRead1 ''Exp + , deriveShow1 ''Exp + , [d| instance Eq a => Eq (Exp a) where (==) = eq1 + instance Ord a => Ord (Exp a) where compare = compare1 + instance Show a => Show (Exp a) where showsPrec = showsPrec1 + instance Read a => Read (Exp a) where readsPrec = readsPrec1 + |] + ] + +-- | Compute the normal form of an expression +nf :: Exp a -> Exp a +nf e@V{} = e +nf (Lam b) = Lam $ toScope $ nf $ fromScope b +nf (f :@ a) = case whnf f of + Lam b -> nf (instantiate1 a b) + f' -> nf f' :@ nf a +nf (Let bs b) = nf (inst b) + where es = map inst bs + inst = instantiate (es !!) + +-- | Reduce a term to weak head normal form +whnf :: Exp a -> Exp a +whnf e@V{} = e +whnf e@Lam{} = e +whnf (f :@ a) = case whnf f of + Lam b -> whnf (instantiate1 a b) + f' -> f' :@ a +whnf (Let bs b) = whnf (inst b) + where es = map inst bs + inst = instantiate (es !!) + +infixr 0 ! +(!) :: Eq a => a -> Exp a -> Exp a +(!) = lam + +-- | Lennart Augustsson's example from "The Lambda Calculus Cooked 4 Ways" +-- +-- Modified to use recursive let, because we can. +-- +-- >>> nf cooked == true +-- True + +true :: Exp String +true = lam "F" $ lam "T" $ V"T" + +cooked :: Exp a +cooked = fromJust $ closed $ let_ + [ ("False", "f" ! "t" ! V"f") + , ("True", "f" ! "t" ! V"t") + , ("if", "b" ! "t" ! "f" ! V"b" :@ V"f" :@ V"t") + , ("Zero", "z" ! "s" ! V"z") + , ("Succ", "n" ! "z" ! "s" ! V"s" :@ V"n") + , ("one", V"Succ" :@ V"Zero") + , ("two", V"Succ" :@ V"one") + , ("three", V"Succ" :@ V"two") + , ("isZero", "n" ! V"n" :@ V"True" :@ ("m" ! V"False")) + , ("const", "x" ! "y" ! V"x") + , ("Pair", "a" ! "b" ! "p" ! V"p" :@ V"a" :@ V"b") + , ("fst", "ab" ! V"ab" :@ ("a" ! "b" ! V"a")) + , ("snd", "ab" ! V"ab" :@ ("a" ! "b" ! V"b")) + -- we have a lambda calculus extended with recursive bindings, so we don't need to use fix + , ("add", "x" ! "y" ! V"x" :@ V"y" :@ ("n" ! V"Succ" :@ (V"add" :@ V"n" :@ V"y"))) + , ("mul", "x" ! "y" ! V"x" :@ V"Zero" :@ ("n" ! V"add" :@ V"y" :@ (V"mul" :@ V"n" :@ V"y"))) + , ("fac", "x" ! V"x" :@ V"one" :@ ("n" ! V"mul" :@ V"x" :@ (V"fac" :@ V"n"))) + , ("eqnat", "x" ! "y" ! V"x" :@ (V"y" :@ V"True" :@ (V"const" :@ V"False")) :@ ("x1" ! V"y" :@ V"False" :@ ("y1" ! V"eqnat" :@ V"x1" :@ V"y1"))) + , ("sumto", "x" ! V"x" :@ V"Zero" :@ ("n" ! V"add" :@ V"x" :@ (V"sumto" :@ V"n"))) + -- but we could if we wanted to + -- , ("fix", "g" ! ("x" ! V"g":@ (V"x":@V"x")) :@ ("x" ! V"g":@ (V"x":@V"x"))) + -- , ("add", V"fix" :@ ("radd" ! "x" ! "y" ! V"x" :@ V"y" :@ ("n" ! V"Succ" :@ (V"radd" :@ V"n" :@ V"y")))) + -- , ("mul", V"fix" :@ ("rmul" ! "x" ! "y" ! V"x" :@ V"Zero" :@ ("n" ! V"add" :@ V"y" :@ (V"rmul" :@ V"n" :@ V"y")))) + -- , ("fac", V"fix" :@ ("rfac" ! "x" ! V"x" :@ V"one" :@ ("n" ! V"mul" :@ V"x" :@ (V"rfac" :@ V"n")))) + -- , ("eqnat", V"fix" :@ ("reqnat" ! "x" ! "y" ! V"x" :@ (V"y" :@ V"True" :@ (V"const" :@ V"False")) :@ ("x1" ! V"y" :@ V"False" :@ ("y1" ! V"reqnat" :@ V"x1" :@ V"y1")))) + -- , ("sumto", V"fix" :@ ("rsumto" ! "x" ! V"x" :@ V"Zero" :@ ("n" ! V"add" :@ V"x" :@ (V"rsumto" :@ V"n")))) + , ("n5", V"add" :@ V"two" :@ V"three") + , ("n6", V"add" :@ V"three" :@ V"three") + , ("n17", V"add" :@ V"n6" :@ (V"add" :@ V"n6" :@ V"n5")) + , ("n37", V"Succ" :@ (V"mul" :@ V"n6" :@ V"n6")) + , ("n703", V"sumto" :@ V"n37") + , ("n720", V"fac" :@ V"n6") + ] (V"eqnat" :@ V"n720" :@ (V"add" :@ V"n703" :@ V"n17")) + +-- TODO: use a real pretty printer + +prettyPrec :: [String] -> Bool -> Int -> Exp String -> ShowS +prettyPrec _ _ _ (V a) = showString a +prettyPrec vs d n (x :@ y) = showParen d $ + prettyPrec vs False n x . showChar ' ' . prettyPrec vs True n y +prettyPrec (v:vs) d n (Lam b) = showParen d $ + showString v . showString ". " . prettyPrec vs False n (instantiate1 (V v) b) +prettyPrec [] _ _ (Lam _) = error "Ran out of variable names" +prettyPrec vs d n (Let bs b) = showParen d $ + showString "let" . foldr (.) id (zipWith showBinding xs bs) . + showString " in " . indent . prettyPrec ys False n (inst b) + where (xs,ys) = splitAt (length bs) vs + inst = instantiate (\n' -> V (xs !! n')) + indent = showString ('\n' : replicate (n + 4) ' ') + showBinding x b' = indent . showString x . showString " = " . prettyPrec ys False (n + 4) (inst b') + +prettyWith :: [String] -> Exp String -> String +prettyWith vs t = prettyPrec (filter (`notElem` toList t) vs) False 0 t "" + +pretty :: Exp String -> String +pretty = prettyWith $ [ [i] | i <- ['a'..'z']] ++ [i : show j | j <- [1 :: Int ..], i <- ['a'..'z'] ] + +pp :: Exp String -> IO () +pp = putStrLn . pretty + +main :: IO () +main = do + pp cooked + let result = nf cooked + if result == true + then putStrLn "Result correct." + else do + putStrLn "Unexpected result:" + pp result + exitFailure diff --git a/src/Bound.hs b/src/Bound.hs --- a/src/Bound.hs +++ b/src/Bound.hs @@ -1,146 +1,146 @@ -{-# LANGUAGE CPP #-} - ------------------------------------------------------------------------------ --- | --- Copyright : (C) 2012 Edward Kmett --- License : BSD-style (see the file LICENSE) --- --- Maintainer : Edward Kmett --- 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 --- --- --- 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 , 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: --- --- --- --- (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 --- --- 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 +-- 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 +-- +-- +-- 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 , 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: +-- +-- +-- +-- (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 +-- +-- 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 diff --git a/src/Bound/Class.hs b/src/Bound/Class.hs --- a/src/Bound/Class.hs +++ b/src/Bound/Class.hs @@ -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 --- 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 +-- 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 (=<<<) #-} diff --git a/src/Bound/Name.hs b/src/Bound/Name.hs --- a/src/Bound/Name.hs +++ b/src/Bound/Name.hs @@ -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 --- 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 +-- 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 #-} diff --git a/src/Bound/Scope.hs b/src/Bound/Scope.hs --- a/src/Bound/Scope.hs +++ b/src/Bound/Scope.hs @@ -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 --- 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 +-- 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 diff --git a/src/Bound/Scope/Simple.hs b/src/Bound/Scope/Simple.hs --- a/src/Bound/Scope/Simple.hs +++ b/src/Bound/Scope/Simple.hs @@ -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 --- 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 +-- 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 diff --git a/src/Bound/TH.hs b/src/Bound/TH.hs --- a/src/Bound/TH.hs +++ b/src/Bound/TH.hs @@ -1,341 +1,345 @@ -{-# LANGUAGE CPP #-} -{-# LANGUAGE PatternGuards #-} - -#if __GLASGOW_HASKELL__ >= 900 -{-# LANGUAGE TemplateHaskellQuotes #-} -#else -{-# LANGUAGE TemplateHaskell #-} -#endif - ------------------------------------------------------------------------------ --- | --- Copyright : (C) 2012-2013 Edward Kmett --- License : BSD-style (see the file LICENSE) --- --- Maintainer : Edward Kmett --- Stability : experimental --- Portability : portable --- --- This is a Template Haskell module for deriving 'Applicative' and --- 'Monad' instances for data types. ----------------------------------------------------------------------------- - -module Bound.TH - ( -#ifdef MIN_VERSION_template_haskell - makeBound -#endif - ) where - -#ifdef MIN_VERSION_template_haskell -import Data.List (intercalate) -import Data.Traversable (for) -import Control.Monad (foldM, mzero, guard) -import Bound.Class (Bound((>>>=))) -import Language.Haskell.TH -import Language.Haskell.TH.Datatype.TyVarBndr - -import Control.Monad.Trans.Class (lift) -import Control.Monad.Trans.Maybe (MaybeT (..)) - --- | --- Use to automatically derive 'Applicative' and 'Monad' instances for --- your datatype. --- --- Also works for components that are lists or instances of 'Functor', --- but still does not work for a great deal of other things. --- --- The @deriving-compat@ package may be used to derive the 'Show1' and 'Read1' --- instances. Note that due to Template Haskell staging restrictions, we must --- define these instances within the same TH splice as the 'Show' and 'Read' --- instances. (This is needed for GHC 9.6 and later, where 'Show' and 'Read' --- are quantified superclasses of 'Show1' and 'Read1', respectively.) --- --- @ --- {-\# LANGUAGE DeriveFunctor #-} --- {-\# LANGUAGE TemplateHaskell #-} --- --- import Bound (Scope, makeBound) --- import Data.Functor.Classes (Show1, Read1, showsPrec1, readsPrec1) --- import Data.Deriving (deriveShow1, deriveRead1) --- --- data Exp a --- = V a --- | App (Exp a) (Exp a) --- | Lam (Scope () Exp a) --- | ND [Exp a] --- | I Int --- deriving (Functor) --- --- makeBound ''Exp --- --- concat <$> sequence --- [ deriveShow1 ''Exp --- , deriveRead1 ''Exp --- , [d| instance Read a => Read (Exp a) where readsPrec = readsPrec1 --- instance Show a => Show (Exp a) where showsPrec = showsPrec1 --- |] --- ] --- @ --- --- and in GHCi --- --- @ --- ghci> :set -XDeriveFunctor --- ghci> :set -XTemplateHaskell --- ghci> import Bound (Scope, makeBound) --- ghci> import Data.Functor.Classes (Show1, Read1, showsPrec1, readsPrec1) --- ghci> import Data.Deriving (deriveShow1, deriveRead1) --- ghci> :{ --- ghci| data Exp a = V a | App (Exp a) (Exp a) | Lam (Scope () Exp a) | ND [Exp a] | I Int deriving (Functor) --- ghci| makeBound ''Exp --- ghci| fmap concat $ sequence [deriveShow1 ''Exp, deriveRead1 ''Exp, [d| instance Read a => Read (Exp a) where { readsPrec = readsPrec1 }; instance Show a => Show (Exp a) where { showsPrec = showsPrec1 } |]] --- ghci| :} --- @ --- --- The 'Eq' and 'Ord' instances can be derived similarly: --- --- @ --- import Data.Functor.Classes (Eq1, Ord1, eq1, compare1) --- import Data.Deriving (deriveEq1, deriveOrd1) --- --- fmap concat $ sequence --- [ deriveEq1 ''Exp --- , deriveOrd1 ''Exp --- , [d| instance Eq a => Eq (Exp a) where (==) = eq1 --- instance Ord a => Ord (Exp a) where compare = compare1 --- |] --- ] --- @ --- --- or in GHCi: --- --- @ --- ghci> import Data.Functor.Classes (Eq1, Ord1, eq1, compare1) --- ghci> import Data.Deriving (deriveEq1, deriveOrd1) --- ghci> :{ --- ghci| fmap concat $ sequence [deriveEq1 ''Exp, deriveOrd1 ''Exp, [d| instance Eq a => Eq (Exp a) where { (==) = eq1 }; instance Ord a => Ord (Exp a) where { compare = compare1 } |]] --- ghci| :} --- @ --- --- We cannot automatically derive 'Eq' and 'Ord' using the standard GHC mechanism, --- because instances require @Exp@ to be a 'Monad': --- --- @ --- instance (Monad f, Eq b, Eq1 f, Eq a) => Eq (Scope b f a) --- instance (Monad f, Ord b, Ord1 f, Ord a) => Ord (Scope b f a) --- @ - -makeBound :: Name -> DecsQ -makeBound name = do - TyConI dec <- reify name - case dec of - DataD _ _name vars _ cons _ -> makeBound' name vars cons - _ -> fail $ show name ++ " Must be a data type." - -makeBound' :: Name -> [TyVarBndrUnit] -> [Con] -> DecsQ -makeBound' name vars cons = do - let instanceHead :: Type - instanceHead = name `conAppsT` map VarT (typeVars (init vars)) - - var :: ExpQ - var = ConE `fmap` getPure name vars cons - - bind :: ExpQ - bind = constructBind name vars cons - - [d| instance Applicative $(pure instanceHead) where - pure = $var - {-# INLINE pure #-} - - ff <*> fy = do - f <- ff - y <- fy - pure (f y) - {-# INLINE (<*>) #-} - - instance Monad $(pure instanceHead) where - (>>=) = $bind - {-# INLINE (>>=) #-} - |] - --- Internals -data Prop - = Bound - | Konst - | Funktor Int -- ^ number tells how many layers are there - | Exp - deriving Show - -data Components - = Component Name [(Name, Prop)] - | Variable Name - deriving Show - -constructBind :: Name -> [TyVarBndrUnit] -> [Con] -> ExpQ -constructBind name vars cons = do - interpret =<< construct name vars cons - -construct :: Name -> [TyVarBndrUnit] -> [Con] -> Q [Components] -construct name vars constructors = do - var <- getPure name vars constructors - for constructors $ \con -> do - case con of - NormalC conName [(_, _)] - | conName == var - -> pure (Variable conName) - NormalC conName types - -> Component conName `fmap` mapM typeToBnd [ ty | (_, ty) <- types ] - RecC conName types - -> Component conName `fmap` mapM typeToBnd [ ty | (_, _, ty) <- types ] - InfixC (_, a) conName (_, b) - -> do - bndA <- typeToBnd a - bndB <- typeToBnd b - pure (Component conName [bndA, bndB]) - _ -> error "Not implemented." - - where - expa :: Type - expa = name `conAppsT` map VarT (typeVars vars) - - typeToBnd :: Type -> Q (Name, Prop) - typeToBnd ty = do - boundInstance <- isBound ty - functorApp <- isFunctorApp ty - var <- newName "var" - pure $ case () of - _ | ty == expa -> (var, Exp) - | boundInstance -> (var, Bound) - | isKonst ty -> (var, Konst) - | Just n <- functorApp -> (var, Funktor n) - | otherwise -> error $ "This is bad: " - ++ show ty - ++ " " - ++ show boundInstance - - -- Checks whether a type is an instance of Bound by stripping its last - -- two type arguments: - -- isBound (Scope () EXP a) - -- -> isInstance ''Bound [Scope ()] - -- -> True - isBound :: Type -> Q Bool - isBound ty - -- We might fail with kind error, but we don't care - | Just a <- stripLast2 ty = pure False `recover` isInstance ''Bound [a] - | otherwise = return False - - isKonst :: Type -> Bool - isKonst ConT {} = True - isKonst (VarT n) = n /= tvName (last vars) - isKonst (AppT a b) = isKonst a && isKonst b - isKonst _ = False - - isFunctorApp :: Type -> Q (Maybe Int) - isFunctorApp = runMaybeT . go - where - go x | x == expa = pure 0 - go (f `AppT` x) = do - isFunctor <- lift $ isInstance ''Functor [f] - guard isFunctor - n <- go x - pure $ n + 1 - go _ = mzero - -interpret :: [Components] -> ExpQ -interpret bnds = do - x <- newName "x" - f <- newName "f" - - let - bind :: Components -> MatchQ - bind (Variable name) = do - a <- newName "a" - match - (conP name [varP a]) - (normalB (varE f `appE` varE a)) - [] - - bind (Component name bounds) = do - exprs <- foldM bindOne (ConE name) bounds - pure $ - Match - (ConP name -#if MIN_VERSION_template_haskell(2,18,0) - [] -#endif - [ VarP arg | (arg, _) <- bounds ]) - (NormalB - exprs) - [] - - bindOne :: Exp -> (Name, Prop) -> Q Exp - bindOne expr (name, bnd) = case bnd of - Bound -> - pure expr `appE` (varE '(>>>=) `appE` varE name `appE` varE f) - Konst -> - pure expr `appE` varE name - Exp -> - pure expr `appE` (varE '(>>=) `appE` varE name `appE` varE f) - Funktor n -> - pure expr `appE` (pure (fmapN n) `appE` (varE '(>>=) `sectionR` varE f) `appE` varE name) - - fmapN :: Int -> Exp - fmapN n = foldr1 (\a b -> VarE '(.) `AppE` a `AppE` b) $ replicate n (VarE 'fmap) - - matches <- for bnds bind - pure $ LamE [VarP x, VarP f] (CaseE (VarE x) matches) - -stripLast2 :: Type -> Maybe Type -stripLast2 (a `AppT` b `AppT` _ `AppT` d) - | AppT{} <- d = Nothing - | otherwise = Just (a `AppT` b) -stripLast2 _ = Nothing - --- Returns candidate -getPure :: Name -> [TyVarBndrUnit] -> [Con] -> Q Name -getPure _name tyvr cons= do - let - findReturn :: Type -> [(Name, [Type])] -> Name - findReturn ty constrs = - case [ constr | (constr, [ty']) <- constrs, ty' == ty ] of - [] -> error "Too few candidates for a variable constructor." - [x] -> x - -- data Exp a = Var1 a | Var2 a | ... - -- result in - -- Too many candidates: Var1, Var2 - xs -> error ("Too many candidates: " ++ intercalate ", " (map pprint xs)) - - -- Gets the last type variable, given 'data Exp a b c = ...' - -- - -- lastTyVar = c - lastTyVar :: Type - lastTyVar = VarT (last (typeVars tyvr)) - - allTypeArgs :: Con -> (Name, [Type]) - allTypeArgs con = case con of - NormalC conName tys -> - (conName, [ ty | (_, ty) <- tys ]) - RecC conName tys -> - (conName, [ ty | (_, _, ty) <- tys ]) - InfixC (_, t1) conName (_, t2) -> - (conName, [ t1, t2 ]) - ForallC _ _ conName -> - allTypeArgs conName - _ -> error "Not implemented" - - return (findReturn lastTyVar (allTypeArgs `fmap` cons)) - -------------------------------------------------------------------------------- --- Type mangling -------------------------------------------------------------------------------- - --- | Extract type variables -typeVars :: [TyVarBndr_ flag] -> [Name] -typeVars = map tvName - --- | Apply arguments to a type constructor. -conAppsT :: Name -> [Type] -> Type -conAppsT conName = foldl AppT (ConT conName) -#else -#endif +{-# LANGUAGE CPP #-} +{-# LANGUAGE PatternGuards #-} + +#if __GLASGOW_HASKELL__ >= 900 +{-# LANGUAGE TemplateHaskellQuotes #-} +#else +{-# LANGUAGE TemplateHaskell #-} +#endif + +----------------------------------------------------------------------------- +-- | +-- Copyright : (C) 2012-2013 Edward Kmett +-- License : BSD-style (see the file LICENSE) +-- +-- Maintainer : Edward Kmett +-- Stability : experimental +-- Portability : portable +-- +-- This is a Template Haskell module for deriving 'Applicative' and +-- 'Monad' instances for data types. +---------------------------------------------------------------------------- + +module Bound.TH + ( +#ifdef MIN_VERSION_template_haskell + makeBound +#endif + ) where + +#ifdef MIN_VERSION_template_haskell +import Data.List (intercalate) +import Data.Traversable (for) +import Control.Monad (foldM, mzero, guard) +import Bound.Class (Bound((>>>=))) +import Language.Haskell.TH +import Language.Haskell.TH.Datatype.TyVarBndr + +import Control.Monad.Trans.Class (lift) +import Control.Monad.Trans.Maybe (MaybeT (..)) + +-- | +-- Use to automatically derive 'Applicative' and 'Monad' instances for +-- your datatype. +-- +-- Also works for components that are lists or instances of 'Functor', +-- but still does not work for a great deal of other things. +-- +-- The @deriving-compat@ package may be used to derive the 'Show1' and 'Read1' +-- instances. Note that due to Template Haskell staging restrictions, we must +-- define these instances within the same TH splice as the 'Show' and 'Read' +-- instances. (This is needed for GHC 9.6 and later, where 'Show' and 'Read' +-- are quantified superclasses of 'Show1' and 'Read1', respectively.) +-- +-- @ +-- {-\# LANGUAGE DeriveFunctor #-} +-- {-\# LANGUAGE TemplateHaskell #-} +-- +-- import Bound (Scope, makeBound) +-- import Data.Functor.Classes (Show1, Read1, showsPrec1, readsPrec1) +-- import Data.Deriving (deriveShow1, deriveRead1) +-- +-- data Exp a +-- = V a +-- | App (Exp a) (Exp a) +-- | Lam (Scope () Exp a) +-- | ND [Exp a] +-- | I Int +-- deriving (Functor) +-- +-- makeBound ''Exp +-- +-- concat <$> sequence +-- [ deriveShow1 ''Exp +-- , deriveRead1 ''Exp +-- , [d| instance Read a => Read (Exp a) where readsPrec = readsPrec1 +-- instance Show a => Show (Exp a) where showsPrec = showsPrec1 +-- |] +-- ] +-- @ +-- +-- and in GHCi +-- +-- @ +-- ghci> :set -XDeriveFunctor +-- ghci> :set -XTemplateHaskell +-- ghci> import Bound (Scope, makeBound) +-- ghci> import Data.Functor.Classes (Show1, Read1, showsPrec1, readsPrec1) +-- ghci> import Data.Deriving (deriveShow1, deriveRead1) +-- ghci> :{ +-- ghci| data Exp a = V a | App (Exp a) (Exp a) | Lam (Scope () Exp a) | ND [Exp a] | I Int deriving (Functor) +-- ghci| makeBound ''Exp +-- ghci| fmap concat $ sequence [deriveShow1 ''Exp, deriveRead1 ''Exp, [d| instance Read a => Read (Exp a) where { readsPrec = readsPrec1 }; instance Show a => Show (Exp a) where { showsPrec = showsPrec1 } |]] +-- ghci| :} +-- @ +-- +-- The 'Eq' and 'Ord' instances can be derived similarly: +-- +-- @ +-- import Data.Functor.Classes (Eq1, Ord1, eq1, compare1) +-- import Data.Deriving (deriveEq1, deriveOrd1) +-- +-- fmap concat $ sequence +-- [ deriveEq1 ''Exp +-- , deriveOrd1 ''Exp +-- , [d| instance Eq a => Eq (Exp a) where (==) = eq1 +-- instance Ord a => Ord (Exp a) where compare = compare1 +-- |] +-- ] +-- @ +-- +-- or in GHCi: +-- +-- @ +-- ghci> import Data.Functor.Classes (Eq1, Ord1, eq1, compare1) +-- ghci> import Data.Deriving (deriveEq1, deriveOrd1) +-- ghci> :{ +-- ghci| fmap concat $ sequence [deriveEq1 ''Exp, deriveOrd1 ''Exp, [d| instance Eq a => Eq (Exp a) where { (==) = eq1 }; instance Ord a => Ord (Exp a) where { compare = compare1 } |]] +-- ghci| :} +-- @ +-- +-- We cannot automatically derive 'Eq' and 'Ord' using the standard GHC mechanism, +-- because instances require @Exp@ to be a 'Monad': +-- +-- @ +-- instance (Monad f, Eq b, Eq1 f, Eq a) => Eq (Scope b f a) +-- instance (Monad f, Ord b, Ord1 f, Ord a) => Ord (Scope b f a) +-- @ + +makeBound :: Name -> DecsQ +makeBound name = do + TyConI dec <- reify name + case dec of + DataD _ _name vars _ cons _ -> makeBound' name vars cons + _ -> fail $ show name ++ " Must be a data type." + +makeBound' :: Name -> [TyVarBndrVis] -> [Con] -> DecsQ +makeBound' name vars cons = do + let instanceHead :: Type + instanceHead = name `conAppsT` map VarT (typeVars (init vars)) + + var :: ExpQ + var = ConE `fmap` getPure name vars cons + + bind :: ExpQ + bind = constructBind name vars cons + + [d| instance Applicative $(pure instanceHead) where + pure = $var + {-# INLINE pure #-} + + ff <*> fy = do + f <- ff + y <- fy + pure (f y) + {-# INLINE (<*>) #-} + + instance Monad $(pure instanceHead) where + (>>=) = $bind + {-# INLINE (>>=) #-} + |] + +-- Internals +data Prop + = Bound + | Konst + | Funktor Int -- ^ number tells how many layers are there + | Exp + deriving Show + +data Components + = Component Name [(Name, Prop)] + | Variable Name + deriving Show + +constructBind :: Name -> [TyVarBndrVis] -> [Con] -> ExpQ +constructBind name vars cons = do + interpret =<< construct name vars cons + +construct :: Name -> [TyVarBndrVis] -> [Con] -> Q [Components] +construct name vars constructors = do + var <- getPure name vars constructors + for constructors $ \con -> do + case con of + NormalC conName [(_, _)] + | conName == var + -> pure (Variable conName) + NormalC conName types + -> Component conName `fmap` mapM typeToBnd [ ty | (_, ty) <- types ] + RecC conName types + -> Component conName `fmap` mapM typeToBnd [ ty | (_, _, ty) <- types ] + InfixC (_, a) conName (_, b) + -> do + bndA <- typeToBnd a + bndB <- typeToBnd b + pure (Component conName [bndA, bndB]) + _ -> error "Not implemented." + + where + expa :: Type + expa = name `conAppsT` map VarT (typeVars vars) + + typeToBnd :: Type -> Q (Name, Prop) + typeToBnd ty = do + boundInstance <- isBound ty + functorApp <- isFunctorApp ty + var <- newName "var" + pure $ case () of + _ | ty == expa -> (var, Exp) + | boundInstance -> (var, Bound) + | isKonst ty -> (var, Konst) + | Just n <- functorApp -> (var, Funktor n) + | otherwise -> error $ "This is bad: " + ++ show ty + ++ " " + ++ show boundInstance + + -- Checks whether a type is an instance of Bound by stripping its last + -- two type arguments: + -- isBound (Scope () EXP a) + -- -> isInstance ''Bound [Scope ()] + -- -> True + isBound :: Type -> Q Bool + isBound ty + -- We might fail with kind error, but we don't care + | Just a <- stripLast2 ty = pure False `recover` isInstance ''Bound [a] + | otherwise = return False + + isKonst :: Type -> Bool + isKonst ConT {} = True + isKonst (VarT n) = n /= tvName (last vars) + isKonst (AppT a b) = isKonst a && isKonst b + isKonst _ = False + + isFunctorApp :: Type -> Q (Maybe Int) + isFunctorApp = runMaybeT . go + where + go x | x == expa = pure 0 + go (f `AppT` x) = do + isFunctor <- lift $ isInstance ''Functor [f] + guard isFunctor + n <- go x + pure $ n + 1 + go _ = mzero + +interpret :: [Components] -> ExpQ +interpret bnds = do + x <- newName "x" + f <- newName "f" + + let + bind :: Components -> MatchQ + bind (Variable name) = do + a <- newName "a" + match + (conP name [varP a]) + (normalB (varE f `appE` varE a)) + [] + + bind (Component name bounds) = do + exprs <- foldM bindOne (ConE name) bounds + pure $ + Match + (ConP name +#if MIN_VERSION_template_haskell(2,18,0) + [] +#endif + [ VarP arg | (arg, _) <- bounds ]) + (NormalB + exprs) + [] + + bindOne :: Exp -> (Name, Prop) -> Q Exp + bindOne expr (name, bnd) = case bnd of + Bound -> + pure expr `appE` (varE '(>>>=) `appE` varE name `appE` varE f) + Konst -> + pure expr `appE` varE name + Exp -> + pure expr `appE` (varE '(>>=) `appE` varE name `appE` varE f) + Funktor n -> + pure expr `appE` (pure (fmapN n) `appE` (varE '(>>=) `sectionR` varE f) `appE` varE name) + + fmapN :: Int -> Exp + fmapN n = foldr1 (\a b -> VarE '(.) `AppE` a `AppE` b) $ replicate n (VarE 'fmap) + + matches <- for bnds bind + pure $ LamE [VarP x, VarP f] (CaseE (VarE x) matches) + +stripLast2 :: Type -> Maybe Type +stripLast2 (a `AppT` b `AppT` _ `AppT` d) + | AppT{} <- d = Nothing + | otherwise = Just (a `AppT` b) +stripLast2 _ = Nothing + +-- Returns candidate +getPure :: Name -> [TyVarBndrVis] -> [Con] -> Q Name +getPure _name tyvr cons= do + let + findReturn :: Type -> [(Name, [Type])] -> Name + findReturn ty constrs = + case [ constr | (constr, [ty']) <- constrs, ty' == ty ] of + [] -> error "Too few candidates for a variable constructor." + [x] -> x + -- data Exp a = Var1 a | Var2 a | ... + -- result in + -- Too many candidates: Var1, Var2 + xs -> error ("Too many candidates: " ++ intercalate ", " (map pprint xs)) + + -- Gets the last type variable, given 'data Exp a b c = ...' + -- + -- lastTyVar = c + lastTyVar :: Type + lastTyVar = VarT (last (typeVars tyvr)) + + allTypeArgs :: Con -> (Name, [Type]) + allTypeArgs con = case con of + NormalC conName tys -> + (conName, [ ty | (_, ty) <- tys ]) + RecC conName tys -> + (conName, [ ty | (_, _, ty) <- tys ]) + InfixC (_, t1) conName (_, t2) -> + (conName, [ t1, t2 ]) + ForallC _ _ conName -> + allTypeArgs conName + _ -> error "Not implemented" + + return (findReturn lastTyVar (allTypeArgs `fmap` cons)) + +------------------------------------------------------------------------------- +-- Type mangling +------------------------------------------------------------------------------- + +-- | Extract type variables +typeVars :: [TyVarBndr_ flag] -> [Name] +typeVars = map tvName + +-- | Apply arguments to a type constructor. +conAppsT :: Name -> [Type] -> Type +conAppsT conName = foldl AppT (ConT conName) + +# if !MIN_VERSION_template_haskell(2,21,0) && !MIN_VERSION_th_abstraction(0,6,0) +type TyVarBndrVis = TyVarBndrUnit +# endif +#else +#endif diff --git a/src/Bound/Term.hs b/src/Bound/Term.hs --- a/src/Bound/Term.hs +++ b/src/Bound/Term.hs @@ -1,62 +1,62 @@ ------------------------------------------------------------------------------ --- | --- Copyright : (C) 2012 Edward Kmett --- License : BSD-style (see the file LICENSE) --- --- Maintainer : Edward Kmett --- 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 +-- 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 #-} diff --git a/src/Bound/Var.hs b/src/Bound/Var.hs --- a/src/Bound/Var.hs +++ b/src/Bound/Var.hs @@ -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 --- 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 +-- 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