タイプレベルのブール値に対して二重否定を証明する方法は？

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の2番目の定義はコンパイルされません、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) 

もちろん、これは些細なことのための多くの仕事です。あなたは何をやっている知っている本当に確信している場合、あなたは「ごまかす」ことができます。これはあなたがSingI制約を取り除くことができます

import Unsafe.Coerce 
import Data.Proxy 

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

：

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