टाइप लेवल बूलियन के लिए डबल नकारात्मकता कैसे साबित करें?

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)