haskell - Data.Typeable.cast 到现有类型

Question

所以这是我的对象系统传奇的延续(part 1，part 2)。

这部分基本上归结为以下内容。

{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE KindSignatures #-}

import Data.Typeable
import GHC.Exts (Constraint)

data Obj (cls :: * -> Constraint) = forall o. (cls o, Typeable o) => Obj o

downcast :: Obj a -> Maybe (Obj b)
downcast (Obj x) = do
                     cx <- cast x
                     return $ Obj cx

downcast 的定义失败并出现此错误:

• Could not deduce: b o0 arising from a use of ‘Obj’
  from the context: (a o, Typeable o)
    bound by a pattern with constructor:
               Obj :: forall (cls :: * -> Constraint) o.
                      (cls o, Typeable o) =>
                      o -> Obj cls,
             in an equation for ‘downcast’
    at downcast.hs:12:11-15
• In the second argument of ‘($)’, namely ‘Obj cx’
  In a stmt of a 'do' block: return $ Obj cx
  In the expression:
    do cx <- cast x
       return $ Obj cx
• Relevant bindings include
    cx :: o0 (bound at moo.hs:13:22)
    downcast :: Obj a -> Maybe (Obj b) (bound at downcast.hs:12:1)

我不太明白为什么会出现这个错误:( 可以修复吗？

Answer 1

当您的 Haskell 被翻译成 GHC Core 时，类(以及随之而来的逻辑编程构造，如蕴涵)已经无处可寻。它们被编译器转换为字典传递代码——每个实例成为一个记录(一个常规值)并且每个方法成为该记录的一个成员。 (有关更多细节，请参阅 a previous answer of mine。)

所以一个打包约束的构造函数，

data Obj c where  -- I'm using GADT syntax
    Obj :: c a => a -> Obj c

在运行时确实由常规产品类型表示，

data Obj c where
    Obj :: c a -> a -> Obj c

其中 c a 字段是表示 c a 实例的运行时方法字典。

在运行时将 Obj c 向下转换为 Obj c'，即使您有办法测试具体的 a 是c 和 c' 的实例，您仍然需要以某种方式为 c' 合成字典。由于 c' 通常包含比 c 更多的方法，这相当于要求计算机为您编写程序。

---

As David mentioned in the comments ，我认为您最好的选择是在封闭世界的假设下将有关特定类层次结构的知识构建到您的运行时系统中。如果你有一个可以查询实例实际运行时间的 oracle dictionary ,

oracle :: MonadRuntime m => TypeRep a -> TypeRep c -> m (Maybe (Dict (c a)))

然后你可以写cast(有一些不舒服的类型争论):

data Obj c where
    Obj :: c a => TypeRep a -> a -> Obj c

cast :: forall c c' m. (MonadRuntime m, Typeable c') => Obj c -> m (Maybe (Obj c'))
cast (Obj tr x) = do
    mdict <- oracle tr (typeRep @c')
    case mdict of
        Just Dict -> return (Just (Obj tr x))
        Nothing -> return Nothing

请注意，此cast 实际上允许您(尝试)将对象的接口(interface)更改为任何 其他接口(interface)，而不仅仅是那些从对象的静态类型派生的接口(interface)。 (在 C# 中，您可以通过向上转换为 object 然后向下转换来执行此操作。)您可以通过要求 entailment 来防止这种情况发生。在 cast 的上下文中:

cast :: forall c c' m. (MonadRuntime m, Typeable c', Class c c') => Obj c -> m (Maybe (Obj c'))

(当然，这个蕴涵实际上不会在运行时使用。)

---

挑战在于实现oracle!我认为这将是那些不好玩的挑战之一，所以我只会给你一两点建议。

您的Runtime monad 可能是某种Reader，带有查找表映射(TypeRep)as 和 c 到字典。 a 和 c 需要进行存在量化，以便将它们存储在异构列表中。

data TableEntry where
    TableEntry :: c a => TypeRep c -> TypeRep a -> TableEntry

type MonadRuntime = MonadReader [TableEntry]

然后oracle需要查找匹配类/类型对的TableEntry，然后打开existential，通过拆开typeRep建立类型相等s，并返回 Just Dict。 (特别是这部分听起来像是编写代码的噩梦。)

在运行 MonadRuntime 程序之前，您需要构建包含程序关心的所有实例的 Table。

table = [
    TableEntry (typeRep @Ord) (typeRep @Int),
    TableEntry (typeRep @Eq) (typeRep @Bool)
    ]

---

总而言之，我不明白这有什么值得头疼的。类型类从根本上不同于 OO 类(它们甚至不太像 OO 接口(interface))，因此很难使用它们来为 OO 类建模也就不足为奇了。