Haskell依赖Kind签名中类型族求值报错，如何实现类型级列表索引？

错误根源 #

GHC在匹配闭合类型族的子句时，不会对出现在参数位置的类型族应用进行规约求值。你原签名中Fin (Length l)把索引i的Kind和Length类型族强制绑定，当你写子句Get (x ': xs) 'FZ时，FZ的Kind是Fin ('S m)，GHC需要验证Length (x ': xs) ~ 'S m，但Length (x ': xs)本身是类型族应用，属于不可匹配的模式，所以直接抛出你遇到的错误。

另外你给出的Length类型族存在笔误：递归分支Length (_ ': xs) = Length xs会导致所有列表的长度计算结果都为'Z，需要修改为Length (_ ': xs) = 'S (Length xs)才能正确计算长度。

可行方案 #

方案1：松绑Get的类型签名，使用时加相等约束

你可以把Get的签名写得更通用，不在签名里强制要求索引的Kind必须是Fin (Length l)，在外部使用时通过相等约束保证索引合法性即可，可编译代码如下：

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}

type Nat :: Type
data Nat = Z | S Nat

type Fin :: Nat -> Type
data Fin n
  where
  FZ :: Fin ('S n)
  FS :: Fin n -> Fin ('S n)

type Length :: [k] -> Nat
type family Length xs
  where
  Length '[] = 'Z
  Length (_ ': xs) = 'S (Length xs) -- 修正笔误

-- 松绑索引的Kind约束，不与Length绑定
type Get :: forall k. [k] -> forall (n :: Nat). Fin n -> k
type family Get l i
  where
  Get (x ': xs) 'FZ = x
  Get (_ ': xs) ('FS i) = Get xs i

使用示例：

type ExampleList = '[Int, Bool, String]
type ExampleIdx = 'FZ :: Fin (Length ExampleList)
type Result = Get ExampleList ExampleIdx -- Result的类型等价于Int

方案2：使用长度索引的向量（Vec）替代普通类型级列表

如果你需要在Kind层面强约束索引合法性、避免运行时越界，最符合依赖类型习惯的方案是直接用带长度参数的向量类型代替普通列表，不需要额外计算Length类型族，天然匹配Fin的索引：

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}

type Nat :: Type
data Nat = Z | S Nat

type Fin :: Nat -> Type
data Fin n
  where
  FZ :: Fin ('S n)
  FS :: Fin n -> Fin ('S n)

-- 长度索引的向量类型，天然携带长度Kind参数
type Vec :: Nat -> Type -> Type
data Vec n a where
  VNil :: Vec 'Z a
  VCons :: a -> Vec n a -> Vec ('S n) a

-- Get定义无任何冲突，Kind层面天然保证索引合法
type Get :: forall a n. Vec n a -> Fin n -> a
type family Get v i where
  Get ('VCons x xs) 'FZ = x
  Get ('VCons _ xs) ('FS i) = Get xs i

这种方案不需要额外的相等约束，也不会出现类型族匹配冲突，是更推荐的工程实践方案。

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