diff --git a/README.md b/README.md index f8483cc..813c480 100644 --- a/README.md +++ b/README.md @@ -5,12 +5,12 @@ Haskell 2010 extended with higher-rank polymorphism is approximately System F*ω* and thus roughly corresponds to intuitionistic higher-order propositional logic via a Curry–Howard isomorphism. GHC’s static pointers extension, while having been conceived specifically for -distributed programming, further extends Haskell such that it becomes a -kind of generic modal programming language. This allows programmers to -write libraries that turn Haskell into the Curry–Howard correspondents -of various modal logics and to combine these libraries to arrive at -programming languages that integrate multiple modal features. The -`modal-programming` package provides support for writing such libraries. +distributed programming, makes it possible to turn Haskell into the +Curry–Howard correspondents of typical modal logics. Since the static +pointers extension only provides the necessary basis for modal +programming, specific features of languages corresponding to concrete +modal logics must be implemented as libraries. The `modal-programming` +package provides support for writing such libraries. Modal logics and modal programming languages diff --git a/modal-programming.cabal b/modal-programming.cabal index f3b726c..df09270 100644 --- a/modal-programming.cabal +++ b/modal-programming.cabal @@ -16,14 +16,13 @@ description: Haskell 2010 extended with higher-rank polymorphism is intuitionistic higher-order propositional logic via a Curry–Howard isomorphism. GHC’s static pointers extension, while having been conceived specifically for distributed - programming, further extends Haskell such that it becomes a - kind of generic modal programming language. This allows - programmers to write libraries that turn Haskell into the - Curry–Howard correspondents of various modal logics and to - combine these libraries to arrive at programming languages - that integrate multiple modal features. The - @modal-programming@ package provides support for writing - such libraries. + programming, makes it possible to turn Haskell into the + Curry–Howard correspondents of typical modal logics. Since + the static pointers extension only provides the necessary + basis for modal programming, specific features of languages + corresponding to concrete modal logics must be implemented + as libraries. The @modal-programming@ package provides + support for writing such libraries. category: Control, Effect, Type System tested-with: GHC == { 8.10.7, 9.2.3 } extra-source-files: README.md CHANGELOG.md CONTRIBUTING.md diff --git a/src/Control/Modal.hs b/src/Control/Modal.hs index 7dd67bd..f21622b 100644 --- a/src/Control/Modal.hs +++ b/src/Control/Modal.hs @@ -3,13 +3,12 @@ System F/ω/ and thus roughly corresponds to intuitionistic higher-order propositional logic via a Curry–Howard isomorphism. GHC’s static pointers extension, while having been conceived specifically for distributed - programming, further extends Haskell such that it becomes a kind of generic - modal programming language. This allows programmers to write libraries that - turn Haskell into the Curry–Howard correspondents of various modal logics - and to combine these libraries to arrive at programming languages that - integrate multiple modal features. The @Control.Modal@ module provides - support for writing such libraries. - + programming, makes it possible to turn Haskell into the Curry–Howard + correspondents of typical modal logics. Since the static pointers extension + only provides the necessary basis for modal programming, specific features + of languages corresponding to concrete modal logics must be implemented as + libraries. The @Control.Modal@ module provides support for writing such + libraries. = Modal logics and modal programming languages