Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 6 additions & 6 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
15 changes: 7 additions & 8 deletions modal-programming.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
13 changes: 6 additions & 7 deletions src/Control/Modal.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down