带有Haskell约束的不安全蕴含

Question

我正在使用约束包（用于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)

因为类型族不是“is element of”语句的归纳定义（就像在agda中一样）。我很确定，在GADT可升级到类型级别之前，无法用数据类型表示列表成员身份。

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

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

怪异，但它的工作。我可以在蕴含物上进行图案匹配来得到我需要的东西。我想知道的是它是否会导致程序崩溃。它似乎不能，因为un安全CoerceConstraint定义为：

unsafeCoerceConstraint = unsafeCoerce refl

在GHC中，类型级别在运行时被省略。我想我应该检查一下，确保这样做没问题。

#编辑

由于还没有人给出解释，我想我应该把这个问题扩大一点。在我创造的不安全的环境中，我只期待一个类型的家庭。如果我做了一些涉及打字字典的事情，而不是像这样：

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

我认为这几乎肯定会导致SEG故障。这是真的吗？如果是的话，是什么让它与原来的不同呢？

---编辑2---

我只是想提供一点背景知识来解释我为什么对这个感兴趣。我的兴趣之一是在Haskell中对关系代数进行可用的编码。我认为，无论您如何定义函数来处理类型级列表，都会有一些明显的事情没有得到正确的证明。例如，我之前遇到的一个约束（对于半连接）看起来像这样（这是来自内存，所以可能不准确）：

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

所以，（对一个人来说）很明显，如果我取两个集合的并集，它包含一个元素x，这个元素在中是，但我不确定约束求解者是否有可能合法地说服这一点。这就是我玩这个把戏的动机。我创建包含来欺骗约束求解器，但我不知道它是否真的安全。




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

我一直难以摆脱这个问题。这里有一种方法可以使用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中是这样。