Simplified Ghost of Departed proofs

0_Named.hs

-- | Our main engine for naming a value, then we can prove properties about a named value.

{-# LANGUAGE ExistentialQuantification #-} -- Used for SomeNamed.
{-# LANGUAGE PatternSynonyms #-} -- Used for the Name pattern.
{-# LANGUAGE ViewPatterns #-} -- Used for the Name pattern.
{-# LANGUAGE RankNTypes #-} -- Used for withName.

module Named ( Named, pattern Name, forgetName, withName, someNamed, SomeNamed(..) ) where

-- | Give a generated type-level name to any value.
newtype Named n a = Named_ { forgetName :: a }

withName :: a -> (forall name. Named name a -> r) -> r
withName x f = f (Named_ x)

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

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

-- | A convenient way to quickly name a value as a pattern.
pattern Name t <- (someNamed -> SomeNamed t)

1_Nonzero.hs

-- | A trivial proof of nonzero for a given named thing.
--
-- Note that only this module can produce an IsNonzero value. Hence you can only get a proof of nonzero via checkNonzero.

module Nonzero ( IsNonzero, checkNonzero ) where

import Named

data IsNonzero name = IsNonzero

checkNonzero :: (Num i, Eq i) => Named name i -> Maybe (IsNonzero name)
checkNonzero named
  | forgetName named /= 0 = Just IsNonzero
  | otherwise = Nothing

2_Div.hs

-- | A simple API that requires proof of nonzero. 
--
-- An obvious example: division requires a nonzero denominator.

module Div (divide) where

import Named
import Nonzero

divide :: Fractional i => IsNonzero y -> Named x i -> Named y i -> i
divide _ x y = (forgetName x / forgetName y)

3_Main.hs

import Div
import Nonzero
import Text.Read
import Named

main = do
  numeratorString <- getLine
  denominatorString <- getLine
  case (,) <$> readMaybe numeratorString <*> readMaybe denominatorString :: Maybe (Double, Double) of
    Nothing -> error "Both must be valid numbers."
    Just (Name numeratorNum, Name denominatorNum) ->
      case checkNonzero denominatorNum of
        Nothing -> error "Denominator must be non-zero."
        Just denominatorNonZero ->
          let result = divide denominatorNonZero numeratorNum denominatorNum
          in putStrLn ("Result: " ++ show result)

-- A monadic style is also possible thanks to the Name pattern:
main2 = do
  numeratorString <- getLine
  denominatorString <- getLine
  let maybeResult = do
        Name numeratorNum   <- readMaybe numeratorString
        Name denominatorNum <- readMaybe denominatorString
        denominatorNonZero  <- checkNonzero denominatorNum
        pure (divide denominatorNonZero numeratorNum denominatorNum)
  maybe
    (error "Something wasn't right and we don't care why.")
    print
    maybeResult

4_examples.md

Here are some example variations of Main.hs which fail to compile, demonstrating that this technique is helping the program be more correct:

This version of main fails to compile simply because I haven't named the numeratorInt.

import Div
import Nonzero
import Text.Read
import Named

main = do
  numeratorString <- getLine
  denominatorString <- getLine
  case (,) <$> readMaybe numeratorString <*> readMaybe denominatorString :: Maybe (Double, Double) of
    Nothing -> error "Both must be valid numbers."
    Just (numeratorInt, Name denominatorInt) ->
      case checkNonzero denominatorInt of
        Nothing -> error "Denominator must be non-zero."
        Just denominatorNonZero ->
          let result = divide denominatorNonZero numeratorInt denominatorInt
          in putStrLn ("Result: " ++ show result)

Couldn't match expected type ‘Named x0 Double’ with actual type ‘Double’

Here is a version where I got the arguments to divide the wrong way round:

import Div
import Nonzero
import Text.Read
import Named

main = do
  numeratorString <- getLine
  denominatorString <- getLine
  case (,) <$> readMaybe numeratorString <*> readMaybe denominatorString :: Maybe (Double, Double) of
    Nothing -> error "Both must be valid numbers."
    Just (Name numeratorInt, Name denominatorInt) ->
      case checkNonzero denominatorInt of
        Nothing -> error "Denominator must be non-zero."
        Just denominatorNonZero ->
          let result = divide denominatorNonZero  denominatorInt numeratorInt
          in putStrLn ("Result: " ++ show result)

• Couldn't match type ‘n’ with ‘n1’

The denominatorNonZero proof refers to denominatorInt by a generate name type (n1), and numeratorInt's name (n) is different.