Idris - сбой функции карты для пользовательского зависимого типа - PullRequest
Новая
       57

Idris - сбой функции карты для пользовательского зависимого типа

0 голосов
/ 09 июня 2018

Я относительно новичок в idris и зависимых типах, и я столкнулся со следующей проблемой - я создал собственный тип данных, похожий на векторы: 

infixr 1 :::

data TupleVect : Nat -> Nat -> Type -> Type where
    Empty : TupleVect Z Z a
    (:::) : (Vect o a, Vect p a) ->
            TupleVect n m a ->
            TupleVect (n+o) (m+p) a

exampleTupleVect : TupleVect 5 4 Int
exampleTupleVect = ([1,2], [1]) ::: ([3,4],[2,3]) ::: ([5], [4]) ::: Empty

Он индуктивно создается путем добавления кортежей векторов и индексируетсясуммой длин векторов в каждой позиции кортежа.

Я попытался реализовать функцию карты для моего типа данных: 

tupleVectMap : ((Vect k a, Vect l a) -> (Vect k b, Vect l b)) ->
               TupleVect n m a -> TupleVect n m b
tupleVectMap f Empty = Empty
tupleVectMap f (x ::: xs) = let fail = f x
                            in ?rest_of_definition

Это приводит к следующей ошибке типа: 

   |
20 | tupleVectMap f (x ::: xs) = let fail = f x
   |                             ~~~~~~~~~~~~~~ ...
When checking right hand side of tupleVectMap with expected type
        TupleVect (n + o) (m + p) b

Type mismatch between
        (Vect o a, Vect p a)
and
        (Vect k a, Vect l a)

Кажется, что средство проверки типов не может объединить длины векторов в извлеченном кортеже x и необходимые длины в аргументе f.Однако я не понимаю, почему это так, поскольку k и l являются просто именами типов, указывающими, что f не меняет длину данных векторов.

Я еще более озадачен, поскольку следующие проверки типов: 

tupleVectMap' : TupleVect n m a -> TupleVect n m b
tupleVectMap' Empty = Empty
tupleVectMap' (x ::: xs) =
    let nonfail = f x
    in ?rest_of_definition
      where
        f : ((Vect k a, Vect l a) -> (Vect k b, Vect l b))

Здесь f имеет точно такую ​​же сигнатуру типа.Единственная разница в том, что f определяется локально.

1 Ответ

0 голосов
/ 09 июня 2018

Если вы :set showimplicits в refl, вы увидите разницу между двумя функциями.

В tupleVectMap есть 

f : (Data.Vect.Vect k a, Data.Vect.Vect l a) ->
    (Data.Vect.Vect k b, Data.Vect.Vect l b)
x : (Data.Vect.Vect o a, Data.Vect.Vect p a)

Потому что k и o(l и p) необязательно равны, x нельзя применить к f.В основном, если вы звоните tupleVectMap, вы уже определили, что f принимает только Vect с длиной k.

В то время как в tupleVectMap' это 

f : {k : Prelude.Nat.Nat} -> {l : Prelude.Nat.Nat} ->
    (Data.Vect.Vect k a, Data.Vect.Vect l a) ->
    (Data.Vect.Vect k b, Data.Vect.Vect l b)
x : (Data.Vect.Vect o a, Data.Vect.Vect p a)

Здесь f принимает два неявных аргумента для установки длины Vect s при каждом вызове.Так что f x {k=o} {l=p} работает (хотя вам не нужно указывать неявные аргументы).

Это будет работать так же, если вы определите свой тип функции как 

tupleVectMap : ({k, l : Nat} -> (Vect k a, Vect l a) -> (Vect k b, Vect l b)) ->
               TupleVect n m a -> TupleVect n m b
...