具有 Haskell 约束的不安全内涵问题

Question

我正在尝试使用 constraints 包（用于 GHC Haskell）。我有一个类型族，用于确定类型级列表是否包含元素：

type family HasElem (x :: k) (xs :: [k]) where
  HasElem x '[] = False                                                                               
  HasElem x (x ': xs) = True                                                                          
  HasElem x (y ': xs) = HasElem x xs

这个可以运行，但是它没有给我知道的一件事

HasElem x xs   entails   HasElem x (y ': xs)

因为类型族不是“属于”语句的归纳定义（就像在Agda中会有的那样）。在GADTs可以提升到类型级别之前，我相信没有办法使用数据类型表示列表成员资格。

所以，我使用了constraints包来编写这个：

containerEntailsLarger :: Proxy x -> Proxy xs -> Proxy b -> (HasElem x xs ~ True) :- (HasElem x (b ': xs) ~ True)
containerEntailsLarger _ _ _ = unsafeCoerceConstraint

有点诡异，但它很有效。我可以在蕴含中进行模式匹配以获取所需内容。我想知道的是它是否会导致程序崩溃。似乎不可能，因为unsafeCoerceConstraint的定义如下：

unsafeCoerceConstraint = unsafeCoerce refl

在 GHC 中，类型级别在运行时被省略。虽然我想检查一下，以确保这样做是可以的。

--- 编辑 ---

由于还没有人给出解释，所以我想扩展一下问题。在我创建的不安全隐含中，我只期望有一个类型族。如果我像下面这样涉及到类型类字典，会怎么样：

badEntailment :: Proxy a -> (Show a) :- (Ord a)
badEntailment _ = unsafeCoerceConstraint

我假设这几乎肯定会导致segfault。这是真的吗？如果是，它与原始内容有何不同？

--- 编辑2 ---

我想提供一些背景，解释我为什么对此感兴趣。我之一的兴趣是在Haskell中制作可用的关系代数编码。我认为，无论您如何定义函数来处理类型级别的列表，都会有明显的未正确证明的事情。例如，我以前遇到的一个约束条件（用于半连接）看起来像这样（这是从记忆中得出的，因此可能不完全准确）：

semijoin :: ( GetOverlap as bs ~ Overlap inAs inBoth inBs
            , HasElem x as, HasElem x (inAs ++ inBoth ++ inBs)) => ...

所以，对于一个人来说，如果我取两个集合的并集，其中包含了一个元素 x 也在 as 中，这应该是显而易见的。但我不确定是否能够让约束求解器合法地相信这一点。这就是我使用这种技巧的动机。我创建蕴含关系来欺骗约束求解器，但我不知道这是否真的安全可靠。

- Andrew Thaddeus Martin

---

如果你不知道某个东西在联合体 as 和 bs 中的位置，知道它在联合体中会有什么帮助呢？我很想看一些实际的代码。 - dfeuer

如果你只想知道某个元素是否存在，那么你所做的是正确的。但如果你想要字段的第一个匹配项，那么就会有问题。例如，如果它返回的不是布尔值而是HList中的偏移量，那么你将无法使用unsafeCoerceConstraint。 - Edward Kmett

@EdwardKMETT，谢谢。这基本上回答了我关于这种方法的安全性的问题。 - Andrew Thaddeus Martin

Answer 1

我不知道这是否符合您的其他需求，但它完成了这个特定的目的。对于字体家族，我自己也不太擅长，所以我不清楚您的字体家族实际可用于哪些方面。

{-# LANGUAGE ...., UndecidableInstances #-}
type family Or (x :: Bool) (y :: Bool) :: Bool where
  Or 'True x = 'True
  Or x 'True = 'True
  Or x y = 'False

type family Is (x :: k) (y :: k) where
  Is x x = 'True
  Is x y = 'False

type family HasElem (x :: k) (xs :: [k]) :: Bool where
  HasElem x '[] = 'False
  HasElem x (y ': z) = Or (Is x y) (HasElem x z)

containerEntailsLarger :: proxy1 x -> proxy2 xs -> proxy3 b ->
                          (HasElem x xs ~ 'True) :- (HasElem x (b ': xs) ~ 'True)
containerEntailsLarger _p1 _p2 _p3 = Sub Dict

使用GADTs的方法

我一直在苦恼如何解决这个问题。这里介绍了一种使用GADT的方法，可以在使用类型族和类来获得良好接口的同时获得良好证据。

-- Lots of extensions; I don't think I use ScopedTypeVariables,
-- but I include it as a matter of principle to avoid getting
-- confused.
{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, UndecidableInstances #-}
{-# LANGUAGE TypeFamilies, TypeOperators #-}
{-# LANGUAGE DataKinds, PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE GADTs #-}

-- Some natural numbers
data Nat = Z | S Nat deriving (Eq, Ord, Show)

-- Evidence that a type is in a list of types
data ElemG :: k -> [k] -> * where
  Here :: ElemG x (x ': xs)
  There :: ElemG x xs -> ElemG x (y ': xs)
deriving instance Show (ElemG x xs)

-- Take `ElemG` to the class level.
class ElemGC (x :: k) (xs :: [k]) where
  elemG :: proxy1 x -> proxy2 xs -> ElemG x xs

-- There doesn't seem to be a way to instantiate ElemGC
-- directly without overlap, but we can do it via another class.
instance ElemGC' n x xs => ElemGC x xs where
  elemG = elemG'

type family First (x :: k) (xs :: [k]) :: Nat where
  First x (x ': xs) = 'Z
  First x (y ': ys) = 'S (First x ys)

class First x xs ~ n => ElemGC' (n :: Nat) (x :: k) (xs :: [k]) where
  elemG' :: proxy1 x -> proxy2 xs -> ElemG x xs

instance ElemGC' 'Z x (x ': xs) where
  elemG' _p1 _p2 = Here

instance (ElemGC' n x ys, First x (y ': ys) ~ 'S n) => ElemGC' ('S n) x (y ': ys) where
  elemG' p1 _p2 = There (elemG' p1 Proxy)

这实际上似乎有效，至少在简单的情况下：

*Hello> elemG (Proxy :: Proxy Int) (Proxy :: Proxy '[Int, Char])
Here

*Hello> elemG (Proxy :: Proxy Int) (Proxy :: Proxy '[Char, Int, Int])
There Here

*Hello> elemG (Proxy :: Proxy Int) (Proxy :: Proxy '[Char, Integer, Int])
There (There Here)

虽然不能支持您所需的精确蕴含关系，但我认为ElemGC'递归情况可能是带有如此信息约束条件下最接近您所需的。至少在GHC 7.10中是这样。

- dfeuer

---

这绝对是解决这个问题的正确方法。 - Edward Kmett

谢谢，@EdwardKMETT。您认为我添加的GADT方法如何？有更好的方法吗？我不是很喜欢First x (y ': ys) ~ Just (S n)这个约束条件，因为它没有基于First x ys ~ Just n来构建，但我还没有看到其他的解决方法。 - dfeuer

不错。我最近读了hasochism论文，所以这对我来说是一个很好的例子。只是为了确保我正确理解，ElemGC类（在您的GHCi示例中未使用）是否用于隐式创建ElemG（就像hasochism论文中的NATTY一样）？ - Andrew Thaddeus Martin

@AndrewThaddeusMartin，它在示例中被使用！我使用了 elemG 函数。是的，它隐式地创建了一个 ElemG。我还没有阅读这篇论文，但我想我应该去看看。 - dfeuer

@EdwardKMETT，我刚刚意识到新的OVERLAPS和OVERLAPPABLE相对于旧的OverlappingInstances在这方面有多大提升。谢谢！ - dfeuer