GADT中De Bruijn索引变量的平等性

Question

我有一个问题,说服编译器两个De Bruijn索引变量是相同的.我有以下深度嵌入DSL,De Bruijn索引代码基于Manuel Chakravarty 将HOAS术语GADT转换为de Bruijn术语GADT:

{-# LANGUAGE GADTs #-}

data Ix env t where
    ZeroIx ::             Ix (env, t) t
    SuccIx :: Ix env t -> Ix (env, s) t

-- | Heterogeneous equality for 'Ix'. Note, this only ensures that
-- the indices are equal as integers; it does not ensure that their
-- type environments are equal. (Though we do require that the types
-- of the values they're bound to to be the same, i.e. @(a ~ a)@.)
eqIx :: Ix l a -> Ix r a -> Bool
eqIx ZeroIx     ZeroIx     = True
eqIx (SuccIx m) (SuccIx n) = eqIx m n
eqIx _          _          = False

data Dist env e where
    Var        :: Ix env e -> Dist env e
    --- XXX: What should Let look like?
    ConcatMap  :: (a -> [b]) -> Dist env [a] -> Dist env [b]
    -- For sibling fusion:
    ConcatMap2 :: (a -> ([b], [c])) -> Dist env [a] -> Dist env ([b], [c])
    Fst        :: Dist env ([a], [b]) -> Dist env [a]
    Snd        :: Dist env ([a], [b]) -> Dist env [b]

fuse :: Dist env e1 -> Dist env e2 -> (Dist env e1, Dist env e2)
fuse (ConcatMap f v@(Var x)) (ConcatMap g (Var y))
    | eqIx x y = let e = ConcatMap2 (f `mapBoth` g) v
                 in (Fst e, Snd e)  -- XXX: Doesn't type check.
fuse e1 e2 = (e1, e2)

mapBoth :: (a -> [b]) -> (a -> [c]) -> a -> ([b], [c])
mapBoth = undefined

该函数fuse试图实现兄弟融合(一种元组优化).我需要对两个Var相同的模式匹配.虽然我可以比较索引本身,但我还需要说服编译器这些索引所在的键入环境是相同的,因此它们映射到相同类型的值.我有一种感觉,这可以通过添加Let构造函数和模式匹配来解决,但我不清楚如何.这是类型错误的删节版本:

/tmp/Minimal.hs:27:14:
    Could not deduce (a1 ~ a)
    from the context (e1 ~ [b])
      bound by a pattern with constructor
                 ConcatMap :: forall env a b.
                              (a -> [b]) -> Dist env [a] -> Dist env [b],
               in an equation for ‘fuse’
      at /tmp/Minimal.hs:26:7-27
    or from (e2 ~ [b1])
      bound by a pattern with constructor
                 ConcatMap :: forall env a b.
                              (a -> [b]) -> Dist env [a] -> Dist env [b],
               in an equation for ‘fuse’
      at /tmp/Minimal.hs:26:31-49
      ‘a1’ is a rigid type variable bound by
           a pattern with constructor
             ConcatMap :: forall env a b.
                          (a -> [b]) -> Dist env [a] -> Dist env [b],
           in an equation for ‘fuse’
           at /tmp/Minimal.hs:26:31
      ‘a’ is a rigid type variable bound by
          a pattern with constructor
            ConcatMap :: forall env a b.
                         (a -> [b]) -> Dist env [a] -> Dist env [b],
          in an equation for ‘fuse’
          at /tmp/Minimal.hs:26:7
    Expected type: Ix env [a]
      Actual type: Ix env [a1]

如何在两个相同的变量上进行模式匹配？

Answer 1

我可以通过两个相对简单的更改来进行代码类型检查.但是我不完全确定它们是否真的在整个代码的更广泛的环境中有效.

首先,类型eqIx不会利用您已有的知识,即env当您调用参数时已知参数相同.我们可以将它改为此而且它仍然会进行类型检查 - 即我们假设环境是相同的但变量类型可能不是.

eqIx :: Ix env a -> Ix env b -> Bool

在这个改变之后,重要的是eqIx告诉我们两个变量的类型实际上是相同的.但是只返回一个Bool我们将其隐藏在编译器中.如果我们返回标准类型级别的"相同见证",我们可以传播这些信息:

data EqWitness a b where
    IsEq :: EqWitness a a

eqIx :: Ix env a -> Ix env b -> Maybe (EqWitness a b)
eqIx ZeroIx     ZeroIx     = Just IsEq
eqIx (SuccIx m) (SuccIx n) = eqIx m n
eqIx _          _          = Nothing

(某些EqWitness地方可能存在一些标准类型的hackage)

现在我们可以PatternGuards稍微添加和更改您的呼叫站点,以便在eqIx成功时提取相同的见证.这使得相关案例正文中的类型检查器可以使用相等性:

fuse :: Dist env e1 -> Dist env e2 -> (Dist env e1, Dist env e2)
fuse (ConcatMap f v@(Var x)) (ConcatMap g (Var y))
    | Just IsEq <- eqIx x y
               = let e = ConcatMap2 (f `mapBoth` g) v
                 in (Fst e, Snd e)
fuse e1 e2 = (e1, e2)