Làm thế nào để chứng minh sự phủ định kép cho các boolean mức loại?

Question

tôi có các module sau:

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

Định nghĩa thứ hai của norm không biên dịch, vì flipVec v lợi nhuận Vector (Not isCol) và do đó sprod muốn một Vector (Not (Not isCol)) như là đối số thứ hai:

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

tôi có thể tất nhiên thêm ràng buộc isCol ~ Not (Not isCol) đến loại norm:

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

Tại trang web cuộc gọi, giá trị thực tế của isCol được biết và trình biên dịch sẽ thấy ràng buộc này thực sự hài lòng. Nhưng có vẻ lạ khi chi tiết triển khai của norm bị rò rỉ vào chữ ký loại.

Câu hỏi của tôi: có thể bằng cách nào đó thuyết phục trình biên dịch rằng isCol ~ Not (Not isCol) luôn đúng, do đó hạn chế thừa không cần thiết?

Answer 1

Câu trả lời: có, đúng vậy. Bằng chứng là khá tầm thường nếu bạn có các kiểu dữ liệu chính xác:

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 

Như bạn thấy, trình biên dịch sẽ thấy bằng chứng khi kiểm tra các trường hợp khác nhau. Bạn sẽ tìm thấy tất cả các định nghĩa dữ liệu này trong một số gói, ví dụ: singletons. Bạn sử dụng bằng chứng như vậy:

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) 

Tất nhiên điều này rất nhiều công việc cho một điều nhỏ nhặt như vậy. Nếu bạn đang thực sự chắc chắn rằng bạn biết những gì bạn đang làm, bạn có thể "ăn gian":

import Unsafe.Coerce 
import Data.Proxy 

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

này cho phép bạn thoát khỏi những hạn chế SingI:

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