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

[deniok]

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

[true,false,true] : Vec Bool 3
[2,12,85,0,6] : Vec ℕ 5

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

Comments

[ulysses4ever.livejournal.com]

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

[deni-ok.livejournal.com]

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

[ulysses4ever.livejournal.com]

А, круто…

[alexey bakhirkin (from livejournal.com)]

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

[akuklev.livejournal.com]

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

[deni-ok.livejournal.com]

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

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

Правда тип выражения можно в минибуфере глядеть по C-c C-d

[dmytro starosud (from livejournal.com)]

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

[deni-ok.livejournal.com]

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

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 ∷ []

[deni-ok.livejournal.com]

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

[dmytro starosud (from livejournal.com)]

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

[deni-ok.livejournal.com]

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

Буду думать.

[nivanych.livejournal.com]

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

[nivanych.livejournal.com]

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

[nivanych.livejournal.com]

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

[nivanych.livejournal.com]

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

[deni-ok.livejournal.com]

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

[deni-ok.livejournal.com]

не, я согласен, что это хороший способ именования, просто к нему привыкнуть надо, очень уж он необычный

[nivanych.livejournal.com]

Я считаю, что агдочка достаточно красиво, чтобы её рассказывать без обману! ;-)

[deni-ok.livejournal.com]

Хорошо, так и поступим!

[nivanych.livejournal.com]

Нет, ну правда — неужели, этот мелкий синтаксический трюк что-то значит?

[deni-ok.livejournal.com]

я уже вполне согласен, что идея была дурацкой

[nivanych.livejournal.com]

Нет, я буду доказывать! ;-)