haskell - 我可以静态拒绝存在类型的不同实例吗？

Question

第一次尝试

很难使这个问题简洁，但提供一个最小的例子，假设我有这种类型:

{-# LANGUAGE GADTs #-}
data Val where
  Val :: Eq a => a -> Val

这种类型让我愉快地构建了以下异构列表:

l = [Val 5, Val True, Val "Hello!"]

但是，唉，当我写下 Eq例如，事情出错了:

instance Eq Val where
  (Val x) == (Val y) = x == y -- type error

啊，所以我们Could not deduce (a1 ~ a) .非常正确;定义中没有任何内容说 x和 y必须是同一类型。事实上，重点是允许它们不同的可能性。

第二次尝试

让我们带Data.Typeable混合，并且只有在它们碰巧是相同类型时才尝试比较它们:

data Val2 where
  Val2 :: (Eq a, Typeable a) => a -> Val2

instance Eq Val2 where
  (Val2 x) == (Val2 y) = fromMaybe False $ (==) x <$> cast y

这很不错。如 x和 y是相同的类型，它使用底层 Eq实例。如果它们不同，它只返回 False .但是，此检查会延迟到运行时，允许 nonsense = Val2 True == Val2 "Hello"打字检查没有投诉。

题

我意识到我在这里与依赖类型调情，但是 Haskell 类型系统是否有可能静态拒绝类似上面的内容 nonsense ，同时允许类似 sensible = Val2 True == Val2 False交还False在运行时？

我处理这个问题的次数越多，我似乎就越需要采用 HList 的一些技术。将我需要的操作实现为类型级函数。但是，我对使用existentials 和GADT 比较陌生，我很想知道是否可以找到解决方案。所以，如果答案是否定的，我非常感谢讨论这个问题到底在什么地方达到了这些功能的限制，以及对适当的技术、HList 或其他方面的插入。

Answer 1

为了根据所包含的类型做出类型检查决定，我们需要通过将其作为类型参数公开来“记住”所包含的类型。

data Val a where
  Val :: Eq a => a -> Val a

现在 Val Int和 Val Bool是不同的类型，所以我们可以很容易地强制要求只允许相同类型的比较。

instance Eq (Val a) where
  (Val x) == (Val y) = x == y

但是，由于 Val Int和 Val Bool是不同的类型，我们不能在没有附加层的情况下将它们混合在一个列表中，该层会再次“忘记”所包含的类型。

data AnyVal where
  AnyVal :: Val a -> AnyVal

-- For convenience
val :: Eq a => a -> AnyVal
val = AnyVal . Val

现在，我们可以写

[val 5, val True, val "Hello!"] :: [AnyVal]

现在应该很清楚了，您无法使用单一数据类型同时满足这两个要求，因为这样做需要同时“忘记”和“记住”所包含的类型。