Использование неявных параметров в Agda - PullRequest
Новая
       71

Использование неявных параметров в Agda

0 голосов
/ 02 июля 2018

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

proof : (A : Set) → A → A
proof _ x = x

Из того, что я понимаю, _ необходимо пропустить параметр (A : Set). Я хотел использовать неявный параметр, чтобы пропустить _: 

-- using implicit parameter
proof' : {A : Set} → A → A
proof' x = x

Это доказательство работает. Затем я хотел применить его к конкретному случаю, как это делается в учебнике. Я определяю ℕ и даю подпись типа для того, что я хочу доказать: 

data ℕ : Set where
  zero : ℕ
  suc : ℕ → ℕ

idProof : ℕ → ℕ

Конструктор, приведенный в руководстве с использованием proof: 

idProof = proof ℕ

Я не совсем понимаю это, так как ожидал, что proof потребуется 2 параметра, учитывая конструктор, который мы уже определили.

Я хотел написать конструктор, используя proof', но обнаружил, что ничего из следующего не работает: 

idProof = proof' ℕ
idProof = {x : ℕ} → proof' x
idProof = {x : Set} → proof' x

Используя солвер, я нашел, что это сработало: 

idProof = proof' (λ z → z)

Мои вопросы:

  1. В чем различия между proof и proof'?

  2. Почему допустимо использовать один параметр, ℕ, для proof?

  3. Почему три конструктора, использующие proof', не работают?

Бонус:

Небольшое объяснение того, как работает idProof = proof' (λ z → z) (особенно лямбда), будет оценено, если только оно, вероятно, не будет соответствовать моему нынешнему уровню понимания Агды.

1 Ответ

0 голосов
/ 02 июля 2018

Я не до конца понимаю, так как ожидал, что proof потребуется 2 параметра, учитывая конструктор, который мы уже определили.

proof ожидает 2 параметра. Но idProof также ожидает один параметр.

Когда вы пишете 

idProof : ℕ → ℕ
idProof = proof ℕ

Это эквивалентно сначала ввести idProof 'ℕ, а затем передать его proof ℕ, вот так. 

idProof : ℕ → ℕ
idProof n = proof ℕ n

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

  • idProof = proof' ℕ

Параметр A для proof' неявный. Поэтому нет необходимости явно указывать ℕ. Вы можете просто написать idProof = proof' и позволить Агде выяснить, что A должно быть ℕ.

  • idProof = {x : ℕ} → proof' x и idProof = {x : Set} → proof' x

idProof имеет тип ℕ → ℕ, но {x : _} → ... используется для создания Set, а не функции, поэтому он не может работать.

Бонус: небольшое объяснение того, как idProof = proof' (λ z → z) работает (особенно лямбда)

proof' : {A : Set} -> A -> A пытается выяснить, что A должно быть основано на его аргументе и типе отверстия, в котором он используется. Здесь:

  • передается функция идентификации, поэтому A должна иметь форму B -> B для некоторых B;
  • используется в отверстии типа ℕ → ℕ, поэтому A должно иметь форму ℕ → ℕ.

Вывод: Агда выбирает ℕ → ℕ для A.

...