Haskell - désactiver la vérification de liaison d'accompagnement haskell

Question

Je ne voulais pas désactiver la fonction qui vérifie la liaison d'accompagnement dans Haskell.

La raison pour laquelle je veux faire cela est de pouvoir mettre en œuvre la preuve par contradiction. La signature de type suivante n'a aucune liaison, et ne devrait pas l'être.

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

Il n'y a pas habitant du type Refl Z (S Z), et donc il devrait y avoir aucune liaison.

Dans l'extrait ci-dessus les types signifient ce que vous attendez de telle sorte que S Z est le Peano naturel pour 1 et Refl n'a qu'un seul habitant de type Refl a a

Answer 1

Vous n'avez pas besoin: en utilisant l'extension de la langue EmptyCase , cette déclaration est réellement prouvable. Voici un fichier autonome démontrant qu'il:

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

Étant donné que vous parliez théorème de prouver dans les commentaires, il m'a fait penser et il se trouve que nous pouvons jouer un petit jeu aux utilisateurs Coq comme un peu: en utilisant une fonction diagonale au niveau du type. Cf. JF Monin Proof Trick: Small inversions. Cette fois, nous allons utiliser l'extension TypeFamilies. L'idée de rejeter un a == b contradictoire est d'utiliser une fonction de niveau type qui nous demandera de prouver un objectif trivial lorsqu'il est présenté avec a et un impossible quand il est présenté avec b. Et puis utiliser la preuve de l'égalité pour transporter le résultat trivial à l'impossible une:

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