在依赖类型签名中键入家庭评估

Question

考虑以下：

\n

type Nat :: Type\ndata Nat = Z | S Nat\n\ntype Fin :: Nat -> Type\ndata Fin n\n  where\n  FZ :: Fin (\'S n)\n  FS :: Fin n -> Fin (\'S n)\n\ntype Length :: [k] -> Nat\ntype family Length xs\n  where\n  Length \'[] = \'Z\n  Length (_ \': xs) = Length xs\n

\n

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

\n

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

\n

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

\n

\xe2\x80\xa2 Illegal type synonym family application \xe2\x80\x98Length @k xs\xe2\x80\x99 in instance:\n    Get @k ((\':) @k x xs) (\'FZ @(Length @k xs))\n\xe2\x80\xa2 In the equations for closed type family \xe2\x80\x98Get\xe2\x80\x99\n  In the type family declaration for \xe2\x80\x98Get\xe2\x80\x99\n

\n

Length因此，GHC 似乎对依赖类型签名中类型系列的评估不满意。有什么方法可以让 GHC 相信定义这样一个函数是可以的吗？或者，是否有一些解决方法可以用来描述索引到类型级别列表的依赖类型操作？

\n

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

这种方法有点粗俗和反组合，但我认为它是有效的。