GHC 无法在存在 GADT 和类型族的情况下推断类型

Question

我有一个简单的长度索引向量类型和一个基于长度索引向量的 append 函数：

{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}

module LengthIndexedList where

  data Zero
  data Succ a

  type family Plus (a :: *) (b :: *) :: *
  type instance Plus Zero b = b
  type instance Plus (Succ a) b = Succ (Plus a b)

  data Vec :: * -> * -> * where
    VNil :: Vec a Zero
    VCons :: a -> Vec a n -> Vec a (Succ n)

  -- If you remove the following type annotation, type inference
  -- fails.
  -- append :: Vec a n1 -> Vec a n2 -> Vec a (Plus n1 n2)
  append v1 v2 = case v1 of
    VNil -> v2
    (VCons x xs) -> VCons x (append xs v2)

编译失败，因为 GHC 无法推断 append 函数的类型。我知道在存在 GADT 和类型族的情况下类型推断很棘手，部分原因是多态递归。尽管如此，根据 Vytiniotis 等人的 JFP paper GHC7 的类型推断应该在存在 "type classes + GADTs + type families" 的情况下工作。在这种情况下，我有两个问题：

为什么类型推断不适用于上述示例（我使用的是 GHC7）？
GHC 可以推断类型的涉及 GADT 和类型函数（如上面的 append）的重要示例是什么？

Answer 1

我只读了一滴纸，这让我头疼，但我相信问题几乎肯定是由类型家族引起的。你有一个函数类型

Vec a n1 -> Vec a n2 -> Vec a (Plus n1 n2)

但原则上类型推断无法识别这一点。我可以在您的代码中添加第二类家族，

type family Plus' (a :: *) (b :: *) :: *
type instance Plus' Zero b = b
type instance Plus' (Succ a) b = Succ (Plus' a b)

看起来很像 Plus，但名称不同。推理无法判断你想要 Plus 还是 Plus'。推理从不选择，也从不让自己陷入可能不得不选择的位置（没有一些像 IncoherentInstances 这样非常不愉快的事情）。因此，只有在 没有 Plus 存在 的情况下推论才有效。我对类型检查背后的理论知之甚少，但我不认为可以凭空推断出类型族。

我相信这篇论文的意思是，推理在所有这些东西存在的情况下仍然有用，并且在没有它们的情况下仍然一样好。例如，您可以编写使用您的 append 函数并且没有类型签名的代码：

append3 a b c = a `append` b `append` c

额外的奖励说明：DataKinds 和封闭类型族使一些代码更容易理解。我会这样写你的代码：

data Nat = Zero | Succ Nat

type family Plus (a :: Nat) (b :: Nat) :: Nat where
  Plus Zero b = b
  Plus (Succ a) b = Succ (Plus a b)

data Vec :: * -> Nat -> * where
  VNil :: Vec a Zero
  VCons :: a -> Vec a n -> Vec a (Succ n)

Answer 2

假设我们有以下定义：

append VNil         v2 = v2
append (VCons x xs) v2 = VCons x (append xs v2)

从定义中可以明显看出：

append :: Vec a n -> Vec a m -> Vec a p

好像你不介意Vec中的Nat索引一样，它是HM类型，一切都应该简单。

然后我们可以写出 n、m 和 p 的约束条件：

appendIndex Zero m ~ m                          -- from VNil case
appendIndex (Succ n) m ~ Succ (appendIndex n m) -- from VCons case

我没看过JFP论文，但我认为OutsideIn不能解决这个约束。它必须能够在没有任何上下文的情况下解决它们，即知道某处是 Plus.

它可以用类似（伪语法，类型 lambda）的方式解决约束：

append :: Vec a n -> Vec a m -> Vec a (rec f (λ n → case n of { Zero -> m ; Succ n' -> Succ (f n') }))

并且使用更智能的编译器，当使用函数时，plus 的匿名定义可以与 Plus 或 Plus' 统一。

值得从更简单的论文中获取建议：FPH: First-class Polymorphism for Haskell,，尤其是对于顶级定义：

如果type是HM就可以推断
其他类型（RankN）需要标注，无法推断

至于重要的例子，我猜不可能有一个，因为 GHC 类型的语言没有（甚至非递归的）匿名类型函数 (AFAIK)。

即使是非常简单的（非递归类型）示例也失败了

data NonEmpty :: * -> Bool -> * where
  VNil :: NonEmpty a False
  VCons :: a -> NonEmpty a b -> NonEmpty a True

append VNil         v2 = v2
append (VCons x xs) v2 = VCons x (append xs v2)

因为它必须推断

appendIndex True b = True
appendIndex False b = b

在类型级别上本质上是 ||。 GHC 不支持（还？）功能提升。所以你甚至不能写

append :: NonEmpty a x -> NonEmpty b y -> NonEmpty b (x '|| y)

但是在使之成为可能方面取得了一些进展http://www.cis.upenn.edu/~eir/papers/2014/promotion/promotion.pdf

GHC 无法在存在 GADT 和类型族的情况下推断类型

GHC could not infer types in presence of GADTs and Type Families

haskell

types

ghc