能否用Typenats实现向量拼接？解决GHC报错及移除UndecidableInstances

现有代码定义 #

{-# LANGUAGE TypeFamilies, DataKinds, UndecidableInstances #-}
data VList f a = a :. (f a) deriving (Show,Eq,Ord,Functor,Foldable,Traversable)
infixr 5 :.
type family Vec n where
  Vec 0 = End
  Vec n = VList (Vec (n - 1))

目标拼接函数 #

尝试实现的向量拼接函数：

append :: Vec m a -> Vec n a -> Vec (m + n) a
append End a = a
append (a :. b) c = a :. append b c

GHC报错信息 #

• Couldn't match type: VList (Vec m0) a
  with: End a
  Expected: Vec m a
  Actual: VList (Vec m0) a
• In the pattern: a :. b
  In an equation for `append': append (a :. b) c = a :. append b c
• Relevant bindings include
  append :: Vec m a -> Vec n a -> Vec (m + n) a
  (bound at Vector.hs:36:1)
  |
  37 | append (a :. b) c = a :. append b c

核心疑问 #

1. 推测GHC无法识别Vec类型族的全量情况，导致Vec m a与VList类型匹配失败，该如何修复？
2. 如何移除UndecidableInstances编译指令？

一、修复append的类型匹配错误 #

GHC无法自动关联Vec m a和VList (Vec (m-1)) a的等价性——类型族的展开逻辑不会直接被模式匹配利用，需要通过类型类的归纳实例给GHC提供明确的结构证据。另外代码中缺失了End类型的定义，这是基础前提。

完整修正代码 #

{-# LANGUAGE TypeFamilies, DataKinds, TypeOperators #-}
-- 补充End数据类型定义
data End a = End deriving (Show, Eq, Ord)
data VList f a = a :. (f a) deriving (Show,Eq,Ord,Functor,Foldable,Traversable)
infixr 5 :.

type family Vec n where
  Vec 0 = End
  Vec n = VList (Vec (n - 1))

-- 借助类型类实现带类型推导的append
class Append m n where
  append :: Vec m a -> Vec n a -> Vec (m + n) a

-- 基例：空向量拼接直接返回另一个向量
instance Append 0 n where
  append End ys = ys

-- 归纳例：非空向量拆头递归拼接
instance Append m n => Append (m + 1) n where
  append (x :. xs) ys = x :. append xs ys

原理说明 #

• 通过Append类型类的实例链，让GHC逐步推导Vec m的结构：当m>0时，Vec m必然是VList (Vec (m-1))，因此可以安全匹配:.模式；
• 类型级加法(+)由GHC内置的Nat类型支持，无需额外定义（若导入GHC.TypeLits可直接使用）。

二、移除UndecidableInstances #

原代码需要该扩展是因为GHC最初无法确认Vec类型族的递归终止性，但只要保证类型族是结构递归（每次递归的Nat参数严格减小），GHC就能自动判定终止性，无需该扩展。

修正后的代码满足终止条件：

• Vec的递归是对Nat参数的递减操作（n-1），完全符合终止规则；
• Append的实例基于Nat的结构归纳，没有违反GHC的实例判定逻辑。

因此可以直接删除UndecidableInstances编译指令，仅保留TypeFamilies, DataKinds, TypeOperators三个必要扩展。

内容的提问来源于stack exchange，提问作者Ashok Kimmel