haskell - 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 的类型推断应该在存在“类型类 + GADT + 类型族”的情况下工作。在此背景下，我有两个问题:

1. 为什么类型推断对于上面的示例不起作用(我使用的是 GHC7)？
2. 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)