Wie beweisen Sie die doppelte Negation für Boolesche Typen?

Question

Ich habe folgendes Modul:

{-# LANGUAGE DataKinds, KindSignatures, TypeFamilies, RoleAnnotations #-} 
module Main where 

import Data.Coerce (coerce) 

-- logical negation for type level booleans 
type family Not (x :: Bool) where 
    Not True = False 
    Not False = True 

-- a 3D vector with a phantom parameter that determines whether this is a 
-- column or row vector 
data Vector (isCol :: Bool) = Vector Double Double Double 

type role Vector phantom 

-- convert column to row vector or row to column vector 
flipVec :: Vector isCol -> Vector (Not isCol) 
flipVec = coerce 

-- scalar product is only defined for vectors of different types 
-- (row times column or column times row vector) 
sprod :: Vector isCol -> Vector (Not isCol) -> Double 
sprod (Vector x1 y1 z1) (Vector x2 y2 z2) = x1*x2 + y1*y2 + z1*z2 

-- vector norm defined in terms of sprod 
norm :: Vector isCol -> Double 
-- this definition compiles 
norm v = sqrt (v `sprod` flipVec v) 
-- this does not (without an additional constraint, see below) 
norm v = sqrt (flipVec v `sprod` v) 

main = undefined 

Die zweite Definition von norm nicht kompilieren, weil flipVec v kehrt Vector (Not isCol) und damit sprod eine Vector (Not (Not isCol)) als zweites Argument will:

Main.hs:22:34:                              
    Couldn't match type ‘isCol’ with ‘Not (Not isCol)’                    
     ‘isCol’ is a rigid type variable bound by                      
       the type signature for norm :: Vector isCol -> Double                 
       at Main.hs:20:9                          
    Expected type: Vector (Not (Not isCol))                       
     Actual type: Vector isCol                          
    Relevant bindings include                          
     v :: Vector isCol (bound at Main.hs:22:6)                      
     norm :: Vector isCol -> Double (bound at Main.hs:22:1)                   
    In the second argument of ‘sprod’, namely ‘v’                     
    In the first argument of ‘sqrt’, namely ‘(flipVec v `sprod` v)’ 

Ich könnte natürlich hinzufügen die Bedingung isCol ~ Not (Not isCol) zum Typ norm:

norm :: isCol ~ Not (Not isCol) => Vector isCol -> Double 

Am Aufrufort ist der tatsächliche Wert von isCol bekannt und der Compiler wird sehen, dass diese Einschränkung tatsächlich erfüllt ist. Aber es scheint komisch, dass die Implementierungsdetails von norm in die Typ-Signatur eindringen.

Meine Frage: ist es irgendwie möglich, den Compiler zu überzeugen, dass isCol ~ Not (Not isCol) immer wahr ist, so dass die überflüssige Einschränkung nicht notwendig ist?

Answer 1

Die Antwort: ja, ist es. Der Beweis ist ziemlich trivial, wenn Sie die richtigen Datentypen haben:

data family Sing (x :: k) 

class SingI (x :: k) where 
    sing :: Sing x 

data instance Sing (x :: Bool) where 
    STrue :: Sing True 
    SFalse :: Sing False 

type SBool x = Sing (x :: Bool) 

data (:~:) x y where 
    Refl :: x :~: x 

double_neg :: SBool x -> x :~: Not (Not x) 
double_neg x = case x of 
       STrue -> Refl 
       SFalse -> Refl 

Wie Sie sehen können, wird der Compiler sehen, dass der Nachweis der bei der Untersuchung der verschiedenen Fällen trivial ist. Sie finden alle diese Datendefinitionen in mehreren Paketen, z. B. . Sie verwenden den Beweis wie folgt:

instance Sing True where sing = STrue 
instance Sing False where sing = SFalse 

norm :: forall isCol . SingI isCol => Vector isCol -> Double 
norm v = case double_neg (sing :: Sing isCol) of 
      Refl -> sqrt (flipVec v `sprod` v) 

Natürlich ist das eine Menge Arbeit für so eine triviale Sache. Wenn Sie wirklich sicher sind, wissen Sie, was Sie tun, können Sie „betrügen“:

import Unsafe.Coerce 
import Data.Proxy 

double_neg' :: Proxy x -> x :~: Not (Not x) 
double_neg' _ = unsafeCoerce (Refl ::() :~:()) 

Auf diese Weise können Sie von der SingI Zwang loszuwerden:

norm' :: forall isCol . Vector isCol -> Double 
norm' v = case double_neg' (Proxy :: Proxy isCol) of 
      Refl -> sqrt (flipVec v `sprod` v)