4

第一次尝试

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

{-# 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

这很不错。如果xy是相同类型,则使用底层Eq实例。如果它们不同,它只会返回False. 但是,此检查会延迟到运行时,从而nonsense = Val2 True == Val2 "Hello"可以毫无怨言地进行类型检查。

问题

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

我处理这个问题的次数越多,我就越需要采用HList的一些技术来实现我需要作为类型级函数的操作。但是,我对使用存在主义和 GADT 比较陌生,我很想知道是否可以找到解决方案。所以,如果答案是否定的,我非常感谢讨论这个问题究竟在哪里达到了这些功能的限制,以及推动适当的技术、HList 或其他方式。

4

2 回答 2

14

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

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

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

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

然而,由于Val IntVal 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]

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

于 2011-09-27T02:38:46.310 回答
7

因此,您需要一个允许您使用异构类型的构造函数,但您希望拒绝在编译时已知的异构类型之间的比较。如:

Val True == Val "bar"  --> type error

allSame [] = True
allSame (x:xs) = all (== x) xs

allSame [Val True, Val "bar"]  --> False

但可以肯定:

(x == y) = allSame [x,y]

所以我很确定满足这些约束的函数会违反类型系统的某些理想属性。在你看来不是这样吗?我强烈猜测“不,你不能那样做”。

于 2011-09-27T02:39:54.470 回答