Birim tipleri eşittir postular güvenli midir?

Question

Her türlü tür ()'un aynı olduğunu kabul etmek güvenli midir? Yani, tip güvenliği kırmak için aşağıdakiler kullanılabilir mi?

-- Bad postulate 
unitsEqual :: (x ::()) :~: (y ::()) 
unitsEqual = unsafeCoerce (Refl :: '() :~: '()) 

Answer 1

Bu ghc 7.8.3 altında güvensiz (aşağıdaki kodu bakınız). User2407038 ifadesiyle, aşağıdakiler GHC 7.10.3 tarafından reddedilmiştir. Şaşırtıcı olmayan bir şekilde, bu veri ailesi, tip denetçisinin yasaklamak için değiştirildiğinden yeterince kötüydü. Hala bunun 7.10.3 altında gerçekleşmesinin bir yolu olup olmadığını görmeye çalışıyorum.

{-# LANGUAGE TypeFamilies #-} 
{-# LANGUAGE TypeOperators #-} 
{-# LANGUAGE KindSignatures #-} 
{-# LANGUAGE DataKinds #-} 

module UnitsEqual where 
import Unsafe.Coerce 
import Data.Type.Equality 

data family Yeah (a ::()) b c 
data instance Yeah '() b c = Yeah { yeah :: b } 
data instance Yeah a b c = Nope c 

-- Entirely valid 
castYeah :: x :~: y -> Yeah x p q -> Yeah y p q 
castYeah Refl x = x 

-- Bad postulate 
unitsEqual :: (x ::()) :~: (y ::()) 
unitsEqual = unsafeCoerce (Refl :: '() :~: '()) 

-- Oh no! This doesn't actually cast, but 
-- it's horrible enough. It consistently produces 
-- either segmentation faults or nonsense, 
-- whether the types are the same or not. 
uc :: a -> b 
uc a = yeah $ castYeah unitsEqual (Nope a) 

Ben Void yaşayan sıkışmış/sahte türlerinin herhangi ayırt etmek bariz yolu yoktur çünkü

voidsEqual :: (a :: Void) :~: (b :: Void) 

önermeyi güvenli olduğunu, ancak, inanmak .

Answer 2

Sorumluluk reddi: Bu yanıt esasen tahmin çalışmasıdır, çünkü bu davranış gerçekten beni şaşırttı ve ben hala tam olarak typechecker içinde Any semantiklerinden çok emin değilim. o belirsiz bir tip değişken bulur ve Any bunu somutlaştırır Nope a tipi hesaplar zaman Yeah muhtemelen reddedilmesi gerektiğini göz ardı senin örnekte

. Bu, örn. length [] çalışması.

Sen ghc 7.10 kabul edilen bir GADT, Aynı işlemleri :, eşitlik '() ~ Any

data Yeah (a ::()) b c where 
    Yeah :: b -> Yeah '() b c 
    Nope :: c -> Yeah Any b c 

ikinci durumda bir işlev

yeah :: Yeah '() b c -> b 
yeah (Yeah a) = a 
yeah (Nope _) = error "???" 

ihtiyaç uc yazmak için ise verdiğim gibi, örneğin

okay :: 'True :~: 'False -> x 
-- okay Refl = error "???" -- Compiler rejects this case 
okay x = case x of 

ama bu bir: 'True ~ 'False, Int ~ Bool vb typechecker bu gerçekleri bilir!

really :: Any :~: '() -> x 
really Refl = error "???" -- Perfectly valid pattern match 

Aslında bu işlevi çağırmak olamaz:

>:t really Refl 

<interactive>:1:8: Warning: 
    Couldn't match type `Any' with '() 
    Expected type: Any :~: '() 
     Actual type: '() :~: '() 
    In the first argument of `really', namely `Refl' 
    In the expression: really Refl 

ve süre uc typechecks (tanım değişmedi) artık kırar:

>uc 'a' :: Int 
*** Exception: ??? 

O typechecker yapar gibi görünüyor '() :~: Any'un iskan edilmediğine inanmayın, çünkü bu, çünkü typechecker dahili olarak böyle bir kanıt üretmesine izin verilir, ancak kullanıcı hala sağa sola Kendileri yazıyor.

Tüm söylemek gerekirse: Bence Any varsa, unitsEqual sesli ve Any varoluşundan kaynaklanır.Any :~: '() - - kar¸ıt tarafından açıkça yanlış olduğu görünüyor ama x ~ yx ve y farklı türleri vardır ve ne x veya yAny yalnızca trivially yanlış olduğunu söylüyor Any için özel typechecker kural var gibi görünüyor.

voidEqual eşit çürük olduğu için Any :: Void, Any Any :: Void, Any Any Any :: Void vb