È possibile utilizzare i GADT per dimostrare le disuguaglianze di tipo in GHC?

Question

Così, nei miei continui tentativi di mezza capire Curry-Howard attraverso piccoli esercizi Haskell, ho ottenuto bloccato a questo punto:

{-# LANGUAGE GADTs #-} 

import Data.Void 

type Not a = a -> Void 

-- | The type of type equality proofs, which can only be instantiated if a = b. 
data Equal a b where 
    Refl :: Equal a a 

-- | Derive a contradiction from a putative proof of @Equal Int Char@. 
intIsNotChar :: Not (Equal Int Char) 
intIsNotChar intIsChar = ??? 

chiaramente il tipo Equal Int Char non ha abitanti (non in basso), e quindi semanticamente ci dovrebbe essere una funzione absurdEquality :: Equal Int Char -> a ... ma per la vita di me non riesco a trovare un modo per scriverne uno diverso dall'uso di undefined.

Quindi, o:

1. mi manca qualcosa, o
2. V'è una certa limitazione del linguaggio che rende questo un compito impossibile, e io non sono riuscito a capire che cosa è.

ho il sospetto che la risposta è qualcosa di simile: il compilatore è in grado di sfruttare il fatto che non ci sono Equal costruttori che non hanno a = b. Ma se è così, cosa lo rende vero?

Answer 1

Ecco una versione più breve della soluzione di Philip JF, che è il modo in cui i teorici del tipo dipendente hanno confutato le equazioni per anni.

type family Discriminate x 
type instance Discriminate Int =() 
type instance Discriminate Char = Void 

transport :: Equal a b -> Discriminate a -> Discriminate b 
transport Refl d = d 

refute :: Equal Int Char -> Void 
refute q = transport q() 

Al fine di dimostrare che le cose sono diverse, è necessario catturarli comportarsi in modo diverso fornendo un contesto di calcolo che si traduce in osservazioni distinte. Discriminate fornisce esattamente un tale contesto: un programma a livello di carattere che tratta i due tipi in modo diverso.

Per risolvere questo problema non è necessario ricorrere a undefined. La programmazione totale a volte comporta il rifiuto di input impossibili. Anche se è disponibile lo standard undefined, è consigliabile non utilizzarlo quando è sufficiente un metodo totale: il metodo totale spiega perché qualcosa è impossibile e il tipografo conferma; undefined solo documenti la tua promessa.In effetti, questo metodo di confutazione è come Epigram dispensa da "casi impossibili" pur garantendo che un'analisi del caso copra il suo dominio.

quanto riguarda il comportamento computazionale, notare che refute, tramite transport è necessariamente rigorosa q e che q non può calcolare a testa forma normale nel contesto vuoto, semplicemente perché non esiste alcuna forma normale tale testa (e perchè il calcolo conserva tipo, di corso). In un'impostazione totale, saremo sicuri che refute non verrebbe mai richiamato in fase di esecuzione. In Haskell, siamo almeno certi che la sua argomentazione divergerà o genererà un'eccezione prima di essere obbligati a rispondere ad essa. Un pigro versione , come ad esempio

absurdEquality e = error "you have a type error likely to cause big problems" 

ignorerà la tossicità del e e dirvi che avete un errore di tipo quando non lo fanno. Preferisco

absurdEquality e = e `seq` error "sue me if this happens" 

se la confutazione onesta è troppo simile a un duro lavoro.

Answer 2

Non capisco il problema con l'utilizzo di undefined ogni tipo è abitato dal basso in Haskell. La nostra lingua non sta normalizzando fortemente ... Stai cercando la cosa sbagliata. Equal Int Char porta a errori di tipo non belle eccezioni ben tenute. Si veda

{-# LANGUAGE GADTs, TypeFamilies #-} 

data Equal a b where 
    Refl :: Equal a a 

type family Pick cond a b 
type instance Pick Char a b = a 
type instance Pick Int a b = b 

newtype Picker cond a b = Picker (Pick cond a b) 

pick :: b -> Picker Int a b 
pick = Picker 

unpick :: Picker Char a b -> a 
unpick (Picker x) = x 

samePicker :: Equal t1 t2 -> Picker t1 a b -> Picker t2 a b 
samePicker Refl x = x 

absurdCoerce :: Equal Int Char -> a -> b 
absurdCoerce e x = unpick (samePicker e (pick x)) 

si potrebbe usare questo per creare la funzione che si desidera

absurdEquality e = absurdCoerce e() 

ma che produrrà un comportamento indefinito come sua norma di calcolo. false dovrebbe causare l'interruzione di programmi o almeno eseguire per sempre. Aborting è la regola di calcolo che è simile a trasformare la logica minima in logica intiutiva aggiungendo no. La definizione corretta è

absurdEquality e = error "you have a type error likely to cause big problems" 

per quanto riguarda la domanda nel titolo: essenzialmente no. Per quanto ne so, l'ineguaglianza di tipo non è rappresentabile in modo pratico nell'attuale Haskell. Le modifiche apportate al sistema dei tipi potrebbero portare a un miglioramento, ma al momento abbiamo uguaglianze ma non disuguaglianze.