'half' function type signature в Idris

Question

Я довольно новичок в Идрисе, и я пытаюсь поймать основные понятия и синтаксис.

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

Я хочу, чтобы придумать что-то вроде:

half : (n : Nat) -> (k : Nat) -> (n = k + k) -> (k : Nat) 

но, конечно, это не работает. В частности, я получаю:

error: expected: dependent type signature

half : (n : Nat) -> (k : Nat) -> (n = k + k) -> (k : Nat) 

Возможно ли это?

Спасибо.

Answer 1

Что вы хотите, так это выразить то, что half n является некотором Nat номеру уезда k такой, что n = k + k занимает. Способ сделать это с помощью sigma type, т.е. зависимой пары ряда k и доказательства n = k + k (это зависит от пары, потому что типа второй координаты, n = k + k зависит от значения первой координаты, k).

Стандартная библиотека Идриса определяет DPair для пар мере зависит, в том числе некоторых синтаксических, позволяя вам писать

half : (n : Nat) -> (k ** n = k + k) 

Однако, обратите внимание, что вы не сможете реализовать half (как общая функция), потому что есть нет хорошего ответа, например half 1. Возможно, вы хотите знать, что вы хотите:

half : (n : Nat) -> (k ** Either (n = k + k) (n = k + k + 1)) 

?

Answer 2

Вы не должны использовать k дважды. half: (n: Nat) -> (k: Nat) -> (n = k + k) -> Nat является правильным, но бесполезным. Думаю, что вам нужно половина: (n: Nat) -> Может быть (k ** n = k + k)