nom 0.1.0.0 → 0.1.0.1
raw patch · 6 files changed
+61/−26 lines, 6 files
Files
- CHANGELOG.markdown +7/−0
- nom.cabal +25/−18
- src/Language/Nominal/Blurb.txt +19/−0
- src/Language/Nominal/Examples/IdealisedEUTxO.hs +1/−1
- src/Language/Nominal/Sub.hs +0/−7
- stack.yaml +9/−0
+ CHANGELOG.markdown view
@@ -0,0 +1,7 @@+0.1.0.1+---+Fixed build error with Haddock documentation (missing file)++0.1.0.0+---+Initial release
nom.cabal view
@@ -1,19 +1,24 @@-cabal-version: 2.0-name: nom-version: 0.1.0.0-description: Nominal-flavoured implementation of data in a context of local names, following the ideas in <https://link.springer.com/article/10.1007/s001650200016 a new approach to abstract syntax with variable binding> (see also <http://www.gabbay.org.uk/papers.html#newaas-jv author's pdfs>).- __The recommended landing page is "Language.Nominal", so please go there first.__ See also: a tutorial in "Language.Nominal.Examples.Tutorial"; a short development of untyped lambda-calculus in "Language.Nominal.Examples.UntypedLambda"; an example development of System F in "Language.Nominal.Examples.SystemF"; and an example development of an EUTxO-style blockchain in "Language.Nominal.Examples.IdealisedEUTxO".-homepage: https://github.com/bellissimogiorno/nominal#readme-bug-reports: https://github.com/bellissimogiorno/nominal/issues-author: Murdoch J. Gabbay-maintainer: murdoch.gabbay@gmail.com-copyright: 2020 Murdoch J. Gabbay-license: BSD3-license-file: LICENSE-build-type: Custom-category: Language, Compilers/Interpreters-synopsis: Name-binding & alpha-equivalence- +cabal-version: 2.0+name: nom+version: 0.1.0.1+description: Nominal-flavoured implementation of data in a context of local names, following the ideas in <https://link.springer.com/article/10.1007/s001650200016 a new approach to abstract syntax with variable binding> (see also <http://www.gabbay.org.uk/papers.html#newaas-jv author's pdfs>).+ __The recommended landing page is "Language.Nominal", so please go there first.__ See also: a tutorial in "Language.Nominal.Examples.Tutorial"; a short development of untyped lambda-calculus in "Language.Nominal.Examples.UntypedLambda"; an example development of System F in "Language.Nominal.Examples.SystemF"; and an example development of an EUTxO-style blockchain in "Language.Nominal.Examples.IdealisedEUTxO".+homepage: https://github.com/bellissimogiorno/nominal#readme+bug-reports: https://github.com/bellissimogiorno/nominal/issues+author: Murdoch J. Gabbay+maintainer: murdoch.gabbay@gmail.com+copyright: 2020 Murdoch J. Gabbay+license: BSD3+license-file: LICENSE+build-type: Custom+category: Language, Compilers/Interpreters+synopsis: Name-binding & alpha-equivalence+extra-source-files:+ stack.yaml+ , src/Language/Nominal/Blurb.txt+ , CHANGELOG.markdown++ custom-setup setup-depends: base@@ -24,6 +29,7 @@ type: git location: https://github.com/bellissimogiorno/nominal + library exposed-modules: Language.Nominal.Utilities@@ -72,9 +78,10 @@ base >= 4.7 && <5, TypeCompose >= 0.9.14 && < 0.10 default-language: Haskell2010- ghc-options: -Wall + ghc-options: -Wall -- -Werror + test-suite nom-test type: exitcode-stdio-1.0 main-is: Spec.hs@@ -91,7 +98,7 @@ , Language.Nominal.Examples.IdealisedEUTxOSpec hs-source-dirs: test- ghc-options: -Wall + ghc-options: -Wall -- -Werror build-depends: base >=4.7 && <5
+ src/Language/Nominal/Blurb.txt view
@@ -0,0 +1,19 @@++{- $blurb ++The interaction of name-binding and alpha-equivalence with data can be tricky. Examples include:++* Inductively defining syntax and reductions of a syntax with binding, e.g. lambda-calculus. An example is in "Language.Nominal.Examples.SystemF".+* Graph-like structures, especially if they have dangling pointers. An example is in "Language.Nominal.Examples.IdealisedEUTxO".++This package implements a solution in Haskell, based on names and swappings. ++Features include:++* This is a package; no need to use a modified compiler.+* No state monad is imposed. Binding environments like @'Nom'@ and @'Abs'@ are available, but they track local scope not global scope and are relatively easy to escape.+* No distinction is imposed between free names and bound names. Names are just another datatype whose values can be freely passed around. Binding operators are just datatype constructors.+* Capture-avoidance is taken care of in the background.+* A well-understood mathematical reference model is available, in nominal techniques as referenced in <https://link.springer.com/article/10.1007/s001650200016 a new approach to abstract syntax with variable binding> (see also <http://www.gabbay.org.uk/papers.html#newaas-jv author's pdfs>).++-}
src/Language/Nominal/Examples/IdealisedEUTxO.hs view
@@ -390,7 +390,7 @@ singletonChunk tx = toMaybe (transactionValid tx) $ Chunk (return [tx]) -- | Creates a valid @'Chunk'@ from a single @'Transaction'@.--- If it fails (because the transaction is invalid), it raises and error.+-- If it fails (because the transaction is invalid), it raises an error. unsafeSingletonChunk :: HasCallStack => Transaction r d v -> Chunk r d v unsafeSingletonChunk = fromMaybe err . singletonChunk where
src/Language/Nominal/Sub.hs view
@@ -91,13 +91,6 @@ conc y' x = y' @@! \n -> sub n x -{-- | Nameless form of substitution, where the name for which we substitute is packaged in a @'KAbs'@ abstraction. -subApp :: (Typeable s, Swappable n, Swappable x, Swappable y, KSub (KName s n) x y) => KAbs (KName s n) y -> x -> y-subApp y' x = y' @@! \n -> sub n x -- flip sub x --- | Nameless form of substitution, where the name for which we substitute is packaged in a @'KAbs'@ abstraction ('flip'ped version). -appSub :: (Typeable s, Swappable n, Swappable x, Swappable y, KSub (KName s n) x y) => x -> KAbs (KName s n) y -> y-appSub = flip subApp --}- -- | sub on a nominal abstraction substitutes in the label, and substitutes capture-avoidingly in the body instance (Typeable s, Typeable u, KSub (KName s n) x t, KSub (KName s n) x y, Swappable t, Swappable y) =>
+ stack.yaml view
@@ -0,0 +1,9 @@+resolver: lts-15.8+packages:+- .+extra-deps:+ - Unique-0.4.7.7@sha256:2269d3528271e25d34542e7c24a4e541e27ec33460e1ea00845da95b82eec6fa,2777+ - algebra-4.3.1@sha256:323cf20c508e0b71422b767ff3a89e4188f68aa59b2df9d0fe6e9f9bae7938fb,4129+ - extra-1.6.21+ - finite-typelits-0.1.4.2 # for Data.Finite in IdealisedEUTxOSpec+ - data-default-0.7.1.1 # for Data.Default