Is this a proper way to exploit Ghosts of Departed Proofs in Haskell?

Question

I'm experimenting with the approach introduced in:

Matt Noonan. 2018. Ghosts of departed proofs (functional pearl). In Proceedings of the 11th ACM SIGPLAN International Symposium on Haskell (Haskell 2018). Association for Computing Machinery, New York, NY, USA, 119–131. https://doi.org/10.1145/3242744.3242755

I've written some toy code to play with the ideas presented in the paper:

data NumPositive num

data NumNegative num

data NumZero num

data Sgn a num where
  SgnNeg :: (Num a, Ord a) => Proof (NumNegative num) -> Sgn a num
  SgnPos :: (Num a, Ord a) => Proof (NumPositive num) -> Sgn a num
  SgnZero :: (Num a, Ord a) => Proof (NumZero num) -> Sgn a num

getSgn :: (Num a, Ord a) => (a ~~ xs) -> Sgn a num
getSgn = classify . the
  where
    classify num
      | num > 0 = SgnPos axiom
      | num < 0 = SgnNeg axiom
      | otherwise = SgnZero axiom

getPositive :: (Num a, Ord a) => (a ~~ num ::: NumPositive xs) -> a
getPositive = the

main :: IO ()
main = do
  let x = 4.0 :: Double
  name x $ \y -> case getSgn y of
    SgnPos proof -> print . getPositive $ y ... proof
    _ -> print "Nonpositive"

Questions: Is this the correct way to exploit the approach outlined in the paper? Doesn't this introduce similar toil overhead for the user of a library written using GDP as if they have to pattern-match values wrapped in Maybe?

Answer 1

I believe the point of the GDP approach is to provide a mechanism for a library author to export proof-making tools to the library user, so that they can construct new proofs.

The gdpEndpts example in Figure 1 of the paper is able to determine that the list xs is non-empty via the classify call:

name xs $ \xs -> case classify xs of
    IsCons proof -> _

and then exploit the proof of its non-emptyness not only directly to safely extract the first element of this non-empty list:

-> (return (gdpHead (xs ...proof), _)

but also indirectly by deriving a proof that the reversed list is non-empty using the rev_cons axiom, in order to safely extract the last element (the head of the reversed list):

-> (_, gdpHead (gdpReverse xs ...rev_cons proof))

There's not much point to GDP if you aren't using combinators like rev_cons to manipulate an existing proof to learn something new about a derived value.

So, for your use case, if you only need to know a fact about values in isolation, like that a particular Double value is positive, then a smart constructor that returns Maybe is sufficient. The resulting newtype PositiveDouble = PositiveDouble Double (or whatever) provides proof of the single fact that the contained Double is positive, and you don't need anything else.

But, if you want to take a proof that x is positive and y is negative and turn it into a proof that x-y is positive using the axioms that the negation of a negative double is positive and the sum of two positive doubles is positive, then the GDP approach provides a framework for expressing that sort of proof derivation within a unified framework across your library.