È sempre sicuro usare unsafeCoerce per le uguaglianze valide?

Question

Ho un tipo di testimone per gli elenchi tipo di livello,

data List xs where 
    Nil :: List '[] 
    Cons :: proxy x -> List xs -> List (x ': xs) 

nonché le seguenti utilità.

-- Type level append 
type family xs ++ ys where 
    '[] ++ ys = ys 
    (x ': xs) ++ ys = x ': (xs ++ ys) 

-- Value level append 
append :: List xs -> List ys -> List (xs ++ ys) 
append Nil ys = ys 
append (Cons x xs) ys = Cons x (append xs ys) 

-- Proof of associativity of (++) 
assoc :: List xs -> proxy ys -> proxy' zs -> ((xs ++ ys) ++ zs) :~: (xs ++ (ys ++ zs)) 
assoc Nil _ _ = Refl 
assoc (Cons _ xs) ys zs = case assoc xs ys zs of Refl -> Refl 

Ora, ho due definizioni diverse ma equivalenti di una funzione inversa tipo-livello,

-- The first version, O(n) 
type Reverse xs = Rev '[] xs 
type family Rev acc xs where 
    Rev acc '[] = acc 
    Rev acc (x ': xs) = Rev (x ': acc) xs 

-- The second version, O(n²) 
type family Reverse' xs where 
    Reverse' '[] = '[] 
    Reverse' (x ': xs) = Reverse' xs ++ '[x] 

Il primo è più efficiente, ma il secondo è più facile da usare quando dimostrando cose al compilatore , quindi sarebbe bello avere una prova di equivalenza. Per fare ciò, ho bisogno di una prova di Rev acc xs :~: Reverse' xs ++ acc. Questo è ciò che mi si avvicinò con:

revAppend :: List acc -> List xs -> Rev acc xs :~: Reverse' xs ++ acc 
revAppend _ Nil = Refl 
revAppend acc (Cons x xs) = 
    case (revAppend (Cons x acc) xs, assoc (reverse' xs) (Cons x Nil) acc) of 
     (Refl, Refl) -> Refl 

reverse' :: List xs -> List (Reverse' xs) 
reverse' Nil = Nil 
reverse' (Cons x xs) = append (reverse' xs) (Cons x Nil) 

Purtroppo, revAppend è O (n³), che sconfigge completamente lo scopo di questo esercizio. Tuttavia, siamo in grado di bypassare tutto questo e ottenere O (1) utilizzando unsafeCoerce:

revAppend :: Rev acc xs :~: Reverse' xs ++ acc 
revAppend = unsafeCoerce Refl 

Questa funzione è sicura? E il caso generale? Ad esempio, se ho due famiglie di tipi F :: k -> * e G :: k -> * e so che sono equivalenti, è sicuro definire quanto segue?

equal :: F a :~: G a 
equal = unsafeCoerce Refl 

Answer 1

Sarebbe molto bello se GHC utilizzato un correttore di terminazione sulle espressioni e::T dove T ha solo un costruttore senza argomenti K (ad esempio :~:, ()). Quando il controllo riesce, GHC potrebbe riscrivere e come K saltando completamente il calcolo. Dovresti escludere FFI, unsafePerformIO, trace, ... ma sembra fattibile. Se questo fosse implementato, risolverebbe la domanda postata molto bene, permettendo a uno di scrivere effettivamente prove senza costi di runtime.

In caso contrario, è possibile utilizzare unsafeCoerce nel frattempo, come si propone. Se sei davvero, davvero sicuro che due tipi sono uguali puoi usarlo tranquillamente. L'esempio tipico è l'implementazione di Data.Typeable. Ovviamente, un uso improprio di unsafeCoerce su tipi diversi porterebbe a effetti imprevedibili, si spera che si verifichi un arresto anomalo.

Si potrebbe anche scrivere il proprio variante "sicura" di unsafeCoerce:

unsafeButNotSoMuchCoerce :: (a :~: b) -> a -> b 
#ifdef CHECK_TYPEEQ 
unsafeButNotSoMuchCoerce Refl = id 
#else 
unsafeButNotSoMuchCoerce _ = unsafeCoerce 
#endif 

Se CHECK_TYPEEQ definito porta a codice più lento. Se non definito, lo salta e lo costruisce a costo zero. In quest'ultimo caso non è ancora sicuro perché è possibile passare il fondo come primo argomento e il programma non si arresta ma eseguirà invece la coercizione sbagliata. In questo modo puoi testare il tuo programma in modalità sicura ma lenta, quindi passare alla modalità non sicura e pregare che le tue "prove" siano sempre terminate.