Ghost prototype

Ghost.hs

{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE ExplicitNamespaces #-}
{-# LANGUAGE TypeOperators #-}

-- |  An alternate implementation of the Ghosts of Departed Proofs <https://kataskeue.com/gdp.pdf idea>,
-- inspired by <https://ocharles.org.uk/blog/posts/2019-08-09-who-authorized-these-ghosts.html ollie's blog post>.
--
-- It omits the following from the gdp package:
--   - the Proof type: our proofs are simple enough, at least for now...
--   - type aliases: those tend to give confusing error messages
--   - the CPS-style `name` function: use the `New` pattern instead
--   - a @The@ typeclass: our 'the' is specialized to '(^::)'
--
-- The view pattern is renamed and taken from
-- https://gist.github.com/chrisdone/2178b64d18c32cfe8684066950940aaa#file-0_named-hs-L16-L24
--
-- The pattern was renamed to @New@ because that seems to be more relevant in
-- application programming.
-- When creating the type variable, the newness of it seems to be more relevant
-- than it being a name. Everything is a name.
--
-- Also it doesn't interfere with other types called @Name@ or @Named@ and it alludes
-- to the "new" keywords in OOP languages that introduce a new
-- <https://en.wikipedia.org/wiki/Identity_(object-oriented_programming) object identity>.
--
module Hercules.Server.Ghost
  ( -- * Identify values at the type level
    type (^::),
    the,
    SomeNamed (..),
    someNamed,
    pattern New
    )
where

import Text.Show(Show)

-- | A newtype that assigns a unique type level name to a value.
--
-- This allows type system to associate certain other values, to the wrapped value.
--
-- These other values may be proofs or statements about relations between values,
-- connected via the @name@.
newtype name ^:: a = Named_ {the_ :: a}
  deriving newtype (Show)

the :: name ^:: a -> a
the = the_

-- NOTE: Maybe expose SomeNamed if it makes sense to leave construction to other
--       functions? So far I've wanted to add proofs immediately and use
--       the type variable directly, which is inconvenient-to-impossible with
--       SomeNamed. (inconvenient: point-free programming, "impossible": multiple
--       names)

-- | A convenient way to name something and access the name later.
data SomeNamed a = forall name. SomeNamed (name ^:: a)

-- | Wrap a value up with a non-exposed name.
someNamed :: a -> SomeNamed a
someNamed x = SomeNamed (Named_ x)

-- | Create a new type level name for a value.
--
-- Example use:
--
-- @@@
-- thingValue & \(New thing) ->
--   use thing
--
-- use :: thing ^:: Thing -> IO ()
-- use thing = print (the thing)
-- @@@
--
-- Originally intended as a convenient way to quickly name a value as a pattern, however
-- this requires a MonadFail instance on GHC 8.6, for no good reasons.
--
-- Do notation always generates a 'MonadFail m` constraint.
-- See <https://wiki.haskell.org/MonadFail_Proposal Edward Kmett's notes>
--
-- COMPLETE pragmas <https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#complete-pragmas require> a "type signature" on the <https://gitlab.haskell.org/ghc/ghc/wikis/pattern-synonyms/complete-sigs "result type constructor">
-- when the pattern is polymorphic. This is not feasible for this pattern.
-- Hopefully, this restriction can be removed in cases where the COMPLETE pragma only has a single pattern.
pattern New :: forall a. () => forall name. (name ^:: a) -> a
pattern New t <- (someNamed -> SomeNamed t)