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 {} 

を考えると、あなたがコメントで定理証明を話していたこと、それは私が考えるようになったし、それは我々がかなりのような小さなゲームCoqのユーザーを再生することができ判明：使用します型レベルの対角関数。 Cf。 JF Monin's Proof Trick: Small inversions。今回は、拡張子TypeFamiliesを使用します。矛盾を破棄する考え方a == bは、aと表示されたときに些細な目標を証明し、bと表示されたときに不可能な目標を証明するよう求めるタイプレベル関数を使用することです。そして、不可能なものに平凡な結果を輸送するために平等の証明を使用します。 `zeroNeqOne :: Z == Z - > A`、それはshouldnの」：

{-# 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())