Navigation Menu

Skip to content

Instantly share code, notes, and snippets.

@roberth
Created November 11, 2019 14:53
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save roberth/cd4cc445372839198a52b2a33c5d5b55 to your computer and use it in GitHub Desktop.
Save roberth/cd4cc445372839198a52b2a33c5d5b55 to your computer and use it in GitHub Desktop.
Ghost prototype
{-# 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)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment