Как доказать двойное отрицание для булевых уровней типа?

У меня есть следующий модуль:

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

Второе определение norm не компилируется, потому что flipVec v возвращает Vector (Not isCol) и, следовательно, sprod хочет a Vector (Not (Not isCol)) в качестве второго аргумента:

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)’

Я мог бы, конечно, добавить ограничение isCol ~ Not (Not isCol) к типу norm:

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

На сайте вызова фактическое значение isCol известно, и компилятор увидит, что это ограничение действительно выполнено. Но кажется странным, что детали реализации norm просачиваются в подпись типа.

Мой вопрос: возможно ли каким-то образом убедить компилятор, что isCol ~ Not (Not isCol) всегда истинно, так что лишнее ограничение не нужно?

Ответ 1

Ответ: да, это так. Доказательство довольно тривиально, если у вас есть правильные типы данных:

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

Как вы можете видеть, компилятор увидит, что доказательство тривиально при проверке различных случаев. Вы найдете все эти определения данных в нескольких пакетах, например singletons. Вы используете доказательство следующим образом:

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)

Конечно, это большая работа для такой тривиальной вещи. Если вы действительно уверены, что знаете, что делаете, вы можете "обмануть":

import Unsafe.Coerce
import Data.Proxy 

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

Это позволяет избавиться от ограничения SingI:

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