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论文, GHC7的类型推断应该在"类型类+ GADT +类型族"的存在下起作用.在这方面,我有两个问题:

1. 为什么类型推断不适用于上面的例子(我使用的是GHC7)？
2. 什么是涉及GADT和类型函数(append如上所述)的非平凡示例,GHC可以推断出类型？

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)