haskell - eqT 而不是强制转换的用例是什么？

Question

在 Data.Typeable有一个函数转换

cast :: forall a b. (Typeable a, Typeable b) => a -> Maybe b 

和一个函数 eqT

eqT :: forall a b. (Typeable a, Typeable b) => Maybe (a :~: b) 

它们在效果和实现上似乎几乎相同，我想知道对 eqT 的描述是否有任何实际意义:提取两种类型相等的见证。

Answer 1

这很尴尬:

checkEq :: forall a b. (Typeable a, Typeable b, Eq b) => a -> a -> Maybe Bool
checkEq a a' = do
    b  <- cast @_ @b a
    b' <- cast a'
    pure (b == b')

在内部，这会检查强制转换两次，并执行两次 Maybe模式匹配。但是一旦我们完成了一个 Actor ，我们就知道另一个会成功!
这个更好:

checkEq a a' = (\Refl -> a == a') <$> eqT @a @b

一张支票，一张 Maybe模式匹配。
当您对存在进行量化时，经常会出现这种情况 Typeable数据结构中的事物，并希望对它们进行带有多个参数的操作。将类型相等性带入作用域一次(使用 Refl 模式)然后能够多次使用该相等性比重复 cast 更方便、更高效。 ing。
编辑
chi 指出，实际上可以只做一个 cast在这种情况下:

checkEq a a' = (\eq -> eq a a') <$> cast ((==) @b)
checkEq a a' = uncurry ((==) @b) <$> cast (a, a')

在一般情况下，您可以构建一个包含所有需要转换的操作或所有需要转换的值的元组。我想这并没有真正让我对其中任何一个有一个强有力的技术论据!