В Идрисе, какой тип списков двойников, где все длины известны? - PullRequest
Новая
       57

В Идрисе, какой тип списков двойников, где все длины известны?

0 голосов
/ 21 сентября 2018

Пример значения: [[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 является соответствующим элементом первого вектора.

1 Ответ

0 голосов
/ 21 сентября 2018

Вы можете определить новый векторный тип, который содержит возможно по-разному проиндексированные элементы индексированного типа в каждой позиции: 

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]]

В качестве альтернативы, вы можете определить VVect, используя зависимые пары и map, ноэто более громоздко для использования: 

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)
...