?

Log in

No account? Create an account
Как матчит Агда? - Программирование с зависимыми типами [entries|archive|friends|userinfo]
Программирование с зависимыми типами

[ userinfo | livejournal userinfo ]
[ archive | journal archive ]

Как матчит Агда? [Oct. 16th, 2013|08:59 pm]
Программирование с зависимыми типами
ru_deptypes
[nealar]
[Tags|]

В брутальном [мета-]введении в Агду попался пример

data _≤_ : ℕ → ℕ → Set where
z≤n : ∀ {n} → zero ≤ n
s≤s : ∀ {n m} → n ≤ m → succ n ≤ succ m

sub₀ : (n m : ℕ) → m ≤ n → ℕ
sub₀ n zero (z≤n .{n}) = n
sub₀ .(succ n) .(succ m) (s≤s {m} {n} y) = sub₀ n m y

Не могу понять, как определение sub0 раскрывается в case, а главное, почему так.

Тайна раскрыта
Агда матчит в том порядке, в котором написано в программе: по первой строчке выбирается паттерн с конструктором, соответствующая переменная раскрывается в case, и так далее.
Ошибка oxij в том, что по аргументам с точкой паттерн-матчить вообще нельзя

Приз "за лучшую подсказку" уходит к nivanych
LinkReply

Comments:
From: gds
2013-10-16 11:54 pm (UTC)
не помогу и не буду оригинален, но по вопросам "явности" (explicitness, штоле) лучше кококо мучить. Там очень явно, если брать низкий уровень. Но хорошо автоматизируется, если эта явность не нужна для дела.
(Reply) (Thread)
From: nealar
2013-10-17 04:08 am (UTC)
В эпиграмме вообще эти case надо руками писать. :)
(Reply) (Parent) (Thread)
From: dima_starosud
2013-10-17 05:37 pm (UTC)
Я бы советовал не обращать на это внимание (на Хаскель псевдокод). Потому что оно так не раскрывается, это автор себе что-то придумал и парит вам :-D
И так много инфы, как для введения для with half-way-through-undergrad-course, а тут еще и аналогии.
(Reply) (Thread)
From: nealar
2013-10-17 06:08 pm (UTC)
Я так и понял, что с псевдокодом подстава. Хочу понять, как же оно раскрывается. А то у меня из его пяти sub (различающихся только расстановкой точек) две не компилируются.
(Reply) (Parent) (Thread)
From: dima_starosud
2013-10-17 06:23 pm (UTC)
А какие именно? И как матерится?

UPD: Еще я бы советовал действительно пропускать те вещи которые воооооообще непонятны. И конечно же Agda mail list ;) весьма отзывчивое комюнити.

Edited at 2013-10-17 06:42 pm (UTC)
(Reply) (Parent) (Thread)
From: nealar
2013-10-18 07:45 am (UTC)
Мэйл-листом щаз воспользуюсь. А ирка/джаббер у агдосообщества есть?
(Reply) (Parent) (Thread)
[User Picture]From: nivanych
2013-10-18 06:28 pm (UTC)
#agda на irc.freenode.net
(Reply) (Parent) (Thread)
From: nealar
2013-10-21 12:42 pm (UTC)
Матерится, что паттерн sub zero (succ _) _ не закрыт. Функции вот такие:

sub₀ : (n m : ℕ) → m ≤ n → ℕ
sub₀ n zero (z≤n .{n}) = n
sub₀ .(succ n) .(succ m) (s≤s {m} {n} y) = sub₀ n m y

sub₁ : (n m : ℕ) → m ≤ n → ℕ
sub₁ n .zero (z≤n .{n}) = n
sub₁ .(succ n) .(succ m) (s≤s {m} {n} y) = sub₁ n m y

sub : (n m : ℕ) → m ≤ n → ℕ
sub n zero (z≤n .{n}) = n
sub (succ n) (succ m) (s≤s .{m} .{n} y) = sub n m y

sub₃ : (n m : ℕ) → m ≤ n → ℕ
sub₃ n zero _ = n
sub₃ (succ n) (succ m) (s≤s .{m} .{n} y) = sub₃ n m y

sub₄ : (n m : ℕ) → m ≤ n → ℕ
sub₄ n zero (z≤n .{n}) = n
sub₄ (succ .n) (succ .m) (s≤s {m} {n} y) = sub₄ n m y

sub0 и sub1 - принимает, остальные три отвергает.
(Reply) (Parent) (Thread)
From: dima_starosud
2013-10-24 05:35 pm (UTC)
Простите пожалуйста, ничем не могу помочь, у меня все работает :)
Версия Агда где-то месячной давности.
(Reply) (Parent) (Thread)
[User Picture]From: deni_ok
2013-11-16 07:39 pm (UTC)
Мы это в твиттере с Яном обсуждали, там ещё один case нужен, чтобы в 2.3.0.x тоже компилировалось. Он обещал поправить, но, похоже, забиыл.
https://twitter.com/deniok/status/298433882976563200
(Reply) (Parent) (Thread)
[User Picture]From: nivanych
2013-11-08 08:22 pm (UTC)
Короче говоря, читайте документацию, оно рулит ;-)
Даже если документация такая скудная, как у агдочки.
(Reply) (Thread)
From: nealar
2013-11-09 07:50 am (UTC)
Бида в том, что взрослую документацию обычно читаешь после туториала. А тут желательно это делать параллельно.
(Reply) (Parent) (Thread)
From: dima_starosud
2013-11-08 08:59 pm (UTC)
> Ошибка oxij в том, что по аргументам с точкой паттерн-матчить вообще нельзя
Мне кажется, что вы его не правильно поняли. Как можно матчить то, что выводится?
Я это о том, что мысль "по аргументам с точкой паттерн-матчить" - это полнейший бред.
Простите пожалуйста, но, то, что у вас такая мысль возникла, не было понятно с ваших слов.
(Reply) (Thread)
From: nealar
2013-11-09 07:49 am (UTC)
Код функции sub1. Матчинг по аргументам с точкой. Осознал, что аргументы с точкой и параметры с точкой - возможно, разные сущности. Короче, исходник надо будет посмотреть, и не ломать голову. Говорят, он понятный.


Edited at 2013-11-09 08:46 am (UTC)
(Reply) (Parent) (Thread)
From: dima_starosud
2013-11-09 08:51 am (UTC)
А вот и нет :)
sub₁ : (n m : ℕ) → m ≤ n → ℕ
sub₁ n .zero (z≤n .{n}) = n
матчится по доказательству m ≤ n (точнее по голове доказательства) и вводится n, которое первый аргумент, отсюда выводится, что m = zero, а n, которое под z≤n равно первому аргументу n.

sub₁ .(succ n) .(succ m) (s≤s {m} {n} y) = sub₁ n m y
аналогично со второй строкой (то есть матчинг по доказательству). Просто внимательно присмотритесь, возле чего именно стоит точка.
(Reply) (Parent) (Thread)