Вложенные пар Упражнение

Question

Проработка Ch6 упражнений Type-Driven Development with Idris,

упражнение 3 гласит:

Мы могли бы реализовать вектор в качестве вложенных пар, с вложенности, рассчитанной исходя из длины . Например:

TupleVect 0 ty =() 
TupleVect 1 ty = (ty,()) 
TupleVect 2 ty = (ty, (ty,())) 

Определить функцию TupleVect уровня типа, который реализует этот поведение. Не забудьте начать с типа TupleVect. Если у вас есть правильный ответ, следующее определение будет справедливо:

test : TupleVect 4 Nat 
test = (1,2,3,4,()) 

Вот что я придумал:

TupleVectType : Nat -> (a : Type) -> Type 
TupleVectType Z  _ =() 
TupleVectType (S n) a = (a, TupleVectType n a) 

TupleVect : (n : Nat) -> a -> TupleVectType n a 
TupleVect Z _  =() 
TupleVect (S n) a = (a, TupleVect n a) 

Я думал, что это было достаточно, но, MyTupleVect 4 Nat неправильно :

*Exercises> TupleVect 4 Nat 
(Nat, Nat, Nat, Nat,()) : (Type, Type, Type, Type,()) 

Но, если я обеспечиваю действительное значение, т.е. не Type, это Ретур нс:

*Exercises> TupleVect 4 True 
(True, True, True, True,()) : (Bool, Bool, Bool, Bool,()) 

Пожалуйста, сообщите мне о том, как исправить эту TupleVect функции, чтобы соответствовать ожидаемому результату.

Это мне не ясно, как обеспечить TupleVect 4 Nat, а затем перечислить Nat «с, но начиная с 1, не 0.

Answer 1

Ваше определение TupleVectType - это на самом деле то, что должно быть TupleVect. Упражнение просит вас выполнить функцию TupleVect, которая возвращает тип от n -образные кортежи-представленные векторы.

Ваше определение TupleVect является реализация того, что обычно называют replicate, которая принимает один x : a к вектору repeat x : Vect n a за счет тиражирования его п раз.

В целом, с определениями, следующие typechecks, как и ожидалось:

foo : TupleVectType 4 Nat 
foo = (1, 2, 3, 4,()) 

, так что я бы посоветовал просто переименовать TupleVectType в TupleVect.