src/Logic.hs

   1 {-# LANGUAGE Safe #-}
   2
   3 -- | An alternative implementation of `RefGhostOfDepartedProofs`.
   4 module Logic (
   5   module Logic.Kernel,
   6   type RefGhostOfDepartedProofs,
   7 ) where
   8
   9 import Logic.Kernel
  10
  11 data RefGhostOfDepartedProofs
  12 -- ^ Reference to [Ghosts of departed proofs](https://doi.org/10.1145/3242744.3242755)
  13 --
  14 -- > {
  15 -- >   "DOI": "10.1145/3242744.3242755",
  16 -- >   "ISBN": "9781450358354",
  17 -- >   "URL": "https://doi.org/10.1145/3242744.3242755",
  18 -- >   "abstract": "Library authors often are faced with a design choice: should a function with preconditions be implemented as a partial function, or by returning a failure condition on incorrect use? Neither option is ideal. Partial functions lead to frustrating run-time errors. Failure conditions must be checked at the use-site, placing an unfair tax on the users who have ensured that the function’s preconditions were correctly met. In this paper, we introduce an API design concept called “ghosts of departed proofs” based on the following observation: sophisticated preconditions can be encoded in Haskell’s type system with no run-time overhead, by using proofs that inhabit phantom type parameters attached to newtype wrappers. The user expresses correctness arguments by constructing proofs to inhabit these phantom types. Critically, this technique allows the library user to decide when and how to validate that the API’s preconditions are met. The “ghosts of departed proofs” approach to API design can achieve many of the benefits of dependent types and refinement types, yet only requires some minor and well-understood extensions to Haskell 2010. We demonstrate the utility of this approach through a series of case studies, showing how to enforce novel invariants for lists, maps, graphs, shared memory regions, and more.",
  19 -- >   "author": [
  20 -- >     {
  21 -- >       "family": "Noonan",
  22 -- >       "given": "Matt"
  23 -- >     }
  24 -- >   ],
  25 -- >   "collection-title": "Haskell 2018",
  26 -- >   "container-title": "Proceedings of the 11th ACM SIGPLAN International Symposium on Haskell",
  27 -- >   "id": "10.1145/3242744.3242755",
  28 -- >   "issued": {
  29 -- >     "date-parts": [
  30 -- >       [
  31 -- >         2018
  32 -- >       ]
  33 -- >     ]
  34 -- >   },
  35 -- >   "keyword": "API design, formal methods, higher-rank types, software engineering",
  36 -- >   "page": "119-131",
  37 -- >   "publisher": "Association for Computing Machinery",
  38 -- >   "publisher-place": "New York, NY, USA",
  39 -- >   "title": "Ghosts of departed proofs (functional pearl)",
  40 -- >   "type": "paper-conference"
  41 -- > }