第一次尝试
很难使这个问题简洁,但提供一个最小的例子,假设我有这种类型:
{-# 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的一些技术来实现我需要作为类型级函数的操作。但是,我对使用存在主义和 GADT 比较陌生,我很想知道是否可以找到解决方案。所以,如果答案是否定的,我非常感谢讨论这个问题究竟在哪里达到了这些功能的限制,以及推动适当的技术、HList 或其他方式。