haskell - 依赖种类签名中的类型族评估

Question

考虑以下:

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) = Length xs

鉴于所有这些，似乎应该可以定义一个类型级别函数，该函数将类型级别列表和小于其长度的索引映射到存储在相​​应位置的类型。

type Get :: forall k. forall (l :: [k]) -> Fin (Length l) -> k
type family Get l i
  where
  Get (x ': xs) 'FZ = x
  Get (_ ': xs) ('FS i) = Get xs i

但这会因以下错误而爆炸:

• Illegal type synonym family application ‘Length @k xs’ in instance:
    Get @k ((':) @k x xs) ('FZ @(Length @k xs))
• In the equations for closed type family ‘Get’
  In the type family declaration for ‘Get’

所以看来GHC对 Length的评价不太满意在从属种类签名中键入 family。有什么方法可以让 GHC 相信定义这样的函数是可以的？或者，是否有一些解决方法可以用来描述索引到类型级别列表的相关操作？

Answer 1

我个人不知道有什么方法可以使这项工作(希望其他人是)。也就是说，如果我们吸收 Length，我们可以解决在种类签名中评估类型族的需要。进入定义Fin .换句话说，我们可以为镜像 Fin (Length l) 的列表创建一个特殊用途的索引类型。 :

type Index :: [k] -> Type
data Index xs
  where
  Head :: Index (x ': xs)
  Next :: Index xs -> Index (x ': xs)

现在我们可以用它来写 Get 的变体:

type Get :: forall k. forall (l :: [k]) -> Index l -> k
type family Get l i
  where
  Get (x ': xs) 'Head = x
  Get (_ ': xs) ('Next i) = Get xs i

这似乎有效:

type Test = Get '[Int, String, Bool] (Next (Next Head))

> :k! Test
Test :: *
= Bool

这种方法有点粗俗和反成分，但我认为它有效。