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)

因为类型族不是"is element of"语句的归纳定义(就像你在agda中所拥有的那样).我很确定,在GADT可以升级到类型级别之前,没有办法用数据类型表达列表成员资格.

所以,我用这个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

我认为这几乎肯定会导致段错误.这是真的？如果是这样,是什么让它与原版不同？

---编辑2 ---

我只是想提供一些背景知识,为什么我对此感兴趣.我的兴趣之一是在Haskell中对关系代数进行可用的编码.我认为无论你如何定义函数来处理类型级别列表,都会有明显的事情没有被证明是正确的.例如,我之前拥有的约束(对于半连接)看起来像这样(这是来自内存,所以它可能不完全):

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

所以,它应该是显而易见的(一个人),如果我走的两套工会,它包含的元素x,这是在as,但我不知道它是可能的合法说服这个约束求解.所以,这是我做这个技巧的动机.我创建了欺骗约束解算器的蕴涵,但我不知道它是否真的安全.

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的方法

我一直无法解决这个问题.这是一种使用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中如此.