我正在嘗試使用:~:Data.Type.Equality在編譯時確定型別相等性。我的期望是它的行為符合 Scala 確定型別相等性的標準方式：
case class Equals[A >: B <:B , B]()
Equals[Int, Int] // compiles fine
Equals[String, Int] // doesn't compile
所以我嘗試了
foo :: Int :~: Bool
foo = undefined
我希望它會失敗，因為Int :~: Bool它是可居住的。但它編譯得很好。
應該如何
:~:作業？的檔案對Data.Type.Equality我來說非常難以理解，我無法在任何地方找到一個簡潔的例子。也許我完全偏離了軌道。在那種情況下，我怎樣才能
Equals在 Haskell 中實作示例的語意？
uj5u.com熱心網友回復：
就像我們 Haskell 人經常假裝的那樣，Haskell 中的每個正常1型別都是有人居住的。這包括data Void，它包括a :~: b所有a和b。除了我們通常承認的禮貌價值觀外，還有最低價值觀。
undefined :: a是產生任何型別的底值的一種方法a。所以特別是undefined :: Int :~: Bool，因此您的代碼是完全正確的型別。
如果您想要一個在編譯時無法證明相等性而無法編譯的型別相等性，那么您需要一個型別相等性約束（即~運算子），而不是:~:型別。你像這樣使用它：
foo :: Int ~ Int => () -- compiles fine
foo = ()
bar :: Int ~ Bool => () -- does technically compile
bar = ()
bar編譯只是因為在具有約束的函式的主體中假定了約束。但是任何呼叫 的嘗試都bar需要編譯器能夠證明約束才能編譯呼叫。所以這失敗了：
baz :: ()
baz = bar
:~:但是，它不是一個約束（它不在=>型別中箭頭的左側），而是一個普通型別。a :~: b是用作運行時證明型別a等于型別的值的型別b。如果實際上它們不相等，那么您的程式在您表達型別之前不會編譯失敗a :~: b；相反，您將無法實際提出該型別的值（除了底部）。
尤其a :~: b是具有資料建構式的型別：Refl. 要有效地使用它，您通常需要 aa :~: b作為引數。然后對其進行模式匹配。在模式匹配的范圍內（即case陳述句的主體），編譯器將使用兩種型別相等的假設。由于對底部值的模式匹配永遠不會成功（它可能會拋出例外，或者它可能永遠計算），因此您始終可以提供底部作為“證明”，a :~: b這實際上不會導致大問題；你可以對編譯器撒謊，但它永遠不會執行依賴于你撒謊的代碼。
與 OP 中的示例相對應的示例是：
foo :: Int :~: Int -> ()
foo proof
= case proof of
Refl -> ()
bar :: Int :~: Bool -> ()
bar proof
= case proof of
Refl -> ()
bar can exist even though it needs an impossible proof. We can even call bar with something like bar undefined, making use of the bottom value in the type Int :~: Bool. This won't be detected as an error at compile time, but it will throw a runtime exception (if it's actually evaluated; lazy evaluation might avoid the error). Whereas foo can simply be called with foo Refl.
:~: (and ~) is of course much more usefully used when the two types are (or contain) variables, rather than simple concrete types like Int and Bool. It's also frequently combined with something like Maybe so you have a way of expressing when the types are not proven to be equal. A slightly less trivial example would be:
strange :: Maybe (a :~: b) -> a -> b -> [a]
strange Nothing x _ = [x]
strange (Just Refl) x y
= [x, y]
strange takes a maybe-proof that the types a and b are equal, and a value of each. If the maybe is Nothing, then the types might not be equal, so we can only put x in the list of a. If we get Just Refl, however, then a and b are actually the same type (inside the pattern match only!), so it's valid to put x and y in the same list.
But this does show a feature of :~: that cannot be achieved with ~. We can still call strange even when we want to pass it two values of different types; we just in that case are forced to pass Nothing as the first value (or Just undefined, but that won't get us anything useful). It allows us to write code that contemplates that a and b could be equal, without forcing a compilation failure if they actually aren't. Whereas a ~ b (in the constraints) would only allow us to require that they definitely are equal, and provably so at compile time.
1 Where "normal type" means a member of the kind Type AKA *.
轉載請註明出處，本文鏈接：https://www.uj5u.com/ruanti/445372.html
下一篇：計算自定義資料的長度