Haskell -禁用伴随绑定检查haskell

Question

我不打算在Haskell中禁用检查伴随绑定的函数。

我之所以要这样做，是为了能够用矛盾来证明。下面的类型签名没有任何绑定，也不应该有绑定。

zeroDoesNotEqualOne :: Refl Z (S Z) -> Bottom

类型Refl Z (S Z)没有居民，因此不应该有绑定。

在上面的片段中，类型意味着您所期望的那样，S Z是Peano自然的1，而Refl只有一个Refl a a类型的居民。

Answer 1

您不需要:使用EmptyCase语言扩展，这个语句实际上是可证明的。下面是一个自我包含的文件，演示它：

{-# LANGUAGE GADTs         #-}
{-# LANGUAGE PolyKinds     #-}
{-# LANGUAGE DataKinds     #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE EmptyCase     #-}

module ZeroNeqOne where

data (==) a b where
  Refl :: a == a

data Nat where
  Z :: Nat
  S :: Nat -> Nat

zeroNeqOne :: Z == S Z -> a
zeroNeqOne p = case p of {}

考虑到你是在讨论定理证明，在注释中，它让我思考，结果我们可以玩一些游戏，Coq用户非常喜欢:在类型级别上使用对角线函数。请参阅JF Monin的证明技巧:小倒置。这一次我们将使用TypeFamilies扩展。抛弃一个矛盾的a == b的想法是使用一个类型级别的函数，它将要求我们在给出a时证明一个微不足道的目标，当给出b时证明一个不可能的目标。然后用等式的证明将琐碎的结果传递给不可能的结果：

{-# LANGUAGE GADTs         #-}
{-# LANGUAGE PolyKinds     #-}
{-# LANGUAGE DataKinds     #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies  #-}

module ZeroNeqOneDiag where

import Data.Void

data (==) a b where
  Refl :: a == a

subst :: a == b -> p a -> p b
subst Refl pa = pa

data Nat where
  Z :: Nat
  S :: Nat -> Nat

type family Diag (n :: Nat) :: * where
  Diag 'Z     = ()
  Diag ('S n) = Void

newtype Diagonal n = Diagonal { runDiagonal :: Diag n }

zeroNeqOneDiag :: 'Z == 'S 'Z -> Void
zeroNeqOneDiag p = runDiagonal $ subst p (Diagonal ())