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

лень искать на что отвечать: про вектора на коленке:

{-# LANGUAGE TypeFamilies, EmptyDataDecls, UndecidableInstances #-}

import Data.Vector as V

data Z
data S a

type family Plus a b :: * 
type instance Plus Z a = a
type instance Plus (S a) b = Plus a (S b)

data FVector a b = FVector (Vector b)

plus :: FVector a b -> FVector c b -> FVector (Plus a c) b
plus (FVector x) (FVector y) = FVector (x V.++ y)

unsafeConstruct :: Vector a -> FVector b a 
unsafeConstruct v = FVector v

a = unsafeConstruct (V.replicate 3 1) :: FVector (S (S (S Z))) Int
b =  unsafeConstruct (V.replicate 2 1) :: FVector (S (S Z)) Int

хотя для этого FixedVector есть..

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

Только я не Vector обвернул, а списки сделал.

А так примеры типа a и b тоже делал; убедился, что с plus тип результата выводится.

@anonymous

Вот это «система-эф-омега», то есть термы для чисел представляются типами и функции для них работают как type -> type (TypeFamilies), если будет FVector :: Word -> * -> *, так что Word это обычный тип соответствующих термов и функции для него это обычные функции над Word, то это уже будут зависимые типы. Если функции над Word и термы Word которые участвуют в индексации типов типа FVector при этом будут должны приводиться к нормальной форме в compile-time (то есть как в C++ — constexpr), то это всё равно будут зависимые типы — а то как получается, мы хотим провести тайп-чек (compile-time!), начинаем редуцировать типы, какая-то функция блокируется на вызове задачи «прочитать что-то из stdin» или «позвонить Васе и узнать как редуцироваться дальше» и типа если такая ситуация невозможна, то это уже не зависимые типы, тайпчек зависимых типов прямо обязан уметь заказывать пицу, откуда Agda и Coq — не системы с зависимыми типам. По мне так бред.

Во всей SystemF я не вижу средств записать concat.

Не видь дальше, это же не изменит того факта, что я _написал_ твой concat на system fw.

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

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

Ну нет же, там любые термы

Там не любые термы, а только те, что имеют type-level представление (то есть те, что можно подставить в system fw, потому что это system fw).Я для тебя, необразованного долбоеба, даже специально привел ссылку на хаскиль, где это разжевывается на пальцах. но до тебя не дошло.

То что они делают как делают это их проблемы.

При чем тут «как делают», идиот? Там написано, что это представляет по сути. А по сути это - типы-синглтоны. И в плюсах - типы синглтоны. А теперь пиздуй читать тапл и больше тут не появлялся, пока хотя бы не поймешь, чем системы лямбда-куба друг от друга отличаются.

просто compile-time

Так вот это и отличается зависимые типы от простого полиморфизма. В зависимых типах можно ставить любой терм, не только compile-time.

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

Но в плюсах нету таких функций.

Если функции над Word и термы Word которые участвуют в индексации типов типа FVector при этом будут должны приводиться к нормальной форме в compile-time

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

то это всё равно будут зависимые типы — а то как получается, мы хотим провести тайп-чек (compile-time!), начинаем редуцировать типы, какая-то функция блокируется на вызове задачи «прочитать что-то из stdin» или «позвонить Васе и узнать как редуцироваться дальше»

Ты же вообще не в курсе, как работают зависимые типы, да? Никто ничего не редуцирует. И из stdin никто читать не будет.

откуда Agda и Coq — не системы с зависимыми типам.

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

Напиши тип concat.

forall N<:Nat, M<:Nat, T<:Any . Array T N -> Array T M -> Array T (Plus M N)

N, M, T - обычные типы кайнда *, Plus - обычный оператор над типами (тип кайнда * -> * -> *).

В системе с зависимыми типами есть concat, есть она в SystemF?

Конечно же есть. См. выше.

То есть нужно подставить терм не в нормальной форме?

ЛЮБОЙ ТЕРМ СООТВЕТСТВУЮЩЕГО ТИПА. Например - переменную, значение которой в компайлайме, конечно, неизвестно. Ну вот например так должно быть можно:

void fun(n: size_t) {
  Array<int, n> = ...
}

здесь n - терм соответствующего типа.

то есть как там пишутся вещи которые я показывал (функции с ... term ... -> type и зависимостями).

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

В плюсах, вот ведь странно, ты можешь подставить только те термы, которые имеют представление на уровне типов

Нет никакого представления на уровне типов, «известный во время компиляции» как соотносится с «имеет представление на уровне типов»? Вообще не важно как оно реализовано (то есть через типы оно поднимается или вообще через левый MyCompileTimeTermWhichIsOkInTypeLevel с подходящими правилами типизации для типов и этой левой фигни). Например, как работают constexpr термы типа size_t (вида typename) в type-level? Как сахар над типами zero : typename и suc : typename -> typename? А откуда ты знаешь? А может там просто интерпретатор который делает то что нужно делать для реализации стандарта? То что вещи типа size_t _можно_ перевести в такие типы ничего не значит — мало ли какие эквивалентности существуют, это не важно, видим мы самые обычные size_t передаваемые в самые обычные функции (фактически, constexpr size_t <: size_t, считай, что индексация зависимых типов работает не по обычным (= без всяких представлений) термам типов T : typename, а только по обычным термам типов constexpr T : typename — всё равно индексация и зависимые типы, никаких представлений типами нет).

вот например так должно быть можно

В С++ оно всё равно должно быть constexpr, так что делается в <> а не ().

В зависимых типах можно ставить любой терм, не только compile-time.

Это ты придумал ограничение, нет такого. Есть _Dependent_ ML который не умеет в твои примеры с чтением числа и динамическим созданием типа, не умеет так же как Haskell или C++. ATTAPL:

Undecidablef typechecking is not to the taste of all programming language designers, and for reasons such as scalability, may not be suitable for general application. The alternative is to consider dependently typed languages built around standard programming language features, yet with low-complexity typechecking algorithms. To achieve this one must sacrifice some of the generality of dependent types. Dependent ML (DML) is a proposal which follows this approach, which we will investigate in more detail in the remainder of this section. A type system closely related to that of DML, but aimed at Haskell, was studied by Zenger, under the name indexed types (1997).

Exactly because this class of type systems have the desirable feature that they provide “static” typechecking independently from execution or equivalence checking of terms, some authors prefer not to call them “dependent” at all. The definition of dependent types given in Chapter 8 is slightly stricter than ours, and contrasts statically typed languages like DML and Indexed Types with languages where there is a lack of phase distinction between the compilation and execution of a program (see page 305).

«some authors» это не истина в последней инстанции, очевидно. Авторы цитируемой статьи или Conor McBride, например, не видят проблем в том чтобы относить системы с indexed types к dependent types.

Тот же TAPL: «30.5. Идем дальше: зависимые типы» — «семейство типов, индексированное термами» есть, но никаких требований про динамическое создание типов нет.

возможность подставить _любой_ терм, а не только нормализованный

Потому что ненормализованные типы можно подставлять и в ф-омег

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

Такая вещь — во всех системах лямбда куба вообще нет ненормализируемых термов и типов. В Coq и Agda нет ненормализируемых термов и типов. Поэтому если ты в Agda вычислишь (C-c C-n в Emacs) нормальную форму того же main, то вполне увидишь выхлоп представляющий из себя терм в нормальной форме и состоящий из примитивов компилятора, FFI и т.п. (коиндукция, IO) — какой-то интерпретатор может взять такой терм и интерпретировать его как описание каких-то частичных вычислений с эффектами, компилятор может скомпилировать его во что-то (Haskell, JS в нынешних бакендах агды, у MAlonzo даже бонус есть — там типы _можно_ динамически создавать во время выполнения). При этом большинству пользователей агды это не нужно — у них ВСЁ в compile-time, то есть написал, проверил типы, вычислил какое-то нормальные формы, всё гарантированно (за исключением багов) за конечное время и времени «компиляции» (терм-чек, тайп-чек, тотальный интерпретатор — тот же что работает при редукции типов у тайп-чекера). Аналогично для Coq.

Ты же вообще не в курсе, как работают зависимые типы, да? Никто ничего не редуцирует

TAPL 30.3.2. Эквивалентность и редукция типов.

ATTAPL 2.

In the first case, we may choose to include only basic equalities which are manifestly obvious. This is the viewpoint favored by Martin-Löf, who considers definitional equality to be the proper notion of equivalence. The first two equalities above are definitional: 3 + 4 is definitionally equal to 7 by the rules of computation for addition. Alternatively, one may prefer to include as many equalities as possible, to make the theory more powerful. This is the approach followed, for example, in the type theory implemented by the NuPrl system (1986). This formulation of type theory includes type equivalences like the third example above, which may require arbitrary computation or proof to establish. In such a type system, typechecking is undecidable.

«typechecking is undecidable» немного 4.2, но чтобы провести тайп-чек в соответствии с правилами типизации нужно вовлекать эквивалентности типов, значит, уметь производить редукции термов от которых эти типы зависят. В Agda 1 + 4 = 2 + 3 (где _=_ : Nat -> Nat -> *) сначала редуцируется (обычная бета для термов) в 5 = 5, после чего тайпчекер видит, что тривиальный refl подходит по типу, так что well-typed. В более сложных случаях так же — это весьма фундаментально в случае зависимых типов, так что я даже не знаю «в курсе» чего ты там.

<:

Что это? Ты путаешь http://en.wikipedia.org/wiki/System_F#System_F.CF.89 и http://en.wikipedia.org/wiki/System_F-sub ? В 30-ой главе TAPL нет никаких <:.

N, M, T - обычные типы кайнда *

А я хочу обычные термы типа Nat :: *.

Plus - обычный оператор над типами (тип кайнда * -> * -> *)

А должна быть обычная функция Nat -> Nat -> Nat.

Даже если речь про forall N : Nat, то что-то тут не так — что такое Nat? Вот синтаксис SystemFOmega из TAPL:

Типовые переменные:

X, Y, ...

Виды:

K, ... ::= * | K => K

Типы:

T, ... ::= X | T -> T | forall (X :: K). T | lambda (X :: K). T | T T

то есть можно forall (X :: *), forall (X :: * => *), ... но не forall (t :: T) для T :: *.

А вот LambdaLF из ATTAPL:

Типовые переменные:

X, Y, ...

Термы:

t ::= ...

Типы:

T ::= X | P(t : T). T | T t

Виды:

K ::= * | P(t :: T). K

это первый порядок, то есть оно не умеет всего что умеет SystemFOmega, но оно умеет то чего не умеет последняя, то есть как раз forall (t :: T) для T :: * (forall = P тут). CoC уже умеет всё. Sum в дополнение к P обобщает экзистенциальную квантификацию, так же как P обобщает универсальную.

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

Нет никакого представления на уровне типов

Конечно же есть.

«известный во время компиляции» как соотносится с «имеет представление на уровне типов»?

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

Вообще не важно как оно реализовано

Конечно, не важно. Никого не волнует, суешь ты на место типа сахар в виде 1/2/3 или их рассахаренное выражение через succ/zero - в обоих случаях это типы, а не термы.

Как сахар над типами zero : typename и suc : typename -> typename? А откуда ты знаешь?

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

это не важно, видим мы самые обычные size_t передаваемые в самые обычные функции

В том и проблема, что нет. Мы видим типы-синглтоны, передаваемые в операторы над типами. ни одного примера, где передается именно терм ты не показал (подсказка: такой пример невозможно рассахарить до типов/операторов).

В С++ оно всё равно должно быть constexpr, так что делается в <> а не ().

Ну так о чем и речь. Если есть зависимые типы - то оно делается в (). И нам совершенно не обязательно знать, какое значение у них в рантайме. А в плюсах - операторы над типами. Тип - не значение, оно должно быть известно в рантайме. Чуешь, да? Значение не должно быть известно в рантайме. Тип - должен. Аргумент шаблона в плюсах должен быть известен в рантайме.

всё равно индексация и зависимые типы, никаких представлений типами нет

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

Это ты придумал ограничение, нет такого.

Лол что? Это как раз _ты_ ограничение придумал. Которое в плюсах, на вычисляемость в компайлтайме. Ни у кого в определениях такого ограничения нет - зависимый тип параметризуется _любым_ термом подходящего типа. Это определение такое.

Есть _Dependent_ ML

restricted form of dependent types

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

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

Приставку «в компайлтайме» ты предпочел пропустить, да? let n = 10 in n, терм «n» тут какой - нормализованный, ненормализованный? По идее нормализованный, но значением он не является, понятное дело. О таких термах и речь. Как их конкретно называют - я не вкурсе, не слышал. Может, ты подскажешь.

При этом большинству пользователей агды это не нужно — у них ВСЁ в compile-time

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

TAPL 30.3.2. Эквивалентность и редукция типов.

Ничего, что это про омегу? Омега - да, действительно, редуцируется. Вот и в плюсах твоих - ага, редуцируется :)

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

Ну проведи мне редукцию вот тут:

let n = read
let m = read
arr = Array<int, m+n>

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

А должна быть обычная функция Nat -> Nat -> Nat.

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

В 30-ой главе TAPL нет никаких <:.

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

А я хочу обычные термы типа Nat :: *.

Я тоже хочу чтобы ты показал мне пример в плюсах с обычными термами типа : nat. Ну или не nat а что там у тебя, size_t.

то есть можно forall (X :: *)

Пусть так и будет. Это несущественно, как я уже сказал - добавил для красоты.

но оно умеет то чего не умеет последняя, то есть как раз forall (t :: T) для T :: * (forall = P тут)

И то, чего не умеют плюсы как раз.

То есть разница не в compile-time или нет

Именно в этом и разница. Если у тебя какие-то особые зависимые типы, которые требуют, чтобы типовой аргумент был известен на момент компиляции, то выразительность такой системы ничем не отличается от омеги, очевидно, ведь любой код этой системы тривиально переписывается на омегу. А если выразительность систем совпадает, то..? Сам закончишь?

Конечно же есть.

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

Напрямую.

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

Никого не волнует, суешь ты на место типа сахар в виде 1/2/3 или их рассахаренное выражение через succ/zero - в обоих случаях это типы, а не термы.

А когда g++/clang++ пишут свои сообщения об ошибках они pretty printят эти succ/zero? Или может таковых вообще нет? При специализации, например, нет никакого конструктора suc (а с ним бы было удобнее).

главное, что это типы, а не термы

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

ни одного примера, где передается именно терм ты не показал

Я показал

void f(size_t);
template <size_t n> void g() { f(n); }
void test() { g<5>(); }

видим то что видим (ты правда тут видишь какие-то типы-синглтоны? Горе от ума же) — ты придумываешь как оно _реализовано_, я говорю — почему типы, может там специальная хрень для представления термов? (вычислять-то их нужно — специальная же хрень для вычислений, а не type operators, в C++ вместо последних есть constexpr функции которые могут работать с этими представлениями для constexpr термов).

Если есть зависимые типы - то оно делается в ()

А в DML, ATS, Agda (исторически, сейчас уже нет разницы) в {}, а не ().

Нету способа в DML применить zip к двум спискам, длина которых неизвестна в компайлтайме

Ага, http://www.ats-lang.org/PAPER/DML-jfp07.pdf, создаёшь синтаксический статический регион в котором это известно, потом применяешь. Ну и по построению это может быть известно.

Ты понимаешь, что бредишь?

http://www.ats-lang.org/DOCUMENT/INTPROGINATS/PDF/main.pdf

datatype list1(a: t@ype+) =
| nil1(a) of ()
| cons1(a) of (a, list1 a)

datatype list2(a: t@ype+, int) =
| nil2(a, 0) of ()
| {n: int} cons2(a, n + 1) of (a, list2(a, n))

fun{a: t@ype}
length1(xs: list1 a): int = case+ xs of
| cons1(_, xs) => 1 + length1(xs)
| nil1() => 0

(*
// type-checking has failed: there are some unsolved constraints: please inspect the above reported error message(s) for information.
fun{a: t@ype}
list1_to_list2_1 {n: int} (xs: list1 a): list2(a, n) = case+ xs of
| nil1() => nil2()
| cons1(x, xs) => cons2(x, list1_to_list2_1(xs))
*)

(*
// error(2): unrecognized static identifier [length1].
fun{a: t@ype}
list1_to_list2_2 (xs: list1 a): list2(a, length1(xs)) = case+ xs of
| nil1() => nil2()
| cons1(x, xs) => cons2(x, list1_to_list2_2(xs))
*)

let n = 10 in n, терм «n» тут какой - нормализованный, ненормализованный?

Ну let обычно добавляют (http://www.cis.upenn.edu/~bcpierce/sf/MoreStlc.html#lab613) в конструкторы термов вместе с правилами редукции и типизации, так что let n = 10 in n =>beta 10.

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

В агде? Вообще zip _уже_ принимает списки одинаковой длины, так что вопрос откуда они взялись — 1) они по построению могут быть такие, 2) есть статические регионы, то есть проверили один раз в рантайме каким-то предикатом (не имеет отношения с Vec или zip) и передаём всё со свидетельствами в zip, либо вопрос в функциях вида 3) {n : Nat} -> List A -> Vec A n, 4) {n : Nat} -> Stream A -> Vec A n, 5) g : IO Nat, f : (n : Nat) -> Vec A n, f <$> g — 3) {A : Set} → (xs : List A) → Vec A (length xs), а List тут откуда взялся? сводится к 5), 4) наверно, это будут CoVector с Coℕ, так что сводится к 3), также, сама коиндукция отдана на откуп компилятора или интерпретатора (примитивы в нормальной форме), 5) IO отдано им же (тоже), про то что MAlonzo позволяет конструировать типы динамически я уже говорил.

А вот в C++, DML, ATS (хотя про эти два я точно не знаю — может как-то можно, но я сомневаюсь) только 1) и 2) в силе (или около того).

Ничего, что это про омегу?

В зависимых типах — тем более (если уже в омеге).

Вот и в плюсах твоих - ага, редуцируется

Ну так я говорю:

#include <cstddef>

template <size_t x> struct f { enum { result = x * 2 }; };

constexpr size_t g(size_t x, size_t y) {
    return x * y * x * y;
}

#include <cstdio>

int main() {
    printf("%d\n", f<g(2 * 4 + 3 * 5, 6 * 8 + 7 * 9) + 100500>::result);
}

// movl	$.L.str, %edi
// movl	$13236618, %esi         # imm = 0xC9F98A
// xorb	%al, %al
// callq	printf

во что там у тебя m+n редуцируется, позволь-ка узнать?

Есть для него правила редукции? Нет, всё что есть для _+_ это 0 + y => y и suc x + y => suc (x + y), так что будут редуцироваться все константы и все термы с переменные по графу таких редукций.

А все что ты описываешь - это редукция в омеге.

Ну а начиная с LF так же и термы редуцируются (там в синтаксисе T t).

А если выразительность систем совпадает, то..? Сам закончишь?

Удобство, не? Подоказывай ты теоремки и свойства на ATS и на GHC (там же _можно_ накостылять всё на типах и операторах, в принципе).

Ну и ещё — в GHC кодирующие типы нормально передаются на места * (TypeFamilies так и требуют *, никаких DataKinds), а вот в C++ не получится передать вещь типа size_t на место typename (ну и наоборот — тем более). На самом деле, зачем в GHC вводили DataKinds — чтобы более строгая типизация была (как в плюсах :)), а не открытые семейства типов (то есть динамика в type-level, фактически).

то странно считать, что constexpr термы и типы как-то связаны

Дело не в том как ты считаешь дело в том, что они по факту связаны.

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

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

А когда g++/clang++ пишут свои сообщения об ошибках они pretty printят эти succ/zero?

Ну да.

При специализации, например, нет никакого конструктора suc (а с ним бы было удобнее).

Да при чем тут конструкторы? Это только одно из представлений. Мы можем кодировать через succ/zero, можем кодировать через 1/2/3, можем кодировать нумералами Черча (например в чистой омеге придется делать именно так). Сути это не меняет.

Я показал

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

ты придумываешь как оно _реализовано_

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

я говорю — почему типы, может там специальная хрень для представления термов?

Там специальная хрень для представления типов, если уж разбираться в реализации_. То есть вместо типа дается его представление в виде сахара.

вычислять-то их нужно

В случае зависимых типов - не нужно.

вместо последних есть constexpr функции которые могут работать с этими представлениями для constexpr термов

Чем твоя constexpr функция отличается от оператора над типами?

этого требует абстрактная система типов с dependent product

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

А в DML, ATS, Agda (исторически, сейчас уже нет разницы) в {}, а не ().

В агде аргумент {} может быть _любым_ термом. Разница между {} и () чисто синтаксическая и никак не отражена формально. Она для удобства программиста исключительно.

Ага, http://www.ats-lang.org/PAPER/DML-jfp07.pdf, создаёшь синтаксический статический регион в котором это известно

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

http://www.ats-lang.org/DOCUMENT/INTPROGINATS/PDF/main.pdf

не понимаю эту синтаксически перегруженную бурду. Напиши то же самое на агде.

чтобы более строгая типизация была (как в плюсах :))

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

90% кода с шаблонами просто не скомпилируется при нормальной реализации полиморфизма - компилятор плюнет ошибкой.

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

Это да, просто этот конкретный момент — C++ плюётся, так как различает T (of typename) и typename, а GHC... ну просто не умеет нормально (либо над типами с TypeFamilies, либо DataKinds которые как-то вяло работают, по моим впечатлениям).

Ну let обычно добавляют (http://www.cis.upenn.edu/~bcpierce/sf/MoreStlc.html#lab613) в конструкторы термов вместе с правилами редукции и типизации, так что let n = 10 in n =>beta 10.

Я тебя не спрашивал о терме «let n = 10 in n», я спрашивал о терме «n». Для него правил редукции никаких нету. То есть он выходит нормализован.

2) есть статические регионы, то есть проверили один раз в рантайме каким-то предикатом (не имеет отношения с Vec или zip) и передаём всё со свидетельствами в zip, либо вопрос в функциях вида

Замечательно. То есть параметром передается не число, а произвольный терм соответствующего типа. При этом значение этого терма нам неизвестно - нам достатончно, что для аргументов зипа эти значения совпадают. Хотя они неизвестны, да. Вот это и есть зависимые типы.

В зависимых типах — тем более (если уже в омеге).

Зависимые типы - отдельно, омега - отдельно. С чего у тебя оно «уже в омеге»?

Ну так я говорю:

Ну вот - все как в омеге. Где зависимые типы-то? Чем это отличается от омеги? Хоть одно отличие?

Есть для него правила редукции?

Нет, нету. Так куда оно редуцироваться-то будет?

Удобство, не?

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

По факту выходит, что плюсы - это омега с некоторым сахаром, которая позволяет писать 1/2 место succ/zero или других каких-то способов. То есть разница исключительно синтаксическая. Но синтаксические костыли не делают из одной системы типов другую. Нужна семнатическая разница. А такой нет. Ведь любой пример из плюсов переписывается в омеге.

С чего ты взял, что это представление - не есть типы?

Потому что 100500 летит в size_t и не летит в typename, как и в GHC с DataKinds.

Чем твоя constexpr функция отличается от оператора над типами?

Тем что принимает constexpr термы (<: термы)? То есть она закрыта — летели бы типы, летело бы что угодно, а летят только термы данного типа (если ты хочешь считать их типами, то тебе придётся городить систему для типов на типами такую же мощную как сама основная система типов, ну чтобы как-то отразить это летит / не летит, остальным проще оставить в покое эту одну основную систему типов и иметь constexpr T <: T).

В случае зависимых типов - не нужно.

WAT? В омеге нужно, а расширении омеги уже не нужно? Говорю же — начиная с LF там T t, то есть SomeType SomeTermExpr, так что SomeTermExpr нужно редуцировать (уже термы, а не типы с их операциями).

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

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

В агде аргумент {} может быть _любым_ термом

Я же сказал — исторически. Сейчас разницы нет (а раньше никаких компилятор не было, только чекер).

чего и требовалось доказать

Так ты не стесняйся — ооп и функциональщина кратко, внятно. (комментарий), ЧЯДНТ?

Напиши то же самое на агде.

Не понял. В агде (MAlonzo) ограничений нет, там всё работает.

Давай с другой стороны зайдем.

template <int T> Array<T> f();

какой тип у f с точки зрения теории зависимых типов? П(T: int).Array(T). Так?

Не понял. В агде (MAlonzo) ограничений нет, там всё работает.

Ну бида значит.

Потому что 100500 летит в size_t и не летит в typename

И что? Это обычная ограниченная квантификация.

Тем что принимает constexpr термы (<: термы)?

Идем дальше. Чем твой констэкспр терм отличается от типа?

WAT? В омеге нужно, а расширении омеги уже не нужно?

Зависимые типы - это не расширение омеги, ты напутал с СоС.

Строго-нормализированной системы без эффектов.

ради бога - строгонормализованной системы без эффектов. И?

Так что то о чём мы говорим — за рамками таких рассмотрение, но разные реализации имеют право на существование

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

Я же сказал — исторически.

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

Так ты не стесняйся — ооп и функциональщина кратко, внятно. (комментарий), ЧЯДНТ?

Я не знаю, что это ты отпостил и на чем. Так что в душе неебу ЧТДНТ. Пиши на агде.

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

Да (это variable-term, а NF это просто отсутствие (\x.R)S в подтермах), только он не closed (есть подмножество замкнутых термов, так что есть сужение отношения редукций на них).

Замечательно.

Ты не понял — статический регион говорит, например, n == 10 это известно во время компиляции, поэтому zip запускается. Или он говорит n == m (пишем zip : {A B : Set} {n m : Nat} -> Vec A n -> Vec B m -> {_ : n == m} -> Vec (A * B) m — равенство уже не так просто decidable). И я сказал — 2) можно делать и в C++.

Зависимые типы - отдельно, омега - отдельно. С чего у тебя оно «уже в омеге»?

Зависимые типы содержат омегу (если содержат), так что всё что она делает они тоже делают, если не содержат (LF) — ещё раз «начиная с LF там T t, то есть SomeType SomeTermExpr, так что SomeTermExpr нужно редуцировать (уже термы, а не типы с их операциями)». Сама омега термы в типах не умеет редуцировать (да, и прикол в том, что если по твоему (любой терм реального языка), то тайпчек или всегда будет undecidable, или нужно идти по пути агды с монадками для partiality, coinduction и io).

Хоть одно отличие?

Выше я писал — оно типизировано (в омеге летают любые типы и максимум типизации это * => * и т.п., так что по арности можно различать, но не более).

Так куда оно редуцироваться-то будет?

Если редукций нет — оно не редуцируется, если есть — редуцируется. На этом все доказательства основаны — попробуй доказать a + 0 = a, например (при PM в редукциях по левой части).

Ведь любой пример из плюсов переписывается в омеге.

Вот не любой.

А так это что-то вроде LF, но с индексацией не по всем термам настоящего языка (не забываем, что в LF нет системы эффектов и частичности — нам выбирать что делать с настоящими термами языка которые расширяют ядерное LF, а так ведь любой пример омеги переводится в такую LF). И в DML с ATS так же.

Вот не любой.

Ну да есть примеры которые действительно не переписываются, но они с зависимыми типами не связаны. Вот такой пример допустим:

template <T>
T yoba(x T, y T){
  return x + y;
}

А так это что-то вроде LF, но с индексацией не по всем термам настоящего языка

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

Если редукций нет — оно не редуцируется, если есть — редуцируется. На этом все доказательства основаны — попробуй доказать a + 0 = a, например (при PM в редукциях по левой части).

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

Выше я писал — оно типизировано (в омеге летают любые типы и максимум типизации это * => * и т.п., так что по арности можно различать, но не более).

Ну хорошо, вместо system f_w возмем system f_w<:. Тут уже не будет ничего летать, все как надо. Скажешь что в system f_w<: зависимые типы есть?

Зависимые типы содержат омегу

Нет не содержат. Они полиморфизм содержат, а операторы над типами - нет. То есть в хависимых типах ты можешь сделать Vector<1>, но не можешь Vector<int>.

2) можно делать и в C++.

Ну так сделай.

Array<l> f(x: Array<n>, y: Array<m>){
  if (m == n){
    return zip(x, y)
  } else {
    return Array<void*>()
  }    
}

Или он говорит n == m

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

только он не closed

Ну а где написано что аргументом в зависимых типах можно только closed термы подставлять? Покажи. везде: «просто термы».

кстати неправильно ты тип на агде написал. Надо zip : {A B : Set} {n : Nat} -> Vec A n -> Vec B т -> Vec (A * B) n

кстати неправильно ты тип на агде написал. Надо zip : {A B : Set} {n : Nat} -> Vec A n -> Vec B n -> Vec (A * B) n

template <int T> Array<T> f();

У Array какая сигнатура? int -> typename?

Ну бида значит.

Почему? Если есть ограничения — всё равно это зависимые типы.

Зависимые типы - это не расширение омеги, ты напутал с СоС.

Я не путаю — в кубе две обычных омеги, и две с зависимыми типами (одна это CoC), так что эти две умеют что умеет омега. И ещё две с зависимыми типами — они не умеют редукции типов на основе операций над типами, но умеют редукции термов в типах, чего не умеет омега. Ну и вообще все четыре системы с зависимыми типами умеют редукции термов в типах.

И?

И при использовании такой формальной системы как ядра реального языка (или на ЛОРе при обсуждении плюсов) есть выбор что делать уже с частичными и эффектными термами — «и прикол в том, что если по твоему (любой терм реального языка), то тайпчек или всегда будет undecidable, или нужно идти по пути агды с монадками для partiality, coinduction и io».

Почему ты не согалсен с общепринятым определением?

ATTAPL, DML, ATS и Conor McBride тоже не согласны?

Ещё интересно что там в Idris.

Пиши на агде.

«В агде (MAlonzo) ограничений нет, там всё работает.»

А в DML с ATS — нет, там нет зависимых типов?

Надо zip : {A B : Set} {n : Nat} -> Vec A n -> Vec B т -> Vec (A * B) n

Нет, я говорю про два случая

n == 10 это известно во время компиляции, поэтому zip запускается.

в этом случае будет твоя сигнатура.

Или

Второй случай:

он говорит n == m (пишем zip : {A B : Set} {n m : Nat} -> Vec A n -> Vec B m -> {_ : n == m} -> Vec (A * B) m — равенство уже не так просто decidable)

другая сигнатура — в твоей тривиально decidable, тут более общее n == m (identity type).

У Array какая сигнатура? int -> typename?

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

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

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

Я не путаю — в кубе две обычных омеги, и две с зависимыми типами (одна это CoC), так что эти две умеют что умеет омега.

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

Ну и вообще все четыре системы с зависимыми типами умеют редукции термов в типах.

Редукции термов в типах умеют только зависимые типы. Омега умеет делать редукцию типов, но не редукцию термов. Ты уже вконец запутался.

И при использовании такой формальной системы как ядра реального языка (или на ЛОРе при обсуждении плюсов) есть выбор что делать уже с частичными и эффектными термами

И при чем тут это? Один хер в LF не только константные термы, но и те, на которых плюсы обламываются.

ATTAPL, DML, ATS и Conor McBride тоже не согласны?

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

А в DML с ATS — нет, там нет зависимых типов?

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

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

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

Нет, я говорю про два случая

Ну говори. А я говорю конкретно вот про этот: zip : {A B : Set} {n : Nat} -> Vec A n -> Vec B т -> Vec (A * B) n

Остальные случаи меня не интересуют.

в этом случае будет твоя сигнатура.

А если я так сделаю:

let m = n
let k = n
zip Array<k>(...) Array<m>(...)

Прежде чем продолжать наше общение — ооп и функциональщина кратко, внятно. (комментарий) что тут можно навертеть?

И про DML — http://www.ats-lang.org/PAPER/DML-jfp07.pdf, 4.4 где про run-time check и 4.5 — что-то тебе говорит? Что ты «выяснил»?

Ну и «Please note that Dependent ML (DML) is no longer under active development. As a language, it has already been fully incorporated into ATS.»

И про DML — http://www.ats-lang.org/PAPER/DML-jfp07.pdf, 4.4 где про run-time check и 4.5 — что-то тебе говорит? Что ты «выяснил»?

Спасибо, вот ты и подтвердил мою правоту. В ATS и DML можно ставить на место типового аргумента любой терм, не только известный на момент компайлтайма. В пункте 4.4 как раз такой пример - у xs и ys длина на момент компайлтайма неизвестна.

И да ответь таки на вопрос про П-тип для template

Вот такой пример допустим

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

Нет не содержат

Смотри лямбда куб — там две системы с омега и пи (одна CoC, другая зависимые типы первого порядка с операциями над типами). Вообще вся правая грань это зависимые типы (левая — полиморфизм, как ты говоришь).

Мы говорим только про LF? Ну ладно.

Ну так сделай

Я про такие статические регионы — Вышел CompCert 2.0 (комментарий).

Можно ли адаптировать к zip — ХЗ.

Ну а где написано что аргументом в зависимых типах можно только closed термы подставлять?

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

Array - индексированный интами массив.

P{x:int}.P(_:unit).array x — хочешь что-то сломать? (специальные скобочки как бы намекают).

Ты уже вконец запутался.

Все четыре системы (с ЗТ, правая грань) умеют редукции термов в типах — что не так?

А если я так сделаю

Ты про плюсы или про агду? Агда работает, плюсы работают (если у тебя let как val или constexpr).

var? Агда работает, в плюсах непонятно чего ты собрался инстанцировать таким образом.

Там концепт должен быть

Не должен он там быть. Такой код просто не должен компилироваться и все с полиморфизмом. Но в плюсах полиморфизм сломанный.

Смотри лямбда куб — там две системы с омега и пи (одна CoC, другая зависимые типы первого порядка с операциями над типами). Вообще вся правая грань это зависимые типы (левая — полиморфизм, как ты говоришь).

Зависимые типы - это одна грань. Полиморфизм - вторая грань. Операторы - третья грань. Есть зависимые типы без полиморфизма и без операторов. Есть зависимые с полиморфизмом. Есть зависимые с операторами. И есть зависимые со всем вместе (СоС). Но вообще из зависимых типов наличия операторов не следует.

Можно ли адаптировать к zip — ХЗ.

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

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

Ну то есть можно и не закрытие термы аргументом ставить?

Все четыре системы (с ЗТ, правая грань) умеют редукции термов в типах — что не так?

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

Агда работает, плюсы работают

Датычо? нука показывай плюсы.

Ну так ты должен был понять из того примера, что constraint solver будет стирать {n: nat} во время компиляции (поэтому zip там обозван более эффективным), так как в соответствующем регионе статично m = n — его можно стереть не знаю (что круче чем в плюсах, но то же стирание индексации), работает это за счёт типов length, _=_ (и zip, конечно) и dependent-if, то есть это не то что ты думаешь.

Отсюда же следует, что твои примеры с чтением n: nat и созданием списка такой длины (с индексацией по длине) не заведутся — constraint solver не знает что стирать, динамические типы не создаются. Иначе — возвращаемся к примеру с ATS, что там может быть не так?

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

Не должен он там быть

template <T> requires IsAbelianSemiGroup<T>
T yoba(x T, y T){
  return x + y;
}

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

Разумеется.

Ну то есть можно и не закрытие термы аргументом ставить?

И что? Если есть возможные редукции — они проводятся.

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

Редукция термов в типах происходит, а не типов.

Датычо?

«если у тебя let как val или constexpr»

или «непонятно чего ты собрался инстанцировать таким образом».

Что такое constraint solver не знаешь и решил слить пример на три строчки на ATS?

Можешь написать аналог (невозможного) template <size_t n> std::list<std::string, n> read_lines_from_file(...) на ATS?

template <T> requires IsAbelianSemiGroup<T>T yoba(x T, y T){ return x + y;}

И что? Это отменяет тот факт что компилируется код, который я до этого дал?

Редукция термов в типах происходит, а не типов.

Да нету там блять термов.

или «непонятно чего ты собрался инстанцировать таким образом».

Я ничо инстацировать не собирался. Мне вообще похуй на инстанцирование. Это детали реализации. Факт в том, что эта запись должна работать.

Все, тем АТС закрыта - написано, что указанный пример работает. А теперь ответь про П-тип в template

Это отменяет тот факт что компилируется код, который я до этого дал?

Он не компилируется, он вообще пропускается, до инстанцирования, то есть auto z = yoba((SomeModel)x, y) — инстанцируется для SomeModel и если у неё есть operator+, то всё работает (SomeGoodModel), иначе не компилируется (SomeBadModel). Концепт фиксирует интерфейс — более правильный чек получится.

А вообще в чём проблема с таким кодом? Это же как yoba :: IsAbelianSemiGroup t => t -> t -> t; yoba = (+).

Да нету там блять термов

В настоящих зависимых типах — есть. В негодных «зависимые типы без термов, так как я всё в омегу с подтипированием могу загнать, пох веники» — ну ок, что там редуцируется, name it. Я называю constexpr.

Факт в том, что эта запись должна работать.

Если в C++ вместо let будет constexpr, будет работать. Иначе — в C++ не будет, в Agda будет, мне интересно что будет в ATS.

Все, тем АТС закрыта - написано, что указанный пример работает.

Где? В статье про то как они бы хотели реализовать DML?

И важен не пример с zip, а пример с получением обычного list(SomeType, n) для n полученного во время выполнения — если этого нет, то всё тупо как в плюсах (zip работает, но если n статичны — он и в плюсах будет работать, решение уравнений для параметров шаблонов можно накостылять, если они не работают — лень проверять).

А теперь ответь про П-тип в template

Я выше написал — ну да, пи int, именуем n (делаем implicit/constexpr в плюсах), пи unit без зависимости и возвращаем список с индексом n.

Я выше написал — ну да, пи int, именуем n (делаем implicit/constexpr в плюсах), пи unit без зависимости и возвращаем список с индексом n.

Откуда ты взял unit? там нету никакого unit. Ну да ладно, какой тип вот у этого теперь?

template<T> void f();

Где? Там где ты сам указал.

И важен не пример с zip, а пример с получением обычного list(SomeType, n) для n полученного во время выполнения

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

Он не компилируется, он вообще пропускается, до инстанцирования

Ну а когда попытаешься инстанцировать никакой ошибки не будет. Хотя должна быть.

то есть auto z = yoba((SomeModel)x, y) — инстанцируется для SomeModel и если у неё есть operator+, то всё работает (SomeGoodModel), иначе не компилируется (SomeBadModel). Концепт фиксирует интерфейс — более правильный чек получится.

Я прекрасно знаю как работают шаблоны. Факт в том, что они работают _не так_ как полиморфизм. Они предоставляют сломанный полиморфизм. Даже если operator+ есть шаблон все равно не должен инстанцироваться, должна быть ошибка. Она должна быть еще там, когда мы вызываем + для произвольного типа внутри шаблона. То, что плюсы не чекают шаблон - проблема плюсов.

Это же как yoba :: IsAbelianSemiGroup t => t -> t -> t; yoba = (+).

Откуда ты взял IsAbelianSemiGroup? Нету его. Попробуй написать в хаскеле f: forall a. a -> a, let f x = x + 1. Сильно много у тебя работать будет?

В настоящих зависимых типах — есть.

Коненчо есть. Но речь-то об омеге.

В негодных «зависимые типы без термов, так как я всё в омегу с подтипированием могу загнать, пох веники»

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

Если в C++ вместо let будет constexpr, будет работать.

Она должна работать без «если». Просто работать. «если» она работает и в омеге.

мне интересно что будет в ATS.

Я не знаю ATS, по-этому не могу ничего сказать. Но если они говорят что у них есть зависимые типы - то будет работать. По определению П-типа. Другое дело, что у них может быть какой-то особый синтаксис (ну как {} скобочки в агде) или еще какая штука для передачи таких параметров. То есть в формализме зависимых типов такие типовые аргументы передаются как обычный параметр ф-и, но в реальных ЯП для удобства делают специальный «протокол передачи». Хотя это и не логично, ведь аргумент П-функции - обычный аргумент.

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

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

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

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

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

Ну так сам описание классов/интерфейсов/их отношений - оно разве не декларативно? :)

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

А так в той же скале вон иммутабельность по дефолту. Везде val val val.

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

Классы - это такие проагрейженные модули.

Оно +- везде так, в общем-то. Основная «претензия» к композиции этих модулей в традиционных языках.

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

Как макросы связаны с бойлерплейтом?

Т.е. макросы это борьба с копипастом

Не понял, откуда такой вывод? Даже близко не так. У тебя типы - это борьба с копипастом? Или ФВП - борьба с копипастом? Или те же классы - борьба с копипастом?

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

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

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

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

Основная «претензия» к композиции этих модулей в традиционных языках.

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

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

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

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

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

Стандартная либа, по-твоему, написана в хорошем стиле?

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

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

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

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

на шутауте то же самое

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

Как макросы связаны с бойлерплейтом?

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

Т.е. макросы это борьба с копипастом

Не понял, откуда такой вывод? Даже близко не так.

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

У тебя типы - это борьба с копипастом?

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

Или ФВП - борьба с копипастом?

Отчасти, безусловно.

Или те же классы - борьба с копипастом?

Конечно.