Соответствие шаблону Идриса на преемнике (следующее значение) - PullRequest
Новая
       64

Соответствие шаблону Идриса на преемнике (следующее значение)

0 голосов
/ 03 апреля 2020

В следующей функции я сопоставляю шаблон с Преемником k на (S k) 

vectTake : (n : Nat) -> Vect (n + m) a -> Vect n a
vectTake Z xs = []
vectTake (S k) (x :: xs) = x :: vectTake k xs

Можно ли использовать это значение в теле функции, если это необходимо?

Другим решением было бы сопоставление по k и использование предшественника k в функции тела, так что просто еще одна форма решения той же проблемы или такой тип сопоставления с образцом дает какие-либо другие преимущества, которые я не мог видеть?

1 Ответ

1 голос
/ 05 апреля 2020

По первому вопросу ...

(примитивное) определение Nat равно 

data Nat = Z | S Nat

Мы можем сопоставить:

  • an произвольное значение с использованием k
  • конструкторов. Вот это Z или S k. Конечно, S k будет связывать другое значение с k, чем если бы мы сопоставили шаблон только с k

После того, как вы сопоставили значение, вы можете делать все, что обычно можете сделать с Nat, включая создание преемника с использованием S, поэтому, если вы хотите сопоставить S k и использовать его в функции, вы можете просто 

...
vectTake (S k) (x :: xs) = (S k) :: vectTake k xs

, хотя здесь я изменил значение вашей функции, чтобы проиллюстрировать мою точку зрения. В этом примере вы также можете использовать именованный шаблон 

...
vectTake count@(S k) (x :: xs) = count :: vectTake k xs

Для вашего второго вопроса ...

Под pred k Я предполагаю, что вы имеете в виду предшественник, а не предикат , Если это так, вы можете выполнять целочисленные операции над Nat, включая k - 1, поэтому, возвращаясь к исходному определению vecTake

...
vectTake k (x :: xs) = x :: vectTake (k - 1) xs

Обратите внимание, что это зависит от совпадения для Z, которое идет первым иначе вы в конечном итоге будете делать Z - 1, который не будет компилироваться.

Что касается того, что лучше из совпадений на Z и S k или Z и k, я могу не думаю о какой-либо объективной причине, почему один лучше другого. Возможно, в некоторых случаях это влияет на производительность, но я не могу вам помочь. Я бы в основном использовал шаблоны конструктора, потому что люди привыкли бы видеть это, но я уверен, что будут случаи, когда другие стили оправданы.

...