diff --git a/CHANGELOG.markdown b/CHANGELOG.markdown new file mode 100644 --- /dev/null +++ b/CHANGELOG.markdown @@ -0,0 +1,7 @@ +0.1.0.1 +--- +Fixed build error with Haddock documentation (missing file) + +0.1.0.0 +--- +Initial release diff --git a/nom.cabal b/nom.cabal --- a/nom.cabal +++ b/nom.cabal @@ -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 (see also ). - __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 (see also ). + __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 diff --git a/src/Language/Nominal/Blurb.txt b/src/Language/Nominal/Blurb.txt new file mode 100644 --- /dev/null +++ b/src/Language/Nominal/Blurb.txt @@ -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 (see also ). + +-} diff --git a/src/Language/Nominal/Examples/IdealisedEUTxO.hs b/src/Language/Nominal/Examples/IdealisedEUTxO.hs --- a/src/Language/Nominal/Examples/IdealisedEUTxO.hs +++ b/src/Language/Nominal/Examples/IdealisedEUTxO.hs @@ -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 diff --git a/src/Language/Nominal/Sub.hs b/src/Language/Nominal/Sub.hs --- a/src/Language/Nominal/Sub.hs +++ b/src/Language/Nominal/Sub.hs @@ -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) => diff --git a/stack.yaml b/stack.yaml new file mode 100644 --- /dev/null +++ b/stack.yaml @@ -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