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

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

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

Оно +- везде так, в общем-то.

ДА нет - это плюсовое ооп. Ну в том же смоллтолковском все совсем не так.

Различия незначительны. Вот с функциональным программированием - они хоть как-то заметны.

А теперь вопрос на засыпку - и какое отношение модульная система имеет к декларативности языка? :)

Большое, если модульная система говно - нам приходится городить костыли вокруг нее, любой костыль недекларативин по определению.

Сейчас посмотрел - у меня в среднем 1 var на 0.9 клос. При чем из них большая часть в местах интероперабельности с жавалибами

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

Да, а их композиция в основном уже как бы нет.

Это как? Из средств композиции в ООП я знаю агрегацию, композицию, реализацию. Они все полностью декларативны.

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

Бес понятия, если честно, я в ней по-хорошему не копался.

Ну пусть на stdlib - дай ссылку на проект на скале, в котором по твоему мнению хороший код, можно несколько проектов.

пока что те примеры, что мне попадались на скале - это джава-стайл на стероидах.

Ну это как раз один из основных плюсов скалы - на ней можно писать как на улучшенной джаве.

И это (по крайней мере лично для меня) херово. Т.е. если это действительно так, то скала как язык мне не подойдет.

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

Это да, а где смотреть правильный скала код?

Вообще еще вопрос - что такое декларативность

Выше ответил на этот вопрос.

Я бы сказал, что декларативность - это абстракция, которая близка к предметной области и течет пренебрежимо мало.

Для любой области можно построить матмодель в привычных для нее способах выражения.

То есть для каждой задачи будет своя декларативность

И для каждой задачи свой язык? :)

Макросы - неплохой способ его генерить.

Любая селедка - рыба, но не любая рыба - селедка.

Что такое повышение декларативности?

Чего?

В общем случае - нет

Ну и вот с макросами в общем случае - нет. Смотри, программист занимается написанием термов, ну по факту. Макросы - инструмнет генерации термов. Но:

1. Писать я могу только plain-термы, то есть datum, как в общелиспе. С нормальной макросистемой я могу управлять термами полноценно - их source location, связываниями, свойствами и т.д.

2. В некотором смысле, следствие первого пункта - я могу сгенерить макросами такие термы, которые невозможно написать руками. Не сложно - а именно невозможно. Вообще никак.

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

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

Конечно.

Да ну, какая связь между классами и бойлерплейтом? Я б уж наоборот сказал, дефолтное ООП как раз зачастую заставляет бойлерплейт писать.

Декларативность для меня - это возможность изящно описать матмодель проблемы по своей форме максимально приближенно к _определению_ чем является, а не _что_ сделать.

Ну то есть то же самое, что и для меня.

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

Мне кажется декларативный язык именно что общего назначения

Это невозможно. По определению декларативный язык всегда заточен под задачу.

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

Он будет хорошо подходить для некоторых специализированных областей. И плохо - для всех остальных, очевидно.

Для любой области можно построить матмодель в привычных для нее способах выражения.

Для начала, конечно, надо разработать совершенно новый матаппарат и совершенно новую нотацию. С совершенно новым разделом математики. А так, да, можно :)

И для каждой задачи свой язык? :)

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

Макросы - неплохой способ его генерить.

Любая селедка - рыба, но не любая рыба - селедка.

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

С нормальной макросистемой я могу управлять термами полноценно - их source location, связываниями, свойствами и т.д.

Я не встречал этого на практике, нужно хотя бы пример - зачем оно нужно, допустим, какая польза от знания source location?

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

Можно пример?

Да ну, какая связь между классами и бойлерплейтом? Я б уж наоборот сказал, дефолтное ООП как раз зачастую заставляет бойлерплейт писать.

Для тех языков, в которых ооп является основной парадигмой программирования, и в которых еще есть остатки чисто процедурной - ооп играет роль уменьшателя копипасты, ну и макросы с ними - шаблоны++, например. Хотя ооп в борьбизме против копипасты (а точнее правильно это называется - реюз кодовой базы) мало чем помогает: в т.н. традиционных языках ооп в основном выполняет функцию модулей, из-за непродуманности самой модульной системы.

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

Это «в идеале», на практике же все пишут на джаве :)

Например, и ООП - это замечательная матмодель для многих задач.

Например? И ооп как где?

Мне кажется декларативный язык именно что общего назначения

Это невозможно. По определению декларативный язык всегда заточен под задачу.

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

Для начала, конечно, надо разработать совершенно новый матаппарат и совершенно новую нотацию. С совершенно новым разделом математики. А так, да, можно :)

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

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

Мне кажется, хостовой язык тоже должен дорабатываться в сторону какого-то правильного баланса между возможностью писать декларативно и (местами) императивно для скорости. Т.е. это поиск баланса - scala это именно он, видимо, в случае jvm, когда оказалось что баланс в виде java жестко нарушен :)

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

Я не встречал этого на практике, нужно хотя бы пример - зачем оно нужно, допустим, какая польза от знания source location?

Нормальное позиционирование ошибок, например. Допустим, система контрактов racket реализована на макрах. Если ее реализовать на ФВП или на макрах без source location, то в случае нарушения контракта будет выблевываться нечто невнятное и нам, чтобы понять ошибку и ее найти, надо будет смотреть на детали реализации. Знание source location позволяет сгенерить ошибку для _нужного_ терма - абстракция меньше течет.

Можно пример?

Ну допустим так:

(let ()
  (define x #'x)
  (define-syntax-rule (first-x) x)
  (displayln (bound-identifier=? x #'x))
  (let ()
    (define x #'x)
    (define-syntax-rule (second-x) x)
    (displayln (bound-identifier=? x #'x))
    (let ()
      (displayln (eq? (syntax->datum (first-x)) (syntax->datum (second-x))))
      (displayln (bound-identifier=? (first-x) (second-x))))))

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

Ну с моей точки зрения это совершенно не так.

ну и макросы с ними - шаблоны++, например.

Ну если под макросами понимать слабовыразительные системы типы шаблонов с++, TH, макросов общелиспа и т.д. - то, действительно, никак иначе кроме как для генерации бойлерплейта это использовать нельзя.

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

Вот тут согласен. По сути ООП пытается решать несколько ортогональных проблем. Оттуда и кривизна.

И ооп как где?

Ну как эрланге или смоллтолке."

Например?

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

Это «в идеале», на практике же все пишут на джаве :)

которая не декларативна. А мы, вроде, пытаемся рассмотреть ситуацию, когда пишут на декларативном языке :)

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

В достаточной - это в какой? :)

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

Ну и ни для чего из этого нету ни нотации, ни матаппарата, ни примерных представлений о том, как бы выглядел декларативный язык :)

, а сами таски все из себя - теория графов и NLP

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

Что ты, кстати, думаешь о racket2?

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

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

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

Другое дело, что у них может быть какой-то особый синтаксис

Ну (0: int) и x из (val x: int = 0) оба передаются на место int в аргумент функции в круглых скобочках, а в аргумент конструктора типа list (тоже в круглых скобочках) передаётся только (0: int), но не x, причём компилятор жалуется, что оно не static (так же как плюсы жалуются на вещь в <> которая не constant expression).

То, что плюсы не чекают шаблон - проблема плюсов.

Всё верно. Концептов нет, шаблоны не чекаются — не есть хорошо. Можно, например, переписать какое-то простенькое доказательство из зависимых типов на шаблоны, но это бессмысленно — вся конструкция не чекается, никаких гарантий нет, они будут только для конкретных инстансов (никакой универсальности). Точно так же IsAbelianSemiGroup только подразумевается (по факту — есть operator+, считаем, что ты крякнул и утка).

template<T> void f();

<typename T>?

Ты, наверно, этот f начнёшь специализировать, ну хорошо, в агде это будет:

record f-Theory (_ : Set) : Set where
  field axiom-of : IO Void

f : ∀ {T} ⦃ _ : f-Theory T ⦄ → IO Void
f ⦃ model ⦄ = f-Theory.axiom-of model

-- ^ template <typename T> f();

SomeModel : f-Theory SomeType
SomeModel = record { axiom-of = ... proof ... }

-- ^ template <> f<SomeType>() { ... }

t = f ⦃ SomeModel ⦄

-- ^ f<SomeType>();

то есть сахар instance arguments (SomeModel будет выбираться автоматически, как в плюсах, если T ~ SomeType известно из контекста) над теми же базовыми вещами (тут индексации нет, просто полиморфизм по типу).

Давай я ещё раз расскажу как я вижу (и как я твою картинку понял).

Объясняем так, мол, ребята, у нас в языке есть статические константы, то есть если есть тип T с любыми (неизвестными во время выполнения) термами и значениями, например со значениями T read_from_file() и термами some_func(read_from_file(), ...), то есть подтип T из значений которые суть статические константы, будем делать такие подтипы с помощью квалификатора constexpr — constexpt T <: T, constexpt T вкладывается в T, но не наоборот (read_from_file(), например, не вкладывается), дальше, очевидно, что на этот подтип можно сузить все примитивные операции и прочие функции — мы получаем constexpr операции и функции, а в итоге мы получаем constexpr термы вообще (constant + expression, собственно), то есть как some_constexpr_value, так и some_constexpr_func(some_constexpr_value, ...), и известно, что вычисления в рамках таких термов тьюринг-полные в compile-time, как и основной язык, равно как и типизированы, как и обычные термы. Причём семантика «статических констант» ловится именно квалификатором constexpr, более ранние const и static говорят только про память — если данный объект существовать в памяти будет, то мы можем стереть const квалификатор и изменить его значение (если это вообще можно на уровне памяти), или инициализировать const объект любым термом (read_from_file()), тогда как если не брать адреса constexpr, то ему быть в рантайме не обязательно, и инициализировать его чем угодно нельзя.

Теперь dependent product и индексированные типы. Вопрос — есть ли универсальные конструкции P(t : T). u[t] и P(t : T). U[t] (T, U — типы, t, u — термы) в языке? Очевидно, нет. Хорошо — есть ли такие типы T, что P(t : T). u[t] и P(t : T). U[t] существуют и работают — сколько угодно, constexpr типы (в языке они в <> скобочках — все constexpr). То есть как смотреть — либо эти конструкции работают для всех типов, но не для всех их термов, либо они работают не для всех типов (но для всех термов тех типов для которых они работают). Есть в функциях и (индуктивных) типах такие типы индексированные термами (какие-то типы, термами каких-то типов)? Есть.

Ты предлагаешь с каждой статической константой (вообще с канонически сконструированным в нормальной форме термом) t типа T связать тип {t} — t : {t}, {t} <: T, так что, например, в

constexpr int t = -5;

-5 это тип (кхм, дежавю). После чего все constexpt сужения операций и функции нужно поднять на уровень типов — допустим, у нас там тьюринг-полнота (не нужно, конечно, но пусть), а ещё всё так же выразительно как и в омеге, однако, нам нужно сохранить типизацию исходных функций, то есть нужно ввести отношение типизации на типах, то есть мы заменяем статические константы типами-синглетонами, так что нам нужно заменить их типы видами-синглетонами — {t} <: T <=> {t} : {T}, после чего constexpr T -> U типизируется как {T} -> {U}. В итоге P(t : constexpr T). ...[constexpr_func(t)] будет не обычным P(t : T). ...[func(t)] для constexpr T <: T, а forall (U : {T}). ...[TypeOp(U)] где всё поднято в типы. Да, и почему нужны виды — потому что ограниченная квантификация по T даст лишние подтипы (либо это должен быть специально подготовленный тип S(T) подтипы которого это ровно синглетоны — forall (U <: S(T)). ...[TypeOp(U)]). Ещё нам нужно опускать всё обратно, то есть вместо (implicit) constexpr T -> T преобразований нужны (implicit) преобразования {T} -> T (функция из вида в тип, то есть соответствие типов (синглетонов) и термов, либо S(T) -> T).

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

Да пусть ломают, например, тот же самый values сделать первоклассной сущностью, а не через let/ec - уже неплохо.

Ну, и обобщенные for, map, которые они предлагают - тоже ня.

Да пусть ломают

Коненчо пусть. Но им, видимо, неохота.

а в аргумент конструктора типа list (тоже в круглых скобочках) передаётся только (0: int), но не x, причём компилятор жалуется, что оно не static (так же как плюсы жалуются на вещь в <> которая не constant expression).

Ну ты в агду если в () передашь вместо фигурных она же тоже нажалуется.

<typename T>?

Чего? Я спрашиваю какой это тип с точки зрения формализма зависимых типов.

Ты, наверно, этот f начнёшь специализировать

Я хочу дождаться у тебя ответа, что это П(T:type).unit->void, но т.к. в типе результата нету T, то, по определению П(T).unit->void это то же самое, что и type->unit->void (это рдве разные записи одного и того же типа). То есть это не шаблон, а обычная функция. И потом бы я попросил подставить в эту обычную функцию обычный аргумент. Не const. Ведь в обычную функцию можно не толкьо const подставлять.

есть ли универсальные конструкции P(t : T). u[t] и P(t : T). U[t] (T, U — типы, t, u — термы) в языке? Очевидно, нет.

Ну собственно на этом можно и закончить, нет? Потому что если нету зависимых типов - то о каких зависимых типов может идти речь? :)

Хорошо — есть ли такие типы T, что P(t : T). u[t] и P(t : T). U[t] существуют и работают — сколько угодно, constexpr типы

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

так что нам нужно заменить их типы видами-синглетонами

Не, видами-синглтонами не надо, наоборот - суть-то в том, что, например, у нас есть тип int, него значения 0,1,2,-1, етц., далее для каждого значения у нас будет тип синглтон LiftValue 1, LiftValue 0, LiftValue -1, а для типа int (не синглтона) у нас будет обычный вид (не синглтон) LiftType int. Значения лифтятся в типы-синглтоны, типы - в виды (не синглтоны).

И никогда ты не напишешь результат экспанда руками

Ok, спасибо - я не очень еще шарю макросистему рэкет, но зопейсал.

Ну если под макросами понимать слабовыразительные системы типы шаблонов с++, TH, макросов общелиспа и т.д. - то, действительно, никак иначе кроме как для генерации бойлерплейта это использовать нельзя.

Я другого не видел еще, только макры рэкета - и то очень поверхностно.

Вот тут согласен. По сути ООП пытается решать несколько ортогональных проблем. Оттуда и кривизна.

Ну да, поэтому не очень понятно, почему в скале сделали упор на поддерживание этого говна как нейтив.

И ооп как где?

Ну как эрланге или смоллтолке."

Ok, тогда следующий вопрос - для какого класса задач.

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

ФВП тоже объекты, но это не ооп. А классы в ооп - это по сути гибрид типов и модулей.

Это «в идеале», на практике же все пишут на джаве :)

которая не декларативна.

Естественно, но на ней пишут. Это означает, что либо декларативность переоценена, либо человеческий мозг в большинстве свое устроен думать маленькими известными кирпичиками (пусть и не декларативно, долго и через жопу), но стабильно.

А мы, вроде, пытаемся рассмотреть ситуацию, когда пишут на декларативном языке :)

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

Ну и ни для чего из этого нету ни нотации, ни матаппарата, ни примерных представлений о том, как бы выглядел декларативный язык :)

Языки пишут пока что интуитивно, это что-то вроде искусства - это такая математика мимо формализации :) если так можно сказать.

а сами таски все из себя - теория графов и NLP

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

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

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

Я бы хотел бы видел более функциональный racket, т.е. все еще лисп, все еще макросы, но чуть больше функционального синтаксиса.

Ю Ok, спасибо - я не очень еще шарю макросистему рэкет, но зопейсал.

Вобщем-то пример, конечно, весьма искуственный (хотя может и в реале случится нечто подобное, еще можно аналогичный пример сделать с get-local-shadower, думаю). Более интересны примеры с макрами, экспанд которых хоть и можно записать, но только теоретически. А на практике - пизданешься в процессе.

Ну да, поэтому не очень понятно, почему в скале сделали упор на поддерживание этого говна как нейтив.

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

Ok, тогда следующий вопрос - для какого класса задач.

Да в любом случае, когда у нас по факту живут взаимодействующие друг между другом объекты. Например, в играх тех же.

ФВП тоже объекты, но это не ооп.

Ну можно ООП сделать на ФВП. Но ООП от этого не перестанет быть ООП.

Это означает, что либо декларативность переоценена

Либо просто пока нету способа легко, быстро и удобно пилить дсли на каждый чих.

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

С этим согласен, тут не о чем спорить.

Именно созданием такой семантики сейчас заняты все умы :)

НВот когда создадут... :)

Я бы хотел бы видел более функциональный racket, т.е. все еще лисп, все еще макросы, но чуть больше функционального синтаксиса.

Что подразумевается под функциональным синтаксисом? Если речь о синтаксисе - это точно не реализуется макросом на две строки? :)

Что подразумевается под функциональным синтаксисом? Если речь о синтаксисе - это точно не реализуется макросом на две строки? :)

Не знаю, наверное, реализуется, буду пробовать.

Ну ты в агду если в () передашь вместо фигурных она же тоже нажалуется.

Я знаю какие в ATS должны быть скобки (у конструктора типов list) — не в этом проблема.

Чего?

Я думал ты про специализации template <typename T> по разным типам спрашиваешь.

А это было template <SomeType>.

Не const

В <> всё constexpr, так что если переводить template <SomeType> void f(), то в P(_ : constexpr SomeType). void, то есть в constexpr SomeType -> void.

Потому что если нету зависимых типов - то о каких зависимых типов может идти речь? :)

Отлично, если у тебя нет 1000000$, то у тебя, выходит, вообще денег быть не может. Универсальных нет — конкретные индексированные типы по конкретным термам конкретных типов есть, сколько угодно.

Как в соседнем треде — никого не смущает смешивать шаблоны, дженерики и параметрический полиморфизм, ну так в C++ ещё и индексация есть (вот глава TAPL про зависимые типы — индексация типов термами, суть они).

видами-синглтонами не надо

Ну да, {t} <: T <=> {t} : {T} — в {T} много разных {t}. Я к тому что он для _одного_ типа строится, хотя не синглетон в с смысле «содержит один тип».

Ты скажи, что конкретно надо, я скажу реализуется или нет.

А это было template <SomeType>.

О чем ты?

P(_ : constexpr SomeType)

Ты же понимаешь, что такого типа как «constexpr» не может существовать? Ты модель не построишь под такую лажу. Этот факт тебя не смущает?

Универсальных нет

А какие еще они могут быть?

конкретные индексированные типы по конкретным термам конкретных типов есть

Ну так они везде есть, если у нас видов больше чем *, *->* и так далее (то етсь етсь ограниченная квантификация) и есть операторы над типами, угу.

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

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

Только термами, а не constexpr термами. Как ты не поймешь, что в этом принципиальная разница есть, которая и отличает две формальные системы друг от друга? Ты увидел неформальное определение со словом «индексация» и к нему прицепился. А что такое «индексация термами данного типа»? Не все, что можно назвать индексацией, дает зависимые типы. Особенно если ты начинаешь подменять понятия и вместо индексации, про которую говорится в тапле (по любым термам) придумал свою индексацию по const'ам.

Как в соседнем треде — никого не смущает смешивать шаблоны, дженерики и параметрический полиморфизм

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

О чем ты?

ооп и функциональщина кратко, внятно. (комментарий)

template<T> void f();

Например template<int> void f(); — про что ты спрашивал.

Ты же понимаешь, что такого типа как «constexpr» не может существовать?

Типа (constexpt int) не существует? (constexpt это квалификатор типа).

Только термами, а не constexpr термами.

_Всеми_ термами какого-то типа, именно — constexpr типа, все термы типа квалифицированного как constexpr это constexpr термы, то что не по всем типам можно проводить индексацию (а только по constexpr типам) меня совершенно не смущает. Я вообще не понимаю такого требования про неизвестность индексов в рантайме — возьмём ту же агду и выкинем рантайм с бакендами, оставим только останов/тайп-чекер и тотальный интерпретатор который использует тайп-чекер, у нас будет один compile-time, то есть просто разрешимый (пруф) чек (он подразумевает возможность тотальных вычислений (тех самых редукций термов в типах) во время своего выполнения, так что если мы хотим что-то посчитать, то мы всё ещё можем это сделать) — агда перестала быть агдой, из неё пропали зависимые типы и она потеряла свою теоретико-доказательную силу? На самом деле большинству народа от агды (и Coq? хотя на нём ещё можно что-то пописать на выполнение) только этот чек и нужен.

Например template<int> void f(); — про что ты спрашивал.

Я тип template<T> void f(); спрашивал

Типа (constexpt int) не существует?

constexpr существует только если это кайнд. Типом он быть не может - это ломает саму идею типов.

именно — constexpr типа

Нельзя определить такой тип. У тебя сразу все правила типизации при его введении сломаются.

Я вообще не понимаю такого требования про неизвестность индексов в рантайме

Претензии не ко мне, а к тем, кто придумал зависимые типы.

про неизвестность индексов в рантайме

Зависимость индексов от сайд-эффектов - только частный случай.

lambda x. new Array<x> - вот так тоже должно быть можно.

Ты пойми, тут дело не в том, что кто-то требует какое-то специально условие «для всех термов», или там «для термов которые неизвестны в рантайме в том числе». Суть в том, что никто не требует ограничивать эти термы. И в этом зависимые типы отличаются от других систем. В этом вообще идея зависимых типов. Эта та особенность, ради исследования которой зависимые типы вообще придумали. То, ради чего (ИСКЛЮЧИТЕЛЬНО ради чего) они нужны. кроме этого системы с зависимыми типами от других систем не отличает больше _ничего_. Они ни для чего больше не нужны. Они ничем больше неинтересны. Они ничем больше не полезны.

Я тип template<T> void f(); спрашивал

Где T это какой-то тип, так? То есть int, ..., SomeType (определённый как struct SomeType) и т.п. Иначе это не валидная синтаксически конструкция и нужно template<typename> void f(); — как я сначала понял, когда написал про instance agruments. Ну а если template<T> void f(); в первом смысле, то тоже уже выяснили, только по-твоему есть какие-то проблемы иметь constexpr T в виде типа (скорее наоборот — в абстрактной системе типов со строгой нормализацией (как в лямбда кубе) всё изначально constexpr, вопрос в том как расширять это до частичности, памяти, эффектов).

Они ни для чего больше не нужны. Они ничем больше неинтересны. Они ничем больше не полезны.

Таки акцентирую внимание на мой вопрос — Agda, буфер с кодом на ней в Emacs, чек (C-c C-l) и выяснение того какие типы установились в результате этого чека (C-c C-d), всё compile-time, constexpr и известно до рантайма (которого просто нет, иначе пример — чего не известно). Зависимые типы — по горло. А если добавить таки рантайм, то вопрос — как там с getNat >>= \(n : Nat) -> replicate n 0 : Array Int n? Будет работать или нет? С точки зрения базовой агды это уже в нормальной форме, так как >>= это примитив, работать тут нечему — эту форму нужно отдать интерпретатору или компилятору, пусть он решает что с ней делать (но пусть лучше работает). Но индифферентно же — зависимые типы _уже_ есть, без всякого рантайма, «неизвестные» n не в базовой агде, а в монаде IO, и если кто-то не может толком смоделировать эту монаду (пример не компилируется дальнейшим бакендом), то это не отменяет существование зависимых типов в базовой агде.

всё изначально constexpr

Нет, не constexpr. Любая связанная переменная - не constexpr.

Но индифферентно же — зависимые типы _уже_ есть, без всякого рантайма

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

Назначение зависимых типов - выводить утверждения о значениях термов, не зная этих значений. _не зная_.

всё compile-time, constexpr

lambda x. new Arra<x>

Где у тебя тут constexpr?

«неизвестные» n не в базовой агде, а в монаде IO

А IO тут при чем? У тебя и без всякого ИО куча неизвестных термов. Практически все связанные переменные - неизвестные термы. Ну и любой терм, который содержит связанную переменную - тоже будет почти всегда неизвестным.

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

А если у нас программа представляет из себя после нормализации конкретное значение - то тут вообще не надо никакой системы типов. Просто выполняем программу (в компайлтайме) и смотрим что получилось. И если все получилось хорошо - то подставляем вместо программы предвычисленный результат.

Ну и ты как-то проигнорировал тот момент, что попытка ввести тип constexpr сразу ломает типизацию.

Вообще возьми и попробуй для тренировки написать правила типизации для простой типизированной лямбды с базовыми Bool и constexpr. уверен, у тебя настанет просветление.

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

lambda x. new Arra<x>

open import Data.Nat
open import Data.Vec

t = λ n → replicate {n = n} 5
-- :: (n : ℕ) → Vec ℕ n

q = t 5
-- => 5 ∷ 5 ∷ 5 ∷ 5 ∷ 5 ∷ []
-- :: Vec ℕ 5

t в нормальной форме, тип установился (n : ℕ) → Vec ℕ n, проверилось, что всегда при прилёте n получится Vec размера n.

Ну как и

#include <array>

template <size_t n, typename T>
std::array<T, n> replicate(T x) {
    std::array<T, n> res;
    res.fill(x);
    return res;
}

template <size_t n> std::array<nat, n> t() {
    return replicate<n>(nat(5));
}

// for (auto x : t<5>()) printf("%ld\n", x);

тоже проверилось.

Теперь — в чём разница, примеры в студию. В распоряжении только Emacs и C-c C-l с C-c C-d от agda2-mode — даже C-c C-n не нужен, можно вычислять по C-c C-d через proxy-тип:

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

никаких IO и бакендов.

t в нормальной форме, тип установился (n : ℕ) → Vec ℕ n, проверилось, что всегда при прилёте n получится Vec размера n.

Ага. А в плюсах все не так.

Теперь — в чём разница

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

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

Пример будет? Что-нибудь не constexpr на агде что нельзя перевести на плюсы (про навороты уровня системы типов не говорим — что-нибудь базовое)?

А то пока видимая разница только в том, что агда чекает шаблоны^Wтипы, а C++ — нет, вот был бы чек и constraint solver... Было бы то же самое, но лучше.

Что-нибудь не constexpr на агде что нельзя перевести на плюсы

Ты сам и привел пример. Функцию t нельзя написать на плюсах.

Ты никак не понимаешь, что время вычисления терма - существенно. В агде вычисление t 5 происходит в рантайме (во время редукции термов) в плюсах - во время тайпчека (компиляции, инстанцирования шаблонов - ну короче где-то там). В формальной теории эти два шага четко разделены, и зависимые типы в некотором смысле «стирают» между ними границы. Если ты не разделяешь рантайм и компайлтам - то, конечно, у тебя нету зависимых типов. Если у тебя есть только рантайм - то у тебя динамика, типизация отсутствует вовсе. Если у тебя только компайлтайм (то, что ты предлагаешь), то у тебя нету семантики языка.

В агде вычисление t 5 происходит в рантайме (во время редукции термов)

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

w : Proxy (t 5)
w = record {}
-- Proxy (5 ∷ 5 ∷ 5 ∷ 5 ∷ 5 ∷ [])
-- ^ тип w который установился после тайп-чека, то есть в compile-time.
-- Ещё примечательно, что этот тайп-чек разрешим, как и всякий (нормальный)
-- алгоритм компиляции (сам по себе тайп-чек -- только часть этого алгоритма,
-- но остальные тоже разрешимы), тогда как рантайм, вообще говоря, всегда
-- неразрешим.

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

Нет, оно происходит в compile-time

Нет не так. Оно происходит в рантайме.

никакого рантайма вообще нет.

Так не бывает. Нет рантайма = нету семантики у языка.

Смотри, у языка есть:

1. Синтаксис - набор правил, который позволяет построить синтаксическое дерево терма из последовательности символов

2. Система типов - набор правил, который позволяет построить типизированное дерево из синтаксического

3. Семантика - набор правил, который позволяет, имея типизированные деревья термов разбить термы на классы эквивалентности и выделить некое подмножество термов в нормальной форме.

Когда я говорю про «рантайм» или «компайлтайм» - я не имею в виду реальный процесс, чего там происходит в недрах агды, какой там она делает констант фолдин или еще что. Я говорю о том, из какого набора берутся правила. В случае агды совершенно точно, когда ты говоришь, что (t 5) ~ (5 ∷ 5 ∷ 5 ∷ 5 ∷ 5 ∷ []) - то ты пользуешься правилами из набор 3 - «семантика языка». То есть рантайм. При этом как и когда это на самом деле работает и что там агда делает - это все детали реализации, нас это не волнует. На самом деле мы даже не запускали агду, мы только смотрели на ее спецификацию. Возможно, что на самом деле никакой агды нету и ее никто не написал. Будем в дальнейшем считать именно так.

С плюсами несколько сложнее - тут ничего даже отдаленно похожего на формальную спецификацию нет :)

Но какая-то спецификация есть.

И из нее интуитивно так ясно, что процесс инстанцирования мало связан с рантаймом. Утверждать, что связан - может только полностью упоротый товарищ.

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

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

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

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

Сравни с плюсами - он не может типизировать этот терм до вычисления.

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

процесс инстанцирования мало связан с рантаймом

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

В агде (и вообще любой LF) чтобы делать 2 нужно делать 3 во время 2.

Это уже твои собственные придумки. Правила типизации и правила редукции - разные правила.

Ну процесс тайп-чека агды

Тайпчека - да. Но тут же мы как раз и говорим о том, что в агде - это рантайм значение и рантайм терм. И между тем она все чекает. В отличии от плюсов, которые должны вычислить.

вообще мне надоел спор. Мы пока что выяснили следующий ряд фактов:

1. система типов плюсов не удовлетворяет формальному определению зависимых типов.

2. она вообще не удовлетворяет какому-либо определению, которое связано с зависимыми типами.

3. плюсы не умеют делать то, что умеют делать все другие системы с зависимыми типами (даже с restricted версиями)

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

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

6. нету вообще ни одного аргумента за наличие зависимых типов в плюсах кроме _синтаксических_ (!) моментов.

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

в этом контексте не вижу смысла в продолжении разговора.

Это уже твои собственные придумки

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

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)

Подумай, как чекер должен убедиться в том, что эти две программы well-typed (он должен редуцировать по правилам бета-редукции (это никакой не ad-hoc «constant folding») обе части в первом примере, так что refl : 120 ≡ 120 — refl : ∀ {a} → a ≡ a в общем случае, во втором примере он должен разобрать первую ветвь — refl : 0 + 0 ≡ 0 и refl : 0 ≡ 0 после редукции (первое правило для _+_), и вторую ветвь — suc a + 0 ≡ suc a где он должен воспользоваться вторым правилом редукции из определения _+_ — получится suc (a + 0) ≡ suc a, то есть тип cong suc (a+0≡a a) — доказательство по индукции).

Но тут же мы как раз и говорим о том, что в агде - это рантайм значение и рантайм терм.

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

Мы пока что выяснили

Ну как обычно — ты что-то там решил себе, но факты выяснили «мы».

Кстати, можешь Oleg-а приобщить — http://okmij.org/ftp/Computation/lightweight-dependent-typing.html:

All these lightweight approaches rely on type-level proxies for values, so we can statically express properties (e.g., equality, inequality) of the values that are not generally known until the run time.

In general, dependent type is a type that is predicated upon a (dynamic) value

Хотя

http://lambda-the-ultimate.org/node/1566

Adam Chlipala:

Is ATS really «dependently-typed»?

I don't think of it that way. ATS has a clear separation between statics and dynamics, and the statics part may never refer to the dynamics. My definition of «a dependent type system» is based on a cycle in the language's syntactic classes, where some class A (like expressions) is described by some class B (like types), where the syntactic definition of B refers to A. In Coq, for instance, there is just one syntactic class, and it is typed in terms of itself.

Dan Licata:

I use the term «dependent types» more broadly, to refer to any language with fancy type-level data.

For marketing purposes, it's good to have one term for the high-level functionality that the programmer sees: rich type-level data that can be used to specify and verify properties of programs. And «dependent types» seems like as good and historically relevant a term for this as anything else (anyone have counter-proposals)?

The technical methods of providing this functionality are a second-level concern---though of course it's important for researchers to be able to convey a language design quickly, which requires more detailed terminology (e.g., I've heard «phase-sensitive dependent types» for DML-style, or «full spectrum dependency» for Epigram). However, I think the language design space is more complicated than the syntactic condition you described above: For example, if I presented the syntax of the simply typed lambda-calculus with one syntactic category, and then sorted out the difference between expressions and types in the typing judgement, your definition would deem it dependently typed. Alternatively, what if a language allows _some_ programs to be used in types, but not others (e.g., by making a restricting the types at which dependency is allowed)? Or what if a language that allows run-time computation with «type constructors», a static syntactic category? There are lots of variations on restricted forms of dependent types, but we need one word for the overall concept.

http://research.microsoft.com/pubs/67515/phasedistinctions.a4.pdf

This dependency directly causes phase mixing, unless one is careful to distinguish between compile-time values (e.g. given by constant expressions in Pascal), and run-time values.

http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.105.788&rep=rep1...

DML [7], GADTs [8] and Omega restrict the form of dependent types they allow; this is in part in order to preserve a clear phase distinction between types and values. Where the same piece of data must occur in both phases, it must be duplicated by hand at the type level. The justification for such programmer inserted duplications is the need to maintain an erasure semantics;

Ты скажи, что конкретно надо, я скажу реализуется или нет.

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

• include pattern matching forms in more binding positions (e.g. define, let/for clauses)
• Generic programming by default: map, fold, and friends are generic and not specialized to lists
• Add CLOS-like defmethod (with multidispatch and :before, :after, :around) on Racket classes

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

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