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

[deniok]

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

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

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

Comments

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

[dmytro starosud (from livejournal.com)]

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

[deni-ok.livejournal.com]

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

Буду думать.