термологический вопрос

[deni_ok]

Коллеги! Не будет ли слишком изощренным издевательством во вводной части обзора Агды, при самом начале обсуждения типа Vec привести такие примеры

[true,false,true] : Vec Bool 3
[2,12,85,0,6] : Vec ℕ 5
Поясню - я не хочу в этом месте вдаваться в детали описания конструкторов, а скрытый здесь грандиозный обман я честным образом раскрою позже.

Comments

[ulysses4ever]

Я Агды не знаю совсем, но пример мне нравится! Интуитивно понятно. Готов потерпеть обман ради такого.

[deni_ok]

на самом деле в Агде все лексемы должны быть отделены друг от друга пробелами. То что стоит слева от каждого оператора типизации (:) - просто идентификатор (причём валидный :)

[ulysses4ever]

А, круто…

[ext_610527]

Сурово. Кто-нибудь на автомате с пробелами напечатает - и твой обман раскроется.

[akuklev]

Эм, тонкое, тонкое извращение. :)

[deni_ok]

Надо сказать этим извращением активно пользуются в стандартной библиотеке, за милую душу обзывая переменную типа m ≤ n идентификатором m≤n.

[nivanych]

"Ви так говорите, как будто, в этом есть что-то плохое"
Ну так, если знать простое правило про идентификаторы, то ничего страшного-то нет.
В большинстве текстовых редакторов и просто средств для просмотра кода, визуально "m ≤ n" легко отличить от "m≤n".

[nivanych]

Хотя и помнится, по-первости, меня слегка раздражало "идентификатор a+b неизвестен".
Причём, я не сразу на это натолкнулся - обычно, я пишу через пробел ;-)

[dima_starosud]

Я думаю, в вводной части обязательно нужно сказать о пробелах, юникоде и синтаксисе - это ведь база, и здесь ничего сложного нету, просто пробелы, всего то.
Кстати, а как вы такой вектор сделали? Это в стандартной библиотеке? Или это псевдокод?

[deni_ok]

Это форменное издевательство, как и было объявлено:

module VecTest where

open import Data.Nat
open import Data.Vec

[2,12,85,0,6] : Vec ℕ 5
[2,12,85,0,6] = 2 ∷ 12 ∷ 85 ∷ 0 ∷ 6 ∷ []

[dima_starosud]

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

[deni_ok]

Да нет, это случайно вышло. Я во введении хотел рассказать общие вещи про зависимые типы, но нужны какие-то примеры. Полезла Agda, ну и следовательно всякие детали синтаксиса. А вдаваться в них там не очень к месту.

Буду думать.

[nivanych]

Если в сноске признаться, что тут обман, который честным образом раскроется позже, то нормально, думаю.

[deni_ok]

Да, так пока и сделал.

[nivanych]

Но надо сказать, что 2 ∷ 12 ∷ 85 ∷ 0 ∷ 6 ∷ [] выглядит не так и плохо, чтобы зачем-то надо было обманывать.
Можно оператор составить и из одного символа, только с более простым набором.
Но для чтения, это малосущественно.