ооп и функциональщина кратко, внятно.

И еще пара вопросов: на сколько в racket легко (и возможно ли?) запилить свои иммутабельные структуры, есть ли коллекции таких структур в стандартной либе? Распространена ли практика написания программ в функциональном стиле с иммутабельными структурами и ленивыми коллекциями? Удобно ли совмещаются стандартный диалект и lazy-racket в одном модуле? Осуществляются ли какие-то оптимизации на уровне компилятора при программировании в функциональном стиле с использованием иммутабельных структур, как это происходит в тех же clojure и haskell?

Если ты чего-то не знаешь — я тут ни при чём.

При чем тут я не знаю? еще раз - это ты сам придумал.

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

подумай. Если не можешь придумать - подумай еще раз.

Да нет никаких рантаймов кроме описанных тотальных редукций во время тайп-чека.

У агды нету семантики? Нету правил редукции термов и установления их эквивалентности? Значит агда - не язык программирования и говорить не о чем.

Настоящие рантаймы у агды это сторонние расширения

Нету никаких сторонних расширений. И агды самой нету - только ее спеки.

Ну как обычно — ты что-то там решил себе

Я решил, лол? по каждому пункту есть сторонний объективный пруф. Определения зависимых типов - сторонний пруф, возможность подстановки неизвестных термв в агде/атс/петухе - сторонние пруфы, возможность делать в омеге все что в плюсах - сторонние пруфы.

Кстати, можешь Oleg-а приобщить

Замечательно, Oleg со мной соглдасен. (ну я и не ожидал иного -= ведь моя точка зрения - это общепринятая точка зрения, да и вообще единственно возможная)

Omega restrict the form of dependent types they allow

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

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

Ну, хотя бы некоторые интересные вещи (или все?) из драфа racket2. Конкретно меня интересует:

Первые два пункта - это сотня-две строк кода. Последний - тут да, проблемы, CLOS просто так не накостылишь.

Ну, и вообще - на сколько семантика языка позволяет написать нормальный мультидиспатч, типа как в clojure?

Всмысле? Мультидиспатч с семантикой никак не связан, он же в динамических языках все равно делается руками.

Еще вопрос - есть реализация STM для racket?

Нет.

Если попробовать использовать рэкет для «продакшна», на сколько забагована ее PLT-реализация?

Ну кое-где используют, вроде успешно. Если по маиллисту ориентироваться, то баги встречаются, конечно, но достаточно редко. И плюсом то, что их фиксят за сутки-двое обычно.

на сколько в racket легко (и возможно ли?) запилить свои иммутабельные структуры

Ну например: http://planet.racket-lang.org/display.ss?package=pfds.plt&owner=krhari

В стандартной либе вообще для всего есть иммутабельный вариант и значительная часть структур иммутабельна по дефолту.

Распространена ли практика написания программ в функциональном стиле с иммутабельными структурами и ленивыми коллекциями?

Язык-то по дефолту не ленивый, так что пишут тогда, когда от лени есть реальные профиты (а это очень редко, вообще говоря).

Удобно ли совмещаются стандартный диалект и lazy-racket в одном модуле?

Не совсмем понятно, что это значит. Если мы в модуле lay то мы в модуле lazy и там все будет lazy, кроме импортирпованных не-lazy функций, которые будут форситься. Еще могут быть неожиданные для неподготовленного лица эффекты с макросами из-за гигиены аппликации :)

Но lazy у них как-то криво-медленно реализован. А вообще лень без поддержки на самом низком уровне рантайма нельзя сделать быстрой, к сожалению.

Осуществляются ли какие-то оптимизации на уровне компилятора при программировании в функциональном стиле с использованием иммутабельных структур, как это происходит в тех же clojure

А как происходит в clojure? В haskell - это про фьюжн или что?

Всмысле? Мультидиспатч с семантикой никак не связан, он же в динамических языках все равно делается руками.

Ну, в смысле мультидиспатч не только по классу объектов, но и с настраиваемой (пользовательской) функцией диспетчеризации.

Ok, спасибо.

Ну семантика языка тут один хрен не при чем уже, тут дело в том, как именно сделан диспатч.

В стандартной либе вообще для всего есть иммутабельный вариант и значительная часть структур иммутабельна по дефолту.

Конкретно для программирования на рэкете это что-то дает? Ну, кроме очевидных гарантий для пользователя? Типа там JIT применяет какие-то оптимизации итд.

Удобно ли совмещаются стандартный диалект и lazy-racket в одном модуле?

Не совсмем понятно, что это значит.

Например в модуль с базовым рэкетом импортируются ленивые функции / структуры из модуля на lazy, в таком варианте оно норм работает?

А как происходит в clojure? В haskell - это про фьюжн или что?

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

Ну, кроме очевидных гарантий для пользователя? Типа там JIT применяет какие-то оптимизации итд.

Нет не применяет.

Например в модуль с базовым рэкетом импортируются ленивые функции / структуры из модуля на lazy, в таком варианте оно норм работает?

Работает.

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

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

подумай

Я уже сказал как.

ты сам придумал

Нету правил редукции термов и установления их эквивалентности?

Ты же вроде уже соглашался — в омеге типы редуцируются на основе применения операций типов, а в зависимых типах типы применяются к термам (каких-то типов, ага), то есть установление эквивалентности типов требует самой обычной беты для термов, итого — во время 2 нужно делать 3.

неизвестных термв в агде/атс/петухе

атс

Ага. «Сторонний пруф» у тебя, конечно, есть?

Вот в моей цитате Chlipala отказывается называть ATS языком с зависимыми типами.

Ну вот

Статью открой — омега это название языка (хотя отношение к этой самой омеге он и имеет, причём они утверждают, что им этого хватает для «dependent-style programming»).

Вот ты сам привел кучу цитат каждая из которых поддерживает мою правоту

Licata же нормально написал — почитай ещё раз. А то точка зрения единственная, а авторы ATS расписывают в своей документации про зависимые типы, а Chlipala говорит — «нет, ребята, это не зависимые типы».

Ага. «Сторонний пруф» у тебя, конечно, есть?

Ты же сам и скинул на этот пруф ссылку (спеки АТС или что это было?).

Я уже сказал как.

Нет, не сказал.

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

С чего у тебя из первого тут следует второе? Ты явно что-то пропустил. Кроме того, агда же как-то умудряется устанавливать эквивалентность без редукции, например в случае типа

f = lambda x. (let y = x, let z = x, a1 = new array<y>, let a2 = new array<z>)

Вот в моей цитате Chlipala отказывается называть ATS языком с зависимыми типами.

Читаем: «My definition of «a dependent type system»» и на этом моменте читать прекращаем, потому что никого не волнует «my definition» общепринятых математических терминов.

а авторы ATS расписывают в своей документации про зависимые типы

Сами авторы ATS говорят, что у них restricted вариант.

Licata же нормально написал

Читаем: «I use the term «dependent types» more broadly» и снова дальше можно не читать по вышеуказанным причинам.

Есть термин, у термина есть _формально строгое определение_. Это блять не просто какое-то там определение на естественном языке, которое может быть неточным или еще какая хуйня - это математика, блять! строгий формализм, блять! И никого не ебет, чего там себе напридумывала команда долбоебов. Пусть они хоть в жопу друг друга трахают и называют это «зависимыми типами».

Потому что как только мы от строгих определний уходим в сторону «мне кажется, я так думая, я определяю как ...» - то тогда каждый может заебенить свое определение. Если в плюсах есть зависимые типы - то почему в простой типизированной лямбде нету зависимых типов? Ведь простая типизированная лямбда вполне имеет " type-level data that can be used to specify and verify properties of programs" и является «anguage with fancy type-level data». Любой статически типизированный ЯП, таким образом имеет зависимые типы, так как удовлетворяет «широкому пониманию» ебнутого на голову Dan Licata и не менее ебнутого на голову quasimoto.

Ну семантика языка тут один хрен не при чем уже, тут дело в том, как именно сделан диспатч.

Ну как это не при чем? Семантика defmulti позволяет задавать функцию для диспатча, и это не только class. Так можно?

Ну как это не при чем?

Ну так.

Семантика defmulti позволяет задавать функцию для диспатча, и это не только class. Так можно?

Как реализуешь, так и можно.

на сколько семантика языка позволяет написать нормальный мультидиспатч, типа как в clojure?

мультидиспатч сделать не проблема, можно погуглить, кто-то уже делал мультиметды. анонимус вроде даже на лор выкладывал.

Проблема сделать эффективный мультидиспатч. А если не париться то да - делов на полсотни тсрок.

спеки АТС или что это было?

Это была статья про DML про то как «можно сделать». А в ATS statics и dynamics — http://www.ats-lang.org/DOCUMENT/INTPROGINATS/HTML/c2100.html, http://lambda-the-ultimate.org/node/1566 «ATS has a clear separation between statics and dynamics, and the statics part may never refer to the dynamics».

например в случае типа

Ну блин, это же не агда. Агда это

f = λ x → let y = x in let z = x; a₁ = replicate {n = y} 1 in let a₂ = replicate {n = z} 2 in a₁ , a₂

и после редукций с выводом типа получается

f′ : (x : ℕ) → Vec ℕ x × Vec ℕ x
f′ = λ x → replicate 1 , replicate 2

Ну и как бы причём тут это (вообще о чём речь?). Речь про то что, в очередной раз пример, refl : ∀ {a} → a ≡ a, так что если есть программа f : ... → t[...] ≡ u[...]; f ... = ...[refl], то чтобы проверить типы нужно разбирать паттерн-матчинг и проводить редукции термов t и u для каждой ветви, в простейшем случае f : ... → t[...] ≡ u[...]; f ... = refl — проводить редукции t и u для выяснения того что они равны в definitional смысле, так что refl подходит по типу, и _≡_ тут не уникален — для любого типа который применяется к термам (LF!) так, поэтому в агде и вообще в зависимых типах можно считать всё что можно считать на термах при проверке типов (в агде — через тот же Proxy). То есть нужна β-convertibility термов — CR и нормализация делают её разрешимой (в том числе с помощью унификации). http://www.cse.chalmers.se/~peterd/papers/DependentTypesAtWork.pdf — 5.2, http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.65.7934&rep=rep1... — более подробно.

Читаем: «My definition of «a dependent type system»» и на этом моменте читать прекращаем

Даже если его «my definition» совпадает с «общепринятым»? :) Что не позволяет ему смотреть на ATS как на ЗТ (потому как оно omega-like, ну может ещё с какой-то рефлексией (типа http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.128.1673&rep=rep... ) — я пока не нашёл).

так как удовлетворяет «широкому пониманию» ебнутого на голову Dan Licata

А ещё PhD, assistant professor и IAS member, понимаешь :)

Ну блин, это же не агда.

Разница чисто синтаксическая.

и после редукций с выводом типа получается

Там нету никаких редукций. Вообще. В этой программе нету ни одной редукции.

Ну и как бы причём тут это (вообще о чём речь?)

Речь о том, что агда прекрасно проводит тайпчек без редукций.

то чтобы проверить типы нужно разбирать паттерн-матчинг и проводить редукции термов t и u

Но агда прекрасно справляется с тайпчеком, не проводя никаких редукций. Как в вышеприведенном примере. Ни одной редукции - а тайпчек вполне завершен!

Даже если его «my definition» совпадает с «общепринятым»?

«My definition» по определению не совпадает с общепринятым, иначе нет смысла называть его «my». В этом случае можно писать просто: «definition».

А ещё PhD, assistant professor и IAS member, понимаешь :)

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

http://www.cse.chalmers.se/~peterd/papers/DependentTypesAtWork.pdf — 5.2,

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

В этой программе нету ни одной редукции.

f = λ x → let y = x in let z = x; a₁ = replicate {n = y} 1 in let a₂ = replicate {n = z} 2 in a₁ , a₂

f′ : (x : ℕ) → Vec ℕ x × Vec ℕ x
f′ = λ _ → replicate 1 , replicate 2

sup? : f ≡ f′
sup? = refl

как это он догадался без редукций?

И напомню:

  data _≡_ {a} {A : Set a} (x : A) : A → Set a where
    refl : x ≡ x

обычный тип.

агда прекрасно проводит тайпчек без редукций

Давай ещё раз:

5!≡12*10 : 5 ! ≡ 12 * 10
5!≡12*10 = refl

a+0≡a : ∀ a → a + 0 ≡ a
a+0≡a 0 = refl
a+0≡a (suc a) = cong suc (a+0≡a a)

Итак, как проверяется 5!≡12*10 (это такое имя функции — слитно, так что один токен) без редукций (вычислили 5 ! и потом 12 * 10)? На самом деле проводятся обычные редукции closed термов, ну а потом refl : ∀ {a} → a ≡ a — видишь что a с обоих сторон одно и то же, тогда как 5 ! и 12 * 10 — два разных терма, значит их нужно редуцировать и если они сведутся к одному и тому же, значит refl действительно подходит в качестве программы-доказательства данному типу-утверждению (пруф/тайп-чек), разумеется, вместо этих термов могут быть любые сколь угодно сложные тотальные вычисления на термах. Дальше — вторая функция a+0≡a, тут редукции проводятся для открытых термов (если ты откроешь учебник по LC, то увидишь, что отношение редукции задаётся на множестве всех термов — открытых и закрытых). То есть ты не правильно понял статью — редукции проводятся независимо от закрытости или открытости термов (ну как в обычном LC) и это не «дополнительные правила типизации» — используется ровно то что было написано в определении _+_:

_+_ : ℕ → ℕ → ℕ
zero  + n = n           -- (1)
suc m + n = suc (m + n) -- (2)

поэтому 0+a≡a доказывается тривиально как refl (потому что есть редукция (1), тут она применима к открытому терму), тогда как a+0≡a требует доказательства по индукции ((1) для закрытого терма в base-case и (2) для открытых термов в step-case), я объяснял это в начале того поста — ооп и функциональщина кратко, внятно. (комментарий).

Цитаты:

In Agda we cannot infer types in general, but we can always check whether a certain term has a certain type provided it is normal. The reason for this is that the typechecking algorithm in Agda uses normalisation (simplification), and without the normality restriction it may not terminate.

Agda uses these definitions (which are given by equations) during type-checking to reduce type expressions to their normal form.

Here, the symbol _=_, which we have used when introducing the definition of functions, stands for definitional equality. When two terms t and t' are defined to be equal, that is, they are such that t = t', then the type-checker can tell that they are the same by reducing them to normal form. Hence, substitutivity is automatic and the type-checker will accept a term h of type (C t) whenever it expects a term of type (C t') and vice versa, without needing extra logical information.

В (foo : ∀ {a} → Foo a a) две a равны именно в definitional смысле, и как ты видишь из этого объяснения — когда ты пишешь f : Foo (some-closed-term-t) (some-closed-term-u); f = foo у тебя будут происходить обычные произвольные редукции термов во время проверки типов. Если ты пишешь f : ... -> Foo (some-open-term-t[...]) (some-open-term-u[...]); f ...step-case... = ...; ...; f ...base-case... = ...[foo] у тебя будут происходить произвольные редукции открытых термов.

В самом деле — попробуй что-нибудь на агде, кроме type-level ничего нет и все вычисления ты проводишь именно в нём, то есть во время проверки типов (нет тотального вычисления которое бы ты не мог сделать во время проверки типов — не согласен, так примеры сюда).

Ни одной редукции - а тайпчек вполне завершен!

Допустим, q : ℕ; q = 0 не нужны редукции. Но вообще без них никак — это фундаментально в зависимых типах.

нет смысла называть его «my»

У тебя тоже «my». Смотри — если принять твою картинку, то в агде до тайп-чека включительно (и не далее) нет зависимых типов. Там же всё известно во время компиляции (как с constexpr — не согласен? Примеры сюда :)), рантайма в смысле IO нет, только тотальные редукции термов в типах, а всякие вещи с открытыми термами ничем не отличаются от шаблонов (кроме того что чекаются).

как это он догадался без редукций?

Подумай.

Давай ещё раз:

Давай. Итак:

f = λ x → let y = x in let z = x; a₁ = replicate {n = y} 1 in let a₂ = replicate {n = z} 2 in a₁ , a₂

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

То есть ты не правильно понял статью — редукции проводятся независимо от закрытости или открытости термов

Неверно. Открытые термы невозможно редуцировать.

и это не «дополнительные правила типизации» — используется ровно то что было написано в определении _+_:

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

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

у тебя будут происходить обычные произвольные редукции термов во время проверки типов.

Ну когда там стоит constexpr - конечно, будут, это ведь обычные редукции омеги (те самые типы-синглтоны и операторы над типами - они и редуцируются), а в агде есть омега. Зависимые типы вообще ничего такого не требуют, потому непонятно, зачем мы это обсуждаем?

В самом деле — попробуй что-нибудь на агде, кроме type-level ничего нет

Ну сколько ты еще врать-то будешь? Опять выдумал свою хуйню и долбишь как баран.

Но вообще без них никак — это фундаментально в зависимых типах.

В омеге это фундаментально. В чистой dependent-type нельзя вообще редуцировать тип array<1+2>.

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

У тебя тоже «my»

У меня не my, я пользуюсь стандартным определением зависимых типов. Которые бывают П-типы и сигма-типы. Если в системе есть эти типы, то есть зависимые типы.

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

Ну как же нет? Есть П-типы. До тайпчека включительно. Хотя не совсем понимаю что значит фраза «до тайпчека включительно» - зависимые типы либо в принципе есть в языке либо их в принципе нет.

Там же всё известно во время компиляции (как с constexpr — не согласен? Примеры сюда :))

Да уже сотню раз приводился подобный пример:

f = λ x → let y = x in let z = x; a₁ = replicate {n = y} 1 in let a₂ = replicate {n = z} 2 in a₁ , a₂

а всякие вещи с открытыми термами ничем не отличаются от шаблонов (кроме того что чекаются).

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

Это как-то не очевидно, что системы типов друг от друга могут отличаться исключителньо тем, как и что там чекается?

Если на это внимания не обращать то у тебя все языки эквивалентны, внезапно. Мы можем взять любой язык, все в нем в компайлтайме вычислить и БИНГО!

Непонятно только, чего ты тогда вообще используешь для плюсов какие-то функции? Ну пиши одни только шаблоны. Чтобы все по-честноку - компайлтайм онли. И у тебя получится замечательная теория для программ, которые не работают.

#lang racket
(require (for-syntax racket/contract
                     racket/contract/region
                     racket/contract/parametric
                     syntax/parse/define
                     rnrs/base-6)
         (for-meta 2 (except-in racket
                                syntax-rules))
         rnrs/base-6)

(begin-for-syntax
  
  ;;; templates:
  (begin-for-syntax
    (define instance-hash (make-hash)))
 
  (define-simple-macro (define-template (name:id arg:id ...) (inner-args:id ...) body:expr ...)
    (define-simple-macro (name arg ... )
      #:do [(define args (syntax->datum #'(arg ...)))]
      #:with hidden (hash-ref! instance-hash args (syntax-local-lift-expression 
                                                   #'(let ()
                                                       (define/contract (name inner-args ...) body ...)
                                                       name)))
      hidden))
  ;;;
  
  ;;; equality:
  (define nat? exact-positive-integer?)
  
  (define/contract (== x y)
    (-> nat? nat? (-> any/c any))
    (assert (= x y))
    (λ (p) #t))
  ;;;
      
  (define (fact a)
    (if (= a 0)
        1
        (* a (fact (- a 1)))))
  
  (define/contract (factorial_5_eq_12_mult_10)
    (-> (== (fact 5) (* 12 10)))
    (void)) ;check
  
  #;(define/contract (factorial_5_eq_12_mult_9)
    (-> (== (fact 5) (* 12 9)))
    (void)) ;assertion failed
  
  (define-template (a_plus_0_eq_a a:nat) ()
    (-> (== a (+ a 0)))
    (void))
  
  (define-template (a_plus_1_eq_a a:nat) ()
    (-> (== a (+ a 1)))
    (void))
  
  ;;; ^ no checks :(
  
  (define x (factorial_5_eq_12_mult_10)) ; ok
  
  (a_plus_0_eq_a 100500) ; ok   
  #;(a_plus_1_eq_a 100500) ; assertion failed
  )

такие дела

Называется взял и запилил еще одну систему типов для ракетки.

Олсо, я смотрю ты везде юзаешь define-simple-macro вместо syntax-case.

Много профита? Есть ли смысл осилить эту конструкцию вместе с syntax-parse?

Много профита?

Много

Есть ли смысл осилить эту конструкцию вместе с syntax-parse?

Имеет. syntax-parse - мегаохуенная вешь

Называется взял и запилил еще одну систему типов для ракетки.

Там не система типов. Просто у quasimoto же вся программа выполняется в компайлтайме (всяких ИО и т.п. не ту же), вот я и захуярил все в begin-for-syntax с контрактами. Так то они должноы проверяться в рантайме во время объявления функции, когда контракты вычисляются, но тут они в +1 фазе вычисляются.

спасибо

Подумай.

f и f' в sup? редуцируются до одинаковой (метатеоретически) нормальной формы, понятное дело.

Давай.

Давай ты не будешь писать _каких-то отдельных_ программ которым _действительно_ не нужны редукции (их не видно, вообще ноль редукций это частный случай для β⋆, то есть transitive closure для бета-редукции), а рассмотришь кучу программ в зависимых типах которым редукция _нужна_ (строго больше нуля редукций, ну как sup?, 5!≡12*10 или a+0≡a).

Открытые термы невозможно редуцировать.

В очередной раз посылаю на the book (которая про LC, множество термов на которых определяется отношение редукции там просто множество термов (big-lambda), никакой закрытости — это отдельный подкласс (big-lambda-zero там, емнип)).

Ну и как бы — «уметь редуцировать открытые термы» (ну как агда) это строго больше «уметь редуцировать закрытые термы» (если это то что ты хочешь называть «бета-редукция»). И уж второе агда тем более умеет делать и делает — нет примеров закрытых термов которые бы не редукцировались у неё в типах (примеров открытых тоже нет, ну да ладно).

Озвучь хоть один пример редукции (как ты её понимаешь) которую нельзя провести в типах — нет такой, иначе это будут нерабочие зависимые типы.

Это как раз дополнительные правила типизации

Это счётное количество «дополнительных правил типизации» называется β-редукция — натурально, все вычисления на термах в наличии при установлении эквивалентности типов. То есть как в омеге наличествуют все «вычисления» на основе операций над типами (при установлении эквивалентности типов, так как типы можно применять к типам), так в зависимых типах есть все обычные вычисления на термах, то есть на основе обычных операций (функций) (тоже при установлении эквивалентности типов, так как типы можно применять к термам — LF).

Это же просто — омега, есть операции на типах и применения типов к типам — надо редуцировать типы при установлении их же эквивалентности, LF — есть применения типов к термам, так что нужно редуцировать ещё и термы обычной бета редукцией, но при установлении эквивалентности именно типов. Omega + LF — и то, и другое. Либо унифицировано как в агде.

Это две разные вещи (до унификации).

При этом

то есть если агда не сумеет «редуцировать» эти термы зависимые типы все равно останутся

тогда это будет как омега без редукций типов (в смысле TAPL), то есть непригодная штука.

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

Редукции как раз требуются. А вот твоё требование на «не constexpr» никак не фигурирует.

Да уже сотню раз приводился подобный пример

Вот каждую твою лямбду я перепишу как template в котором переменная будет параметром шаблона (возьмём для простоты только натуральные числа и size_t в качестве приближения, так как списки в C++ муторно городить), буду утверждать эквивалентность, так что вопрос к чему ты эту лямбду будешь применять — к чему бы ты её не применил, я так же применю шаблон к constexpr терму (и в отличии от лямбда куба тут даже Тьюринг-полнота будет), так что всё сведётся к IO, но в лямбда кубе нет IO, а единственный нормальный способ его добавить это через монаду (как в Agda и Coq), так что что-то изменится только внутри монады, снаружи всё останется как было.

Тут тоже примеров всё ещё нет.

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

Это ты не понимаешь, но я уже привык — fix-в-SystemF-пишется-но-не-типизируется, элементы-у-термов-как-термы-у-типов, ADT-Maybe/List-не-функторы-и-не-монады, что там ещё... Вот теперь ещё отсутствие редукций в зависимых типах :) (в треде была ссылочка — http://oxij.org/note/BrutalDepTypes/, для ленивых).

Ну как же нет? Есть П-типы. До тайпчека включительно. Хотя не совсем понимаю что значит фраза «до тайпчека включительно»

Ну так и в C++ есть подобие П-типов (сум нет, как я понимаю). Фраза значит, что у нас нет «рантайма» — чекнули теоремку (нужен только тайпчек) и разошлись, запускать нечего, либо есть чего в монаде, но нас это не касается (как и нашей системы типов).

такие дела

Ну и достаточно мило, чего :)

Давай ты не будешь писать _каких-то отдельных_ программ которым _действительно_ не нужны редукции

Ты видимо забыл разговор. Ты утверждаешь что надо редуцировать типовой терм, чтобы чекнуть. Я говорю, что агда прекрасно чекает типы без редукций.

Озвучь хоть один пример редукции (как ты её понимаешь) которую нельзя провести в типах

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

Но с точки зрения зависимых типов совершенно не важно написано у тебя array<a+0> или array<1+0> - в обоих случаях все прекрасно чекнется без редукции. Разница только в том, что в первом случае и ежу понятно, что никакой редукции нету и быть не может, а во втором - это уже не столь очевидно, т.к. терм закрытый и его можно редуцировать. Но _не нужно_.

Это счётное количество «дополнительных правил типизации» называется β-редукция

И какой же такой бетаредукции соответствуют правила для типизации

f = λ x → let y = x in let z = x; a₁ = replicate {n = y} 1 in let a₂ = replicate {n = z} 2 in a₁ , a₂

LF — есть применения типов к термам, так что нужно редуцировать ещё и термы обычной бета редукцией

Так в том и дело, что не нужно. Более того - это невозможно, как в выше приведенном примере! И между тем, все чекается - без редукции!

тогда это будет как омега без редукций типов (в смысле TAPL), то есть непригодная штука.

При чем тут вопрос пригодности? Мы говорим о том, что является системой с зависимыми типами, а что нет, а не о пригодности чгео бы то ни было.

Редукции как раз требуются.

Не требуются.

А вот твоё требование на «не constexpr» никак не фигурирует.

Что, прошу прощения? Вполне явно фигурирует. Найди мне хоть одно определение зависимых типов, где говорится, что П-тип может зависит только от constexpr, а не от _любых_ термов определенного типа.

Вот каждую твою лямбду я перепишу как template в котором переменная будет параметром шаблона

И оно тогда не будет чекаться.

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

А ни к чему не буду. Лямбда - это и есть результат, все программа отработала.

к чему бы ты её не применил, я так же применю шаблон к constexpr терму (и в отличии от лямбда куба тут даже Тьюринг-полнота будет), так что всё сведётся к IO, но в лямбда кубе нет IO, а единственный нормальный способ его добавить это через монаду (как в Agda и Coq), так что что-то изменится только внутри монады, снаружи всё останется как было.

По такой логике любой язык обладает зависимыми типами

Тут тоже примеров всё ещё нет.

Уже сто раз пример приводился с открытым термом. Который ты на плюсах не напишешь.

Ну так и в C++ есть подобие П-типов

Так в том и дело, что нету. П-тип в котором результат типа не зависит от аргумента - это _по определению_ обычный функциональный тип. А в плюсах ты пытаешься задать П-тип шаблоном. Но шаблон - это не обычная функция. Если считать П-типы шаблонами, то тогда ты вообще не имеешь права в плюсах использовать простые функции.

Фраза значит, что у нас нет «рантайма»

Значит и статической типизации нету.

Ну и достаточно мило, чего :)

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

Я говорю, что агда прекрасно чекает типы без редукций.

Но она не чекает без них sup?, 5!≡12*10 и a+0≡a. Как и все прочие программы которые могут задействовать в типах произвольные вычисления.

я тебе показываю пример где агда все прекрасно чекает ничего не редуцируя, при том редукция по-твоему там очевидно нужна.

Если для проверки какой-то конкретной программы редукция не нужна — ради бога. Но я показываю примеры где она нужна. В общем случае и для множества конкретных же программ она нужна. То есть вообще на уровне системы типов.

Твоя риторика это как рассуждать про то что для всех целых чисел x и y имеет место быть x * y = 0, потому что, видите ли, при x = 0 (ты нашёл _одну_ программу без редукций) это так. Ну или «все вороны белые». Рассматривай общий случай.

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

Так оно любых, но _некоторого_ набора типов. В ATTAPL сказано, что есть T t (типы к термам), при этом множество типов никак не оговорено — может у нас чистый и тотальный лямбда-куб и полностью constexpr — теоретико-доказательной силы и CH это не отменяет, а может у нас монада IO (чтобы чистоту не ломать), тогда нужно думать как поселять в ней чистые функции и будут ли образовываться типы динамически или всё будет сильно restricted в этой IO.

И оно тогда не будет чекаться.

Ну то есть если где-то валяется closed source чекер шаблонов то всё тут же становится ок? По факту плохие программы не доживут до рантайма (чекнутся после раскрытия) что с ним, что без него.

А ни к чему не буду.

Вот и у меня — просто template с обычной такой индексацией, типа concat для std::array.

Уже сто раз пример приводился с открытым термом. Который ты на плюсах не напишешь.

Пиши вместо sym === lambda (x : T). U[x] — template <T x> ... sym() { U[x] } и sym(T[...]) — sym<T[...]>(). Что ещё нужно?

По такой логике любой язык обладает зависимыми типами

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

Значит и статической типизации нету.

У тебя как-то отрицание ради отрицания.

Всё есть, суть в теоретико-доказательной силе системы типов как _синтаксического_ средства, равно как и в её непротиворичивости и CH.

Если считать П-типы шаблонами, то тогда ты вообще не имеешь права в плюсах использовать простые функции.

И соответствующее подмножество из шаблонов и constexpr функций тогда чем будет? Имею я право видеть в индексации П-типы?

Но она не чекает без них sup?

Как это не чекает? Все прекрасно чекает.

Но я показываю примеры где она нужна.

Покажи хоть один.

Так оно любых, но _некоторого_ набора типов.

Для какого некоторого?

В ATTAPL сказано, что есть T t (типы к термам), при этом множество типов никак не оговорено

Вполне оговорено. Термы являются типами. Нигде не написано, что типами являются «подмножества» термов.

По факту плохие программы не доживут до рантайма (чекнутся после раскрытия) что с ним, что без него.

Так в том и дело, что нету никакого раскрытия. Программа - это сам шаблон. Неинстанцированный. И он вообще не будет чекнут - никогда.

Пиши вместо sym === lambda (x : T). U[x] — template <T x> ... sym() { U[x] } и sym(T[...]) — sym<T[...]>().

Ну то есть как я и сказал - ты предлагаешь заменить все функции шаблонами, а обычных функций не будет вовсе. То есть в любом языке есть зависимые типы, с чем вас и поздравляю.

Всё есть, суть в теоретико-доказательной силе системы типов как _синтаксического_ средства, равно как и в её непротиворичивости и CH.

Любой динамический язык равен по доказательной силе твоей системе. Что дальше?

И соответствующее подмножество из шаблонов и constexpr функций тогда чем будет?

А это весь твой язык и есть. У тебя же кроме шаблонов и сонстекспр ничего нет - ты больше ничего не имеешь права использовать.

Видишь ли, в чем дело - в полиморфном исчислении у нас две лямбды: большая (обычные ф-и с обычными аргументами-значениями) и малая (полиморфные функции с типовыми аргументами). Им в плюсах соответствуют обычный функции и шаблоны. В зависимых типах ситуация другая - там только _одна_ лямбда - это П-лямбда. Обычная функция - это частный случай П-лямбды (именно _по-этому_ ты должен уметь применять любой терм - не только констекспр - просто потому что функцию ты можешь применять не только к констекспр, если ты ограничиваешься констекспрами, то оказывается, что в твоем языке нету типов для обычных функций). В исчислении зависимых типов мы принципиально не можем отличить тип Int -> Int (обычный функциональный тип) от forall (A:Int).Int (полиморфный тип, в котором А - шаблонный параметр). В случае зависимых типов это один и тот же тип _по определению_: П_(A:Int)Int. Соответственно template<A> Int f и int f(x:int) - имеют один тип. Но в плюсах это не выполняется. Именно в этом то и суть зависимых типов - взаимопроникновение компайлтайма и рантайма. Если ты ограничиваешь систему отсутствием компайлтайма, как ты предлагаешь (делать вычисления только на шаблонах) то и взаимопроникновения никаокго, конечно же, не будет.

И соответствующее подмножество из шаблонов и constexpr функций тогда чем будет?

Забыл, собственно, ответить на сам вопрос. Оно будет простой нетипизированной лямбдой. Ну или простой типизированной лямбдой - если с концептами.

Как это не чекает?

Там две произвольных разных (f и f') функции с двух сторон, чтобы проверить что они «равны» (в смысле refl) нужно редуцировать их — в emacs mode такое вычисление доступно по C-c C-n (от normal form), всё что делает C-c C-n можно делать с помощью C-c C-d (от deduce type) через прокси тип, то есть вычислять любые нормальные формы (открытых и закрытых термов / типов) во время проверки типов, это же вычисление делает и тайпчекер, это часть процесса унификации.

Покажи хоть один.

sup?, 5!≡12*10 и a+0≡a есть на этой странице. А вообще, если говорить про _≡_ (который обычный индуктивный тип), то в

пример : любое-вычисление-1 ≡ любое-вычисление-2
пример = refl

типы можно проверить только проведя любое-вычисление-1 и любое-вычисление-2 до (предполагаемой общей) нормальной формы — прямо во время проверки типа. А как иначе? refl : a ≡ a, так что нужно как-то установить что LHS и RHS это именно этот один и тот же «a», без редукций это не известно.

(В С++ есть нечто похожее — IndexedType<any_constexpr_computation(...)> нельзя инстанцировать не проведя вычислений.)

http://www.csie.ntu.edu.tw/~b94087/ITT.pdf‎

The rules of computation (execution) of the present language will be such that the computation of an element a of a set A terminates with a value b as soon as the outermost form of b tells that it is a canonical element of A (normal order or lazy evaluation).

two arbitrary elements a, b of a set A are equal if, when executed, a and b yield equal canonical elements of A as results.

This is the meaning of a judgement of the form a = b ∈ A.

Это называется definitional equality — equivalence включает computational rules (figure 2-2 в ATTAPL, опять же — вспоминаем (из TAPL) про то как редукции типов возникают в омеге при том же установлении их equivalence, в LF подобным образом, только на основе того что есть T t (а не T S), то есть редуцируются уже термы к которым применяются типы), в случае строгой нормализации это ничего не ломает, возможно и предпочтительно.

Для какого некоторого?

Заданного системой типов. В голой LF это «переменная», «Pi» и «Pi-App». Ещё раз скажу — я считаю что «голая LF» и подобные системы тупо ничего не знают про compile/run-time, так что зависит от того как будет выглядеть реальная система типов и реализация системы эффектов — можно ограничить типы Pi/Pi-App типами с constexpr квалификаторами — сигнатуры определённого (свойственного зависимым типам) вида всё равно в языке _будут_, а вот в языке _без_ зависимых типов их не найти вообще; или не ограничивать, либо, если у нас система эффектов в виде не запускаемой монады — можем неявно считать, что всё снаружи монады constexpr и стирать этот квалификатор при попадании в монаду.

Термы являются типами.

Так и написано? Приведи цитату. И скажи — как какой-нибудь терм, вроде «5», может вдруг оказаться типом (если есть _индуктивный_ Proxy с сигнатурой Nat -> Set, то существует Proxy 5, то есть как раз T t, населён (или нет) этот Proxy 5 чем-то своим, то есть от того что типы можно индексировать и применять к термам каких-то типов термы типами не становятся (+ нужно иметь в виду, что некая эквивалентность термо-типов прослеживается только в вершине, а нас, может быть, только LF или её разновидности интересуют)).

И он вообще не будет чекнут - никогда.

Ну чекни в уме, опять же — свойства системы у тебя вдруг оказываются зависимы от существования каких-то внешних по отношению к ней вещей (рантайма с IO для агды или чекера шаблонов для плюсов).

То есть в любом языке есть зависимые типы, с чем вас и поздравляю.

Очевидно, 1) это должен быть статически типизированный язык, 2) в нём должны существовать определённые вещи и, соответственно, сигнатуры определённого вида — такие вещи как std::array, concat для него, fin, eq и т.п., при этом _правильно_ работающие с _синтаксическими_ проверками этой правильности на уровне этой самой системы типов. Распространённого языка общего назначения удовлетворяющего 1 и 2 кроме C++ я не знаю — DML/ATS не распространены, Coq/Agda/etc. не вполне общего назначения.

К слову, вот в C++ есть «параметрический полиморфизм», сигнатура std::vector это как минимум <typename> -> typename — параметризация типа типами и применение _конструктора типов_ std::vector к типам (все элементы вида typename в C++ это «consttype», то есть точно известные во время компиляции типы (подобно тому как constexpr — точно известные термы)). И тут ты можешь сказать, что и этого нет — Равные длины векторов, типы должны быть точно известны во время компиляции.

Оно будет простой нетипизированной лямбдой. Ну или простой типизированной лямбдой

Не знаю. Я вижу статически типизированный язык в котором у вещей бывают сигнатуры например такого вида — array : <typename, size_t> -> typename; concat : <a : size_t, b : size_t> (array<T, a>, array<T, b>) -> array<T, a + b>, явно в дополнение к параметризации типов типами есть ещё и индексация типов термами и применение типов к термам, то что и тут есть ограничение на compile-time only меня не смущает, можно ещё так записать — array : (consttype typename, constexpr size_t) -> typename; concat : (a : constexpr size_t, b : constexpr size_t, array(T, a), array(T, b)) -> array(T, a + b) — будет единственный Pi вместо стрелки как ты хочешь, но с теми же ограничениями — применение параметризированных/индексированных конструкторов типов к типам и термам (из под Pi) будет работать только для видов и типов с consttype/сonstexpr квалификаторами (похоже на омегу, да, но если поднять все constexpr термы в типы, все типы в виды, вместе со всеми отношениями типизации для них — в обычной омеге этого нет, виды устроены проще).

Там две произвольных разных (f и f') функции с двух сторон, чтобы проверить что они «равны» (в смысле refl) нужно редуцировать их

Очевидно, что не нужно, т.к. редуцировать их нельзя.

5!≡12*10 и a+0≡a есть на этой странице.

И где тут редукция? Особенно во втором случае, с открытым термом, который вообще редуцировать нельзя.

Ещё раз скажу — я считаю что «голая LF» и подобные системы тупо ничего не знают про compile/run-time

Проблема в том, что они знают. Разделение рантайм/компайлтайма есть в определении этих систем. Оно есть в самом определении «статической системы типов».

Заданного системой типов.

Не получается задать.

В голой LF это «переменная», «Pi» и «Pi-App».

Это не типы.

Так и написано?

Так и написано. Это строго оговорено в определении П-типа.

Приведи цитату.

More formally, given a type A:U in a universe of types U, one may have a family of types B: A -> U  which assigns to _each term_ a:A a type B(a):U. A function whose codomain varies depending on its argument is a dependent function, and the type of this function is called a dependent type, dependent product type or pi-type. For this example, the dependent type would be written as
П_(x:A)B(x)
If B is a constant, the dependent type becomes an ordinary function A -> B. That is, П_(x:A)B is judgementally equal to the function type A -> B.

поскольку обычный функциональный тип есть П-тип, то типовой аргумент П-типа может быть всем тем, чем может быть обычный аргумент функции - то есть _любым термом_.

И скажи — как какой-нибудь терм, вроде «5», может вдруг оказаться типом

Он и не оказывается типом (формально). Просто если у нас зависимые типы без полиморфизма, то ф-я в качестве аргумента может принимать как тип, так и терм. По-этому нету разницы между типами и термами (и, соответственно, между типами и кайндами, если добавим еще и high-rank). Точнее - типы это термы типа Universal, а с другой стороны - термы это типы кайнда не Universal.

Ну чекни в уме, опять же — свойства системы у тебя вдруг оказываются зависимы от существования каких-то внешних по отношению к ней вещей (рантайма с IO для агды или чекера шаблонов для плюсов).

Нет, не оказываются. И при чем тут вообще ИО? Никакого ИО мы не рассматирваем ,считаем что его вообще нету. Чтобы чекнуть в уме - у меня должна быть система типов согласно которой я должен чекать. А в нашем случае ее нет. Потому и не чекается ничего. Если чекнется - это будет уже _другая_ система типов.

Очевидно, 1) это должен быть статически типизированный язык

А как ты сформулируешь понятие «статически типизированный язык» если у тебя нету понятий компайлтайма и рантайма?

2) в нём должны существовать определённые вещи и блаблабла

Смотри - либо ты отказываешься от понятий рантайма/компайлтайма и тогда любой (в том числе динамический) ЯП имеет зависимые типы, либо ты не отказываешься, но тогда ВАЖНО когда происходят редукции, а когда - тайпчек. И у тебя не получится уже «выполнить программу во время тайпчека».

Распространённого языка общего назначения удовлетворяющего 1 и 2 кроме C++ я не знаю

c++ не удовлетворяет пункту 2 - в нем нельзя написать сигнатуру зависимого типа и соответственно чекер проверку зависимых типов не поддерживает (то есть зависимых типов нету в системе типов плюсов, потому что в системе типов плюсов есть то и только то, что чекается чекером).

К слову, вот в C++ есть «параметрический полиморфизм»

Мы уже говорили о том, что параметрического полиморфизма в с++ нету. Есть макроподстановка, которая ведет себя _похожим_ на параметрический полиморфизм образом. Не более того.

Не знаю.

А что тут знать? Все что ты можешь написать на шаблонах пишется на простой типизированной лямбде. С другой стороны, все, что ты можешь написать на простой типизированной лямбде, пишется на шаблонах. Вывод сам проделаешь?

Я вижу статически типизированный язык в котором у вещей бывают сигнатуры например такого вида — array : <typename, size_t> -> typename;

Пишется в простой типизированной лямбде.

concat : <a : size_t, b : size_t> (array<T, a>, array<T, b>) -> array<T, a + b>

И это пишется в простой типизированной лямбде.

явно в дополнение к параметризации типов типами есть ещё и индексация типов термами и применение типов к термам

Чего, прошу прощения? Ты в _простой_ (не полиморфной!) типизированной лямбде мало того что обнаружил параметризацию типов типами (которой там, конечно же, нет, иди читай определение простой типизированной лямбды), но еще и индексацию типов термами, которой там и близко не было!

Но сигнатурами чего на само деле были твои примеры? Очень просто - примерами индексации термов термами. То есть примерами обычных функций.

array : (consttype typename, constexpr size_t) -> typename; concat : (a : constexpr size_t, b : constexpr size_t, array(T, a), array(T, b)) -> array(T, a + b) — будет единственный Pi вместо стрелки как ты хочешь, но с теми же ограничениями — применение параметризированных/индексированных конструкторов типов к типам и термам (из под Pi) будет работать только для видов и типов с consttype/сonstexpr квалификаторами

Как ты интересно сказал про «квалификаторы». Что такое эти квалификаторы? Явно не типы. И не кайнды. И вообще у тебя не получится сформулировать корректную систему типов с такими квалификаторами.

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

Как нет? Есть.

виды устроены проще

Ничем не проще. Вид - это тип типа, напрямую. Виды это типы для надлежащего исчисления. Потому они не могут быть устроены проще типов - они и есть типы.

Очевидно, что не нужно, т.к. редуцировать их нельзя.

Можно — что в обычном лямбда исчислении (см. Barendregt — 3 глава, отношение редукции определяется на множестве всех лямбда-термов (открытых и закрытых), которое обозначается как Λ (2 глава), множество закрытых термов обозначается как Λ⁰ — отношение редукции задаётся не на нём, хотя вполне на него сужается), что в агде:

f = λ x → let y = x in let z = x; a₁ = replicate {n = y} 1 in let a₂ = replicate {n = z} 2 in a₁ , a₂

-- C-c C-n f (i.e. normal form of `f`)
-- =>
-- λ x → replicate 1 Σ., replicate 2

f′ : (x : ℕ) → Vec ℕ x × Vec ℕ x
f′ = λ x → replicate 1 , replicate 2

-- C-c C-n f′
-- =>
-- λ x → replicate 1 Σ., replicate 2

record Proxy {A : Set} (_ : A) : Set where

check-f : Proxy f
check-f = record {}

-- C-c C-d check-f (i.e. type of `check-f`)
-- =>
-- Proxy (λ x → replicate 1 Σ., replicate 2)

check-f′ : Proxy f′
check-f′ = record {}

-- C-c C-d check-f′
-- =>
-- Proxy (λ x → replicate 1 Σ., replicate 2)

-- C-c C-n Proxy f (i.e. normal form of _type_ `Proxy f`)
-- =>
-- Proxy (λ x → replicate 1 Σ., replicate 2)

-- C-c C-n Proxy f′
-- =>
-- Proxy (λ x → replicate 1 Σ., replicate 2)

И где тут редукция?

5!≡12*10 : 5 ! ≡ 12 * 10
5!≡12*10 = refl

-- C-c C-n 5 !
-- =>
-- 120

-- C-c C-n 12 * 10
-- =>
-- 120
 
-- C-c C-d 5!≡12*10
-- =>
-- 120 ≡ 120

-- C-c C-n 5 ! ≡ 12 * 10
-- =>
-- 120 ≡ 120

Особенно во втором случае

Я уже два раза рассказывал про то как работает индукция (рекурсия) с зависимым паттерн-матчингом:

a+0≡a : ∀ a → a + 0 ≡ a
a+0≡a 0 = refl
-- 
-- Base case, a ~ 0:
-- 
-- C-c C-n 0 + 0 ≡ 0
-- =>
-- 0 ≡ 0
-- 
-- C-c C-d refl
-- =>
-- _x_76 ≡ _x_76
-- 
-- s.t. refl : 0 ≡ 0 is w.t.
-- 
a+0≡a (suc a) = cong suc (a+0≡a a)
-- 
-- Step case, a ~ suc a:
-- 
-- C-c C-n λ a → suc a + 0 ≡ suc a
-- =>
-- λ a → suc (a + 0) ≡ suc a
-- 
-- C-c C-d λ a → cong suc (a+0≡a a)
-- =>
-- (a : ℕ) → suc (a + 0) ≡ suc a
-- 
-- C-c C-n (a : ℕ) → suc (a + 0) ≡ suc a
-- =>
-- itself
-- 
-- s.t.
-- 
-- ... | suc a = cong suc (a+0≡a a) <- induction/recursion in (dep.) p.m. case.
--               ^ : a + 0 ≡ a
--               i.e. w.t. as well.

Оно есть в самом определении «статической системы типов».

Вот LF это «теория типов», а не «система типов» — ей действительно всё равно, в её абстрактных рамках индексация действительно проводится «любыми» термами, безотносительно каких-то стадий (стадий нет, есть отношения на множествах термов, типов и т.п. — где у Barendregt или Lambek & Scott стадии?), но конкретная «система типов» вместе с реальным языком с «системой эффектов» вполне могут быть построены вокруг LF так, что всё ей (LF) свойственное будет работать исключительно с constexpr типами, или «хуже» — это может быть голый пруф/тайп-чекер LF без рантайма (но с этими самыми тотальными редукциями термов в типах, считаем за CTFE) и он _будет_ реализацией «теории типов» LF.

Это не типы.

http://i.imgur.com/C3a9Bem.png — я про «types:».

More formally

Ты приводишь что я просил? То есть «Термы являются типами»?

Ну ладно, ты всё ещё говоришь про то, что индексация должна проводится «любыми термами». Я этого не понимаю.

Никакого ИО мы не рассматирваем

Ну вот и чекай concat и т.п. как в той же агде — из ИО ничего не прилетает, значит всё известно, проблем нет?

А как ты сформулируешь понятие «статически типизированный язык» если у тебя нету понятий компайлтайма и рантайма?

Но они есть — в C++/D/Agda. Как и редукции термов в типах. В Agda можно считать, что compile-time это проверка типов (с тотальными редукциями), потом (тотальное же) вычисление нормальных форм, в том числе терма main типа IO T, а runtime это интерпретация этого терма main самим RTS (с частичными вычислениями).

но тогда ВАЖНО когда происходят редукции, а когда - тайпчек

А когда происходит вычисление constexpr функций в C++? Или CTFE в D?

пишется в простой типизированной лямбде

Этого тоже не понимаю. Вот в Haskell 2010 не пишется — пробовали же вроде тут.

Что такое эти квалификаторы? Явно не типы. И не кайнды. И вообще у тебя не получится сформулировать корректную систему типов с такими квалификаторами.

Квалификаторы это проблема, вообще-то — следствие отсутствия системы эффектов / patriality (раз мы хотим вычисления в compile-time, нужно как-то отражать тотальность, аналогично чистоте) в языке, а с ними всё уже вполне формулируется (грубо говоря constexpr T -> T; T const[&] -> IO T; T[&] -> IO (Ref T), снаружи IO/Partiality у нас применимо CTFE).

Ничем не проще.

http://en.wikipedia.org/wiki/System_F#System_F.CF.89

Точнее

a+0≡a (suc a′) = cong suc (a+0≡a a′)
-- 
-- Step case, a ~ suc a′:
-- 
-- C-c C-n (a′ : ℕ) → suc a′ + 0 ≡ suc a′
-- =>
-- (a′ : ℕ) → suc (a′ + 0) ≡ suc a′
-- 
-- C-c C-d λ (a′ : ℕ) → cong suc (a+0≡a a′)
-- =>
-- (a′ : ℕ) → suc (a′ + 0) ≡ suc a′
-- 
-- s.t. λ (a′ : ℕ) → cong suc (a+0≡a a′)
--      : (a′ : ℕ) → suc (a′ + 0) ≡ suc a′
--    <=β (a′ : ℕ) → suc a′ + 0 ≡ suc a′
-- w.t. as well.

так же как в base case — нормализируем (бета) утверждение (тип) и выводим тип доказательства (терм), если они совпадают (альфа), то w.t. Хотя всё это часть более общего процесса унификации.

Я уже два раза рассказывал про то как работает индукция (рекурсия) с зависимым паттерн-матчингом:

Ты реально глупый? Это не редукция. Для интереса попробуй редуцировать не а+0, а а+1.

но конкретная «система типов» вместе с реальным языком с «системой эффектов» вполне могут быть построены вокруг LF так, что всё ей (LF) свойственное будет работать исключительно с constexpr типами

В том и дело, что не может. Потому что _по определению_ она должна работать со всеми термами.

и он _будет_ реализацией «теории типов» LF.

Как и любой динамический язык.

Ты все никак не поймешь? Либо у тебя в динамике есть зависимые типы, либо у тебя нету их ни в динамике ни в плюсах.

Ты приводишь что я просил? То есть «Термы являются типами»?

Ну да.

Ну ладно, ты всё ещё говоришь про то, что индексация должна проводится «любыми термами». Я этого не понимаю.

Чего ты не понимаешь? У тебя в определении четко написано «индексация должна проводиться любыми термами». Более того - на этом факте и основана консистентность всей теории, т.к. если мы ограничим набор термов, то вся система типов сразу разваливается.

Вообще, мне непонятна твоя логика - именно возможность индексации ЛЮБЫМИ (не констекспр) термами составляем сущность систем с зависимыми типами. Рассматривать систему с зависимыми типами без индексации любыми термами - это как рассматривать полиморфную систему типов, в которой каждый полиморфный тип может быть инстанцирован единственным аргументом. Ну и что, что такая система по свойствам в точности будет совпадать с обычным типизированным исчислением? Формально то оно будет параметрическим (ну, по-твоему, нормальным людям понятно, что не будет)!

Ну вот и чекай concat и т.п. как в той же агде — из ИО ничего не прилетает, значит всё известно, проблем нет?

Не, все ок - пишу твой concat в обычной типизированной лямбде, все чекается, все работает. Я могу теперь утверждать, что в обычной типизированной лямбде есть зависимые типы?

Но они есть — в C++/D/Agda.

Откуда у тебя в плюсах взялся рантайм, если ты имеешь право писать только шаблоны и контекспры? У тебя в рнатайме ничего не выполняется, значит и рантайма нету.

А когда происходит вычисление constexpr функций в C++? Или CTFE в D?

Вычисление констекспр в с++ и D - это метапрограммирование, оно не связано с тайпчеком никак.

Этого тоже не понимаю.

Чего ты не понимаешь?

Вот в Haskell 2010 не пишется — пробовали же вроде тут.

Вариант из плюсов пишется в любом языке вообще (даже динамическом), вариант из агды - в любом языке со статической типизацией (простая типизированная лямбда). Что тебе тут непонятно? Все люди спокойно во всех языках пользуются функцией concat, а ты не веришь что ее можно написать?

Квалификаторы это проблема, вообще-то — следствие отсутствия системы эффектов

Твои квалификаторы совершенно никак не связаны с эффектами. Они просто делают любую систему типов противоречивой самим фактом своего наличия.

http://en.wikipedia.org/wiki/System_F#System_F.CF.89

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

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

Ты реально глупый?

Серьёзно? Под нос суют же — на, делай _любые_ редукции закрытых (если так хочешь только их) термов в Proxy типе во время проверки типов (или говори конкретно какое тотальное вычисление не можешь провести в это время — а то нет такого). Редукции открытых термов показывают, но всё ещё никак. Ну и изначально в MLTT definitional equality / a = b : T judjment предполагает вычисления, о чём была цитата.

Для интереса попробуй редуцировать не а+0, а а+1.

И? Установившийся тип выражения не совпадёт с редуцированным типом утверждения — forall a. a + 1 = a не тайпчекнется, как и полагается.

В остальном опять началась демагогия и «аналогии». Есть теория типов с Pi, Pi воплощается в системе типов для набора типов A, для другого набора B он не работает на уровне правил типизации (так и хотим в контекстах — типы для Pi из A), подмножество языка с такой системой над типами из A будет моделью для теории типов с Pi, то есть действие этой теории распространяется именно на это подмножество, остальное B нас не интересует. Аналогия с полиморфизмом для одного инстанса не годная — Pi ведь работает не для одного типа, а для многих, в т.ч. Pi-абстракций и аппликаций типов вокруг этих многих, как на картинке про LF. Абстрактная теория говорит именно про все термы типов этого множества A (универсум теории), никаких рантаймов-компайлтаймов она не знает — это дело реализации как воплощать и расширять такую теорию из лямбда-куба не constexpr вещами, системами частичности, эффектов и т.п. (и 100% распространённых ЯП общего назначения не умеют этого делать, то есть теорию таки ломают).

Тезис — ещё раз, сделай себе голый чекер LF, полностью constexpr, зависимые типы теории LF есть, обычная статическая типизация есть, Curry-Howard и proof-strength есть, номинальная непротиворечивость есть, особой общности с динамикой нет, рантайма нет, хотя можно приделать монадами (чтобы ничего не сломать). Agda и Coq (будучи изначально пруф-ассистентами) так развивались — а «я чиселку из stdin прочитал, а тип не создаётся динамически!1» крайне вторично.

Понятно, конечно, что LF и шаблоны C++ это, мягко говоря, различные вещи, но я нахожу выделение понятий параметризации (в духе полиморфизма), индексации (в духе зависимых типов) и атрибутов (ad-hoc) полезным.

Про concat тоже нечего сказать — как-то обсуждаемый concat должен быть именно таким, а у тебя вдруг «люди спокойно во всех языках пользуются функцией concat, а ты не веришь что ее можно написать?» — man статическая типизация и std::array (отличие от std::vector, например)?

Тезис — давай на C/PHP/Haskell2010/R3RS свой concat, будет смешно считать их эквивалентными :)

Вычисление констекспр в с++ и D - это метапрограммирование, оно не связано с тайпчеком никак.

Вот и в агде — «метапрограммирование», только связанное с тайпчеком (ну и как бы нет, в плюсах тоже — редуцировалось constexpr вычисление в терм для которого нет специализации — зафейлилась компиляция).

По-этому зависимые типы есть в агде, но нету в плюсах.

А в Agda1 (там голый тайпчек был, «обычных функций» нет)?

А в ATS (там есть различие statics и dynamics — как в плюсах)?

Редукции открытых термов показывают, но всё ещё никак.

Так ты не показал ни одной редукции открытого терма

И? Установившийся тип выражения не совпадёт с редуцированным типом утверждения — forall a. a + 1 = a не тайпчекнется

Ты бредишь? При чем тут тайпчек forall a. a + 1 = a? Никакого равенства вообще нету, есть только a+1. Давай, редуцируй.

В остальном опять началась демагогия и «аналогии».

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

Pi воплощается в системе типов для набора типов A, для другого набора B он не работает на уровне правил типизации

Ты под наборами А/В подразумеваешь констекспры/неконстэкспры? Еще раз, для особо одаренных - не существует способа отделить констекспры от неконстекспров на уровне типов. Быть констекспром или не быть констекспром - не типовое свойство, оно невыразимо в типизации. любая попытка прихуярить к твоей системе констекспр квалификаторы пустит типизацию по пизде.

Аналогия с полиморфизмом для одного инстанса не годная — Pi ведь работает не для одного типа, а для многих

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

Абстрактная теория говорит именно про все термы типов этого множества A (универсум теории), никаких рантаймов-компайлтаймов она не знает

Прекрасно, в этом случае любой динамический ЯП - имеет зависимые типы. Ты с этим согласен?

Тезис — ещё раз, сделай себе голый чекер LF, полностью constexpr, зависимые типы теории LF есть

Нету. Откуда они взялись? Еще раз - зависимые типы - это тогда и только тогда, когда подставляется любой (не только коснтекспр) терм. Более того - условие на подстановку констекспр терма в рамках правил типизации вообще неформулируемо. Поэтому неясно о чем вообще разговор.

Про concat тоже нечего сказать — как-то обсуждаемый concat должен быть именно таким, а у тебя вдруг «люди спокойно во всех языках пользуются функцией concat, а ты не веришь что ее можно написать?»

Не понял твоей претензии. Ты примел обычную функцию concat из языка с динамической типизацией. Очевидно такую функцию конкат легко написать. О чем ты вообще? Зачем ты привел ее в пример? Твоя функция не является вообще статически ипизированной.

man статическая типизация и std::array (отличие от std::vector, например)?

При чем тут статическая типизация если ты приводишь нетипизированный конкат?

Тезис — давай на C/PHP/Haskell2010/R3RS свой concat, будет смешно считать их эквивалентными :)

Обычный конкат из стандартной библиотеки. Он умеет все, что умеет твой конкат. Вот смотри:

> (define arr (vector 1 2 3)) ; arr имеет тип vector<3>
> (vector-ref arr 1) ; все ок, тайпчек походит
2
> (vector-ref arr 5)
vector-ref: index is out of range
  index: 5
  valid range: [0, 2]
  vector: '#(1 2 3)
;ошибка проверки типов
> (define arr2 (vector-append arr arr)) ; vector-append имеет тип vector<a> vector<b> -> vector<a+b>
> (vector-ref arr2 5) ; тайпчек проходит, arr2 имеет тип vector<3+3> = vector<6>
3
> (vector-ref arr2 7) ; ошибка типов
vector-ref: index is out of range
  index: 7
  valid range: [0, 5]
  vector: '#(1 2 3 1 2 3)

вот vector-append - это твой concat. можешь привести хоть один параметр по которому он, быть может, не соответствует тому, чего ты ждал? ;)

А в Agda1 (там голый тайпчек был, «обычных функций» нет)?

В зависимых типах обычная функция - ПО ОПРЕДЕЛЕНИЮ частный случай полиморфной. По-этому да, обычных ф-й нет. Они просто не нужны.

А в ATS (там есть различие statics и dynamics — как в плюсах)?

Если ATS позволяет совать не констекспр - значит они взаимозаменяемы, с точностью до синтаксического сахара.

Вообще, мне уже надоело.

Итак:

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

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

3. Нам известно, что плюсы не удовлетворяют вышеприведенному определению.

4. Кроме того, нам известно, что все, что можно написать на плюсах, можно написать на омеге (то есть зависимы типы не нужны)

5. И, с другой стороны, не все, что можно написать с зависимыми типами можно написать на омеге.

С КАКИМ ИМЕННО из этих утверждений ты споришь? Давай без аналогий. Четко и ясно.

Так ты не показал ни одной редукции открытого терма

А закрытого?

Начать с того, что ты называешь редукциями только редукции закрытых термов, так что должен спрашивать сначала про них (если они есть, то и твои «редукции» есть) — ну так вот я тебе и показал, что любой закрытый терм редуцируется. Если ты считаешь, что редукций (пусть хотя бы закрытых термов) нет, то тебе не составит труда привести пример закрытого терма не в нормальной форме который не редуцируется до нормальной — но ты не приведёшь, так как они редуцируются. Иначе получится Теория Типов которая не в состоянии доказать (= пруф/тайп-чекнуть принадлежность терма-доказательства к типу-утверждению) 2 + 2 = 4 (потому что она не хочет делать 2 + 2 => 4). Просто офигенная ТТ :)

Редукции открытых термов я тоже показывал. Ниже ещё раз покажу. Без них получится Теория Типов которая не может доказать forall a. a + 0 = a. Это при том, что в задумке MLTT как минимум мощнее PA (а вообще равносильна IZF/CZF).

есть только a+1. Давай, редуцируй.

Данный терм в нормальной форме. Так же как a, suc a, a + 0 или suc (a + 0). С другой стороны, вот примеры редукций открытых термов — 0 + a => a, 1 + a => suc a, a + (2 + 2) => a + 4 или suc a + b => suc (a + b). Поэтому для доказательства forall a. a + 0 = a мы разбираем «a» в PM — в base case получается 0 + 0 = 0 => 0 = 0, что тривиально тип refl, а в step case — suc a + 0 = suc a => suc (a + 0) = suc a, что выражается рекурсивно (индукция!) через предыдущий case. И ещё раз напоминаю, что _=_ это обычный индуктивный тип, подобные ситуации и редукции возникают повсеместно.

* Тут везде считается, что N : Set; 0 : N; suc : N -> N это индуктивный тип, а _+_ определён на нём рекурсивно (индуктивно) через левый аргумент, то есть _+_ : N -> N -> N; 0 + y => y; suc x + y => suc (x + y) (вспоминаем копипасту про категорию с объектами-типами, стрелками-функциями и 2-стрелками-классами-эквивалентности-редукций :)).

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

Ты хоть одну ссылку привёл? Ты берёшь понятие из математической логики (http://ncatlab.org/nlab/show/dependent product#references_34) и переосмысливаешь его в соответствии со своей программистской интуицией в расчёте на какой-то типичный ЯП («выдрал из системы все интересное, ради чего система создавалась» — ты решил для чего она создавалась, ага, не создавалась она для того чего ты ожидаешь — бери для примера любой пруф-ассистент на основе зависимых типов образца 80-ых/90-ых), при этом отвергаешь другие возможные существующие модели.

Ты под наборами А/В подразумеваешь констекспры/неконстэкспры?

Вообще constexpr это костыль. В любой системе лямбда куба (со связанной непротиворечивой теорией с CH) всё по определению «constexpr», без костылей (точнее, это единственный известный мне вариант) у нас будет система лямбда куба + незапускаемые монады Partiality и IO.

Нету. Откуда они взялись?

В LF (синтаксис + отношение типизации + отношение эквивалентности) нет зависимых типов, так и запишем. И я считаю, что в LF всё по определению constexpr (чисто, тотально, без IO, то есть известно на момент «компиляции»), да.

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

Я жду что при попытке населить

template <typename T, size_t a, size_t b>
std::array<T, a + b>
concat(std::array<T, a> const& x, std::array<T, b> const& y);

программой которая возвращает пустой массив или вообще массив длинна которого не есть a + b (при аргументах с длинами a и b — зависимость! пусть a и b и compile-time known) мы получим ошибку времени проверки типов. То есть ты в сигнатуре утверждаешь факт о длинах, после чего чисто по построению (синтаксически) можно будет написать только программу которая соответствует этому факту. То есть _правильность_ — если теория (типов) говорит, что что-то _так_, то оно будет работать именно _так_ в модели (читай «рантайм» = RTS), без исключений. В динамическом языке ты ничего не утверждаешь, сигнатуры не пишешь и можешь сделать себе concat который возвращает всегда '() — в данном примере на C++ так не получится.

С КАКИМ ИМЕННО из этих утверждений ты споришь?

0. В теории типов все термы constexpr, поэтому мне не понятно требование на «любой терм». Ты хочешь ввести грязные функции как в C++, сломать теорию типов и потом что-то от неё требовать?

1. Допустим, но для любых термов каких типов, для всего универсума, а если он сломан?

2. Не вижу проблем в том чтобы конструкция не была универсальной. Исходное утверждение нужно понимать как «конкретные пи-типы формируются», что уже что-то (вообще у нас шаблоны, так что правильнее сказать «можно заставить прикидываться конкретными пи-типами в определённом подмножестве языка», но для простейших вещей вроде std::array и concat даже заставлять не нужно, и ещё — динамический язык с нормальными макросами тоже (теоретически) можно заставить, я не против).

3. А concat нам приснился :)

4. и 5. Мне не интересно есть или нет эквивалентность с омегой или её расширениями. Зачем мне делать ненужную искусственную интерпретацию (пусть значения это типы, пусть их типы это виды и так далее), когда всё и так понятно?

Два месяца прошло. «Эта музыка будет вечной.»