如何证明类型级布尔值的双重否定？

Question

我有以下模块:

{-# 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一个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)始终为真,因此不需要多余的约束？

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