在Haskell中使用Ghosts of Departed Proofs的方式是否正确？

参考文献 #

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.

实践代码 #

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"

技术问题解答 #

1. 实现是否符合GDP思路？ #

你的实现完全贴合GDP（Ghosts of Departed Proofs）的核心设计思路：

• 用幽灵类型（NumPositive/NumNegative/NumZero）编码数值的符号属性，这类类型仅存在于编译期，运行时无额外开销；
• 通过Proof和Sgn类型将证明与具体值绑定，getSgn通过一次动态判断生成对应属性的证明，把动态检查结果固化到类型系统中；
• getPositive要求输入带有NumPositive证明的值，确保只有正数能通过编译检查，实现了GDP"一次动态检查，全程静态安全"的核心目标。

代码中使用的a ~~ xs、name、...等GDP库语法，也完全符合论文中"将证明与值绑定，通过幽灵类型传递证明上下文"的模式。

2. GDP库是否会带来类似Maybe的匹配繁琐开销？ #

确实会有类似模式匹配的"仪式感"，但二者本质不同，且开销可控：

• Maybe的模式匹配是处理值的存在性，而GDP的匹配是处理证明的传递——你是在向类型系统确认"该值满足某属性，现在把这个证明传递给后续逻辑"；
• 这种开销可以通过封装降低：比如编写高阶函数封装getSgn的分支逻辑，或者利用类型类自动推导证明，避免重复手动匹配；
• 这种"开销"换回来的是编译期的安全保证——比如你无法将负数传入要求正数的函数，这在普通Haskell中只能靠运行时检查，而GDP将这类错误提前到编译阶段暴露。

内容的提问来源于stack exchange，提问作者Seeker