Левая часть обобщенной функции zip никогда не проверяет - PullRequest
Новая
       29

Левая часть обобщенной функции zip никогда не проверяет

1 голос
/ 19 апреля 2019

Я пытаюсь написать функцию zip в Idris, которая объединяет произвольно много векторов одинаковой длины (len) в один вектор HList с.

То есть я пытаюсь обобщить следующую функцию: 

module Zip

import Data.Vect

%default total

zip2 : (Vect len a, Vect len b) -> Vect len (a, b)
zip2 ([], []) = []
zip2 ((x :: xs), (y :: ys)) = (x, y) :: zip2 (xs, ys)

Я определяю свой собственный HList («гетерогенный список»), используя векторы: 

data HList : Vect n Type -> Type  where
  Nil : HList []
  (::) : (x : a) -> (xs : HList as) -> HList (a :: as)

Вот вариант функции zip2 с использованием этого HList: 

zip2H : HList [Vect len a, Vect len b] -> Vect len (HList [a, b])
zip2H [[], []] = []
zip2H [(x :: xs), (y :: ys)] = [x, y] :: zip2H [xs, ys]

Пока все хорошо.

Теперь общий случай.

Сигнатура типов для произвольного числа векторов в zip становится немного сложнее, но я уверен, что понял все правильно.

n - количество векторов для zip. len - длина каждого из этих векторов: 

vects : (len : Nat) -> Vect n Type -> Vect n Type
vects len as = map (\type => Vect len type) as
-- Example:
-- `vects len [a, b] = [Vect len a, Vect len b]`
-- You cannot pattern-match on types in Idris, so you cannot get an `a` from an `Vect len a`. Instead, I go the other way around in `zip` and pass my `a`s implicitly.

zip : {types : Vect (S n) Type} -> {len : Nat} -> HList (vects len types) -> Vect len (HList types)

Теперь моя проблема: я не могу написать даже левую часть определения zip. Проверка типов продолжает жаловаться.

Пример: 

zip {n = Z} [xs] = ?zip_rhs1
zip xs = ?zip_rhs2

When checking left hand side of Zip.zip:
When checking an application of Zip.zip:
        Type mismatch between
                HList [a] (Type of [xs])
        and
                HList (Data.Vect.Vect n implementation of Prelude.Functor.Functor, method map (\type =>
                                                                                                 Vect len
                                                                                                      type)
                                                                                              types) (Expected type)

        Specifically:
                Type mismatch between
                        [a]
                and
                        Data.Vect.Vect n implementation of Prelude.Functor.Functor, method map (\type =>
                                                                                                  Vect len
                                                                                                       type)
                                                                                               types

Что мне не хватает? Я неправильно использую неявные параметры? Мне нужно написать некоторые доказательства? Есть ли лучший способ структурировать сигнатуру типа функции?

(Моя версия Idris 1.3.1-git:a93d8c9.)

РЕДАКТИРОВАТЬ: Используя код HTNW, я все равно получаю в основном ту же ошибку: 

module Zip

import Data.Vect

%default total

data HList : Vect n Type -> Type  where
  Nil : HList []
  (::) : (x : a) -> (xs : HList as) -> HList (a :: as)

vects : (len : Nat) -> Vect n Type -> Vect n Type
vects len as = map (\type => Vect len type) as

multiUnCons : {len : Nat} -> {types : Vect n Type} ->
              HList (vects (S len) types) -> (HList types, HList (vects len types))
multiUnCons {types = []} [] = ([], [])
multiUnCons {types = t :: ts} ((x :: xs) :: xss) with (multiUnCons xss)
  | (ys, yss) = (x :: ys, xs :: yss)

zip : {types : Vect n Type} -> {len : Nat} ->
      HList (vects len types) -> Vect len (HList types)
zip {len = Z} _ = []
zip {len = S n} xss with (multiUnCons xss)
  | (ys, yss) = ys :: zip yss

testVectors : HList [Vect 3 Nat, Vect 3 Char]
testVectors = [[1, 2, 3], ['a', 'b', 'c']]

*zip> :t Zip.zip testVectors
(input):1:4-23:When checking an application of function Zip.zip:
        Type mismatch between
                HList [Vect 3 Nat, Vect 3 Char] (Type of testVectors)
        and
                HList (vects len types) (Expected type)

        Specifically:
                Type mismatch between
                        [Vect 3 Nat, Vect 3 Char]
                and
                        Data.Vect.Vect n implementation of Prelude.Functor.Functor, method map (\type =>
                                                                                                  Vect len
                                                                                                       type)
                                                                                               types

РАЗРЕШЕНИЕ: zip требуется дополнительная информация: 

*zip> the (Vect 3 (HList [Nat, Char])) (zip testVectors)
[[1, 'a'], [2, 'b'], [3, 'c']] : Vect 3 (HList [Nat, Char])

*zip> zip {types=[Nat, Char]} testVectors
[[1, 'a'], [2, 'b'], [3, 'c']] : Vect 3 (HList [Nat, Char])

1 Ответ

0 голосов
/ 20 апреля 2019

Вы должны соответствовать на types тоже.Сопоставляя с types, вы также обнаруживаете что-то о vects len types, и это то, что позволяет вам дополнительно сопоставлять аргумент HList (vects len types).Кроме того, требование длины S n для types не является необходимым и нарушено.Наконец, я думаю, что вам действительно нужно сначала набрать len, а затем types.Рекурсию на types лучше всего записать как другую функцию: 

multiUnCons : {len : Nat} -> {types : Vect n Type} ->
              HList (vects (S len) types) -> (HList types, HList (vects len types))
multiUnCons {types = []} [] = ([], [])
multiUnCons {types = t :: ts} ((x :: xs) :: xss) with (multiUnCons xss)
  | (ys, yss) = (x :: ys, xs :: yss)

И zip сама по себе довольно проста: 

zip : {types : Vect n Type} -> {len : Nat} ->
      HList (vects len types) -> Vect len (HList types)
zip {len = Z} _ = []
zip {len = S n} xss with (multiUnCons xss)
  | (ys, yss) = ys :: zip yss
...