Haskell - 禁用伴隨綁定檢查haskell

Question

我不想禁用在Haskell中檢查伴隨綁定的函數。

我想這樣做的原因是能夠通過矛盾來實施證明。以下類型的簽名沒有任何約束力，不應該如此。

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

Refl Z (S Z)類型沒有居民，因此應該沒有約束力。

在上面的代碼中的類型意味着你可以預料到的，使得S Z是皮亞諾自然的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 {} 

既然你都在談論定理的評論證明它讓我的思想和事實證明，我們可以玩一個小遊戲勒柯克用戶喜歡頗有幾分：使用類型級別的對角線函數。參看JF Monin的Proof Trick: Small inversions。這次我們將使用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())