在 Idris 中，所有长度都已知的双打列表的类型是什么？

Question

示例值：[[1, 2], [1]]

在这里，我知道有 2 个列表，第一个列表的长度为 2，而第二个列表的长度为 1。理想情况下，此函数将计算这些类型：

func : (n ** Vect n Nat) -> Type

但是我不知道怎么写。我很确定它与依赖对有关，但我不确定如何写它。

澄清一下，我知道可以简单地使用 (n ** Vect n (p ** Vect p Double)) 作为示例值的类型。然而，n 只限制列表的数量，而不是它们的元素的数量，因为在列表内部，p 可以是任何东西。我很可能需要一些东西，其中依赖对的第一个元素是 长度向量 ，而不仅仅是列表的数量。所以类似于 (Vect n Nat ** Vect n (Vect m Double))--其中每个 m 是第一个向量的对应元素。

Answer 1

您可以定义一个新的向量类型，它在每个位置可能包含索引类型的不同索引元素：

import Prelude
import Data.Vect

-- heterogeneously indexed vector
data IVect : Vect n ix -> (ix -> Type) -> Type where
  Nil  : IVect Nil b
  (::) : b i -> IVect is b -> IVect (i :: is) b

-- of which a special case is a vector of vectors
VVect : Vect n Nat -> Type -> Type
VVect is a = IVect is (flip Vect a)

test1 : VVect [2, 2, 2] Nat
test1 = [[1, 2], [3, 4], [5, 6]]

test2 : VVect [0, 1, 2] Bool
test2 = [[], [True], [False, True]]

或者，您可以使用依赖对和 map 来定义 VVect，但是这样使用起来比较麻烦：

VVect' : Vect n Nat -> Type -> Type
VVect' {n = n} is a = (xs : Vect n (m ** Vect m a) ** (map fst xs = is))

test3 : VVect' [0, 1, 2] Bool
test3 = ([(_ ** []), (_ ** [True]), (_ ** [False, False])] ** Refl)

您可以选择使用列表还是向量。使用列表作为内部容器，值看起来更紧凑：

VVect'' : Vect n Nat -> Type -> Type
VVect'' {n = n} is a = (xs : Vect n (List a) ** (map length xs = is))

test4 : VVect'' [0, 1, 2] Bool
test4 = ([[], [True], [False, True]] ** Refl)

在 Idris 中，所有长度都已知的双打列表的类型是什么？

In Idris, what's the type of a list of lists of doubles, where all the lengths are known?

idris

dependent-type