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

Пример? Чего нельзя?

Ничего нельзя. Ну по стандарту плюсов. Ну там так и написано: «нельзя подставить любой терм в шаблон».

Как type traits (http://www.cantrip.org/traits.html, http://accu.org/index.php/journals/442, http://www.cplusplus.com/reference/type_traits/) только наоборот — можно делать выбор типа по значению.

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

Вообще кайф

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

Вообще кайф :) Ладно, я в маакрасах-двудольных-графах не разбираюсь.

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

Это тебе даже не просто CoC - это совсем уже пиздец, что можно делать :)

Ну и это обычный недо-полиморфизм (так как типы в плюсах не чекаются, ага, динамика :)). Где ты там зависимые типы увидел? Только числа, естественно, надо определить как Zero/Succ будет.

Ну пусть видят.

*Авторы Frama-C, им же видней. Как и авторам gcc/graphite или llvm/polly.

Ну так вот у тебя куча своих sorted в каждой либе

И мне совсем не нужно передавать одну на место другой, а если нужно — должны быть общие на всех интерфейсы (теории), эквивалентность доказывать не нужно (ну то есть если ты не метаешься между iterator из std и из boost в проекте, например, но так же никто не делает).

Ну да, а потом можно посмотреть на тот же код из frama-c где аннотаций больше чем собственно самого кода.

А можно не смотреть, а подумать :) Привязать implicit свойство к аргументам в сигнатуре — большая проблема прям.

Где?

Конкретнее:

template <typename T, size_t size>
struct array;

template <typename T, size_t n, size_t m>
array<T, n + m> concat(array<T, n> const&, array<T, m> const&);

как будет на Haskell 98?

А bind у монад он же forall (a :: *). (_ :: a) ... (m a), то есть по type (a :: *), а не по term (n :: size_t).

просто хуячим простую типизированную лямбду, макросистему поверх нее - и получаем все, что надо - искаробки?

Ничего ты не получаешь. Вот в системе основанной на CIC ты определяешь типы, пишешь утверждения и доказываешь их свойства. Например определяешь _=_ : {A} -> A -> A -> Set и пишешь функцию sym : {x y} -> x = y -> y = x; sym refl = refl, а макросы тут вообще каким боком? Как будем определять типы, писать утверждения и доказывать теоремы? Ну и что конкретно брать — ничего ж нету, одни петухи с агдами.

Где ты там зависимые типы увидел?

Не видишь, что n_vector и NList это один в один?

Только числа, естественно, надо определить как Zero/Succ будет.

Не надо.

*Авторы Frama-C, им же видней. Как и авторам gcc/graphite или llvm/polly.

Нет, не видней.

И мне совсем не нужно передавать одну на место другой

На практике нужно.

а если нужно — должны быть общие на всех интерфейсы

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

Привязать implicit свойство к аргументам в сигнатуре — большая проблема прям.

Ну и ты ту гору аннотаций просто перенес из аннотаций в определение типа. Какая разница? Гора аннотаций осталась.

как будет на Haskell 98?

Ну также один в один.

А bind у монад он же forall (a :: *). (_ :: a) ... (m a), то есть по type (a :: *), а не по term (n :: size_t).

Так в плюсах тоже не по term. n - это не терм, а тип, просто сахарок Zero/Succ на уровне типов.

Ничего ты не получаешь.

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

а макросы тут вообще каким боком?

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

Как будем определять типы, писать утверждения и доказывать теоремы?

Ну да, как? показывай, интересно будет поглядеть :)

Не видишь, что n_vector и NList это один в один?

Я вижу в обоих случаях обычный полиморфизм. При чем тут зависимые типы?

Не надо.

Надо, если сахара нету, как в плюсах. Если сахар есть, то не надо, да.

мне кажется, ТС путает ооп и с++. Это как бы не одно и то же, а ты в своих рассуждениях регулярно подменяешь эти понятия.

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

Ну и google://c++ fqa

и причем тут функциональщина?

Нет, не видней.

Кхм, ничего не имею возразить :)

На практике нужно.

На практике их нет. Не напишешь ты общий интерфейс на каждый чих.

Ты говоришь о сферическом в вакууме программировании.

Нет ты. Ещё раз — если интерфейсов нет, то никакой передачи одного типа на место аргумента который (в статике) ждёт другой быть не может, так что не понятно что ты собрался конвертировать во что. А если интерфейсы ООП, концепты обобщённого программирования или теории зависимых типов есть, и Вася с Петей написали зачем-то в рамках одного проекта два таких, решающих схожие задачи, то кому-то придётся их совмещать — так это не проблема зависимых типов, и непонятно почему ты думаешь, что в их случае конвертировать теории это накладно (я пробовал в агде — те же тривиальные враперы, а там много теорий в Algebra.* и Сategories.*, например).

Гора аннотаций осталась.

Откуда гора? «Ты говоришь о сферическом в вакууме программировании». Если я хочу гарантии для operator[](size_t i) для std::array<T, n>, то не гора, а добавление только <less<i, n>> после круглых скобок и вызовы вида if (i < n) { ... x[i]; ... } else { ... x[i]; <- static error ... } (operator<, less и bool должны быть связаны, dependent-if должен создавать контекст с пруфом, сами свидетели в угловых скобках после круглых в данном случае стираются во время компиляции). А если не хочу — будет как было.

Ну также один в один.

#include <array>

template <typename T, size_t a, size_t b>
std::array<T, a + b> concat(std::array<T, a> const& x, std::array<T, b> const& y) {
    std::array<T, a + b> z;
    std::copy(x.begin(), x.end(), z.begin());
    std::copy(y.begin(), y.end(), z.begin() + x.size());
    return z;
}

#include <cstdio>

int main() {
    for (auto const& x : concat(std::array<int, 3>{{1, 2, 3}},
                                std::array<int, 2>{{4, 5}}))
        printf("%d\n", x);
}

давай на хаскеле98 компилируемый и работающий с main (массивы-аргументы можно сделать переменными, результат concat — тоже, с auto или без), а потом ещё почитаем ассемблер :).

Так в плюсах тоже не по term. n - это не терм, а тип, просто сахарок Zero/Succ на уровне типов.

Мы этого не знаем. А знаем мы, что n можно передать в обычную (constexpr) функцию на место аргумента с обычным типом std::size_t, так что таки терм.

с++, где захуячена макросистема на простой типизированной лямбде

Ага, с quote и defmacro, «макросистема шаблонов», блин. Это ложная предпосылка про шаблоны-макросы, так что я не комментирую дальше. Я dependnet product показал (concat для std::array), ссылка на википедию про то что LambdaP в лямбда кубе это уже зависимые типы — была, NList : Set → ℕ → Set — тоже показал, про type -> type, term -> type, type -> term в type-level (которые делаются не какими-то там макросами, а обычной рекурсией с выборами — структуры играют роль таких type-level рекурсивных функций, причём если посмотреть, то g++ и clang++ умеет для них оптимизации, так что код получается хороший в итоге) сказал, про стандартные type traits (типа is_same) — тоже. Так что тут вопрос обратный — что такого умеют шаблоны, что не вкладывается один в один в зависимые типы (потому что макросы умеют кучу всего, поэтому они к зависимым типам не имеют прямого отношения).

Я вижу в обоих случаях обычный полиморфизм.

полиморфизм

Слово-паразит?

 — ?, — Обычный полиморфизм, — А, ну всё понятно, чё.

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

Так я же тебе объясняю - да, эта проблема есть и БЕЗ зависимых типов. Но без зависимых типах ее:

1. мало

2. легко решается написанием враппера вокруг нужного интерфейса

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

Откуда гора?

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

то не гора, а добавление только <less<i, n>> после круглых скобок и вызовы вида if (i < n) { ... x; ... } else { ... x; <- static error ... }

И доказательства корректности, откуда и будет гора.

давай на хаскеле98 компилируемый и работающий с main (массивы-аргументы можно сделать переменными, результат concat — тоже, с auto или без), а потом ещё почитаем ассемблер :).

Ну например как-то так:

data Zero
data Succ a

class Nat a
instance Nat Zero
instance (Nat a) => Nat (Succ a)

class (Nat a, Nat b, Nat res) => Plus a b res
instance Plus a Zero a
instance (Plus a b res) => Plus a (Succ b) (Succ res)

data (Nat n) => Array t n

concat :: (Plus m n res) => Array t m -> Array t n -> Array t res

А знаем мы, что n можно передать в обычную (constexpr) функцию на место аргумента с обычным типом std::size_t, так что таки терм.

Берем обычную полиморфную функцию id: a -> a. Мы в нее на место типового аргумента может подставить значение синглтон, которое представляет тип на уровне термов (например там Bool, String и т.д.) и имеет тип Type. Вуаля, это зависимые типы!!11!

Ага, с quote и defmacro, «макросистема шаблонов», блин.

Нет, обычные syntax-rules

Это ложная предпосылка про шаблоны-макросы, так что я не комментирую дальше.

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

Я dependnet product показал

Не показал. Ты показал _обычный полиморфизм_. Иди уже прочитай tapl, ну я не знаю. Еще раз, если принять твою тчоку зрения (что в плюсах зависимые типы), то сразу получаем два следствия:

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

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

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

Не понял о чем ты. Если ты показываешь полиморфизм - я и говорю, что это полиморфизм. А что еще я должен сказать?

Так я же тебе объясняю

А я же объясняю — врапер вокруг теории пишется не сложнее врапера вокруг интерфейса (твой второй пункт).

а при добавлении зависимых типов объем работ возрастает на порядки

У меня evidence для такого факта нет.

И доказательства корректности, откуда и будет гора.

at : {A : Set} {n : ℕ} → Vec A n → (i : ℕ) → {_ : i < n} → A
-- 
-- ^ Вот, главным образом, то что ниже это деталь реализации для Vec (списки).
-- 
at [] _ {()}
at (x ∷ _) 0 = x 
at (_ ∷ xs) (suc n) {s≤s p} = at xs n {p}
-- 
-- С настоящим вектором будет просто
-- 
-- at x i = at# x i
-- 
-- где at# уже небезопасен, всё равно сигнатура знает что i < n.

xs : Vec ℕ 3
xs = 1 ∷ 2 ∷ [ 3 ]

t : ℕ → ℕ
t i with i <? 3
... | yes p = at xs i {p}
... | no _ = 0
-- 
-- ^ тут бы хотелось, чтобы p в первой ветке протаскивался автоматически, 
-- адаптация с заменой with (dependent pattern-matching) на dependent-if
-- и даст
-- 
-- if (i < 3) { return xs[i]; } else { return 0; }

не вижу никакой горы в данном случае.

Ну например как-то так

1) Это не Haskell98 и даже не Haskell2010 — если уж использовать расширения GHC, то сразу GHC 7.8 в котором это уже можно (?) сделать, но GHC это зависимые типы — http://stackoverflow.com/questions/12961651/why-not-be-dependently-typed#1324.... 2) -Wall — -XDatatypeContexts is deprecated: It was widely considered a misfeature, and has been removed from the Haskell language. 3) Тут типы вместо термов же для Nat. 4) Я просил компилируемый и работающий с main.

А вообще непонятно как это делать — c DataKinds непонятно как писать (n + m) в Array, с TypeLits computational не заводится (так что unsafeCoerce). С TypeFamilies всё ещё нужно костылять термы на типах:

{-# LANGUAGE KindSignatures, TypeFamilies, TypeOperators, GADTs #-}

data Z
data S a

type family x :+ y :: *
type instance Z :+ y = y
type instance S x :+ y = S (x :+ y)

infixr 5 :.
data Array (a :: *) :: * -> * where
  E :: Array a Z
  (:.) :: a -> Array a n -> Array a (S n)

infixr 4 ++.
(++.) :: Array a n -> Array a m -> Array a (n :+ m)
E ++. ys = ys
x :. xs ++. ys = x :. (xs ++. ys)

Если только TypeNats заработают в будущем релизе.

Берем обычную полиморфную функцию id: a -> a. Мы в нее на место типового аргумента может подставить значение синглтон, которое представляет тип на уровне термов (например там Bool, String и т.д.) и имеет тип Type. Вуаля, это зависимые типы!!11!

Ничего не понял. «представляет тип на уровне термов» — мозги динамикой сломал?

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

size_t в шаблоне это обычный size_t, никакой не сахар.

Шаблоны плюсов - это по факту ограниченные макросы

#include <type_traits>
template <typename T> struct A { static_assert(false, "A"); };
template <typename T> struct B { static_assert(false, "B"); };
int main() { B<A<void>> x; }

Стратегия вычислений не macro-like (http://en.wikipedia.org/wiki/Evaluation_strategy#Call_by_macro_expansion), а самая обычная. Ну и мне всё равно — я пишу программу с шаблонами которая компилируется или нет, что там внутри происходит меня не волнует (но на макросы не похоже, см. выше).

Ты показал _обычный полиморфизм_

Вот это — http://en.wikipedia.org/wiki/Intuitionistic_type_theory#.CE.A0-types, там даже пример такой же (Vec), http://en.wikipedia.org/wiki/Dependent_type#Systems_of_the_lambda_cube — first order dependent type theory. В «простой полиморфной лямбде» этого нет. Что такое «обычный полиморфизм» я не знаю. «макросы обычные syntax-rules» над «типизированной лямбдой» это в раздел НФ.

Если ты показываешь полиморфизм

А тут я показываю рекурсивную шаблонную структуру / функцию <typename, size_t> -> typename / Set → ℕ → Set, без всяких разночтений. Опять же, в обычном полиморфном (параметрически, с подтипированием) этого нет, но есть в зависимых типах, ну и в шаблонах C++ — почему я должен думать про какие-то левые макросы над лямбдой мне не понятно.

Стратегия вычислений не macro-like

Хотя вру, в общем случае выглядит как macro-like — подвыражения ждут пока инстанцируются внешние (они же по требованию инстанцируются, так что от внешних), просто обычная техника это звать ::type или ::value, в этом случае получается обычная стратегия от внутренних к внешним:

#include <type_traits>

template <typename T>
struct A {
    static_assert(std::is_void<T>(), "A");
    typedef void force;
};

template <typename T>
struct B1 {
    static_assert(std::is_void<T>(), "B1");
};

template <typename T>
struct B2 {
    static_assert(std::is_void<typename T::force>(), "B2");
};

int main() {
    B1<A<int>> x;
    B2<A<int>> y;
}

А я же объясняю — врапер вокруг теории пишется не сложнее врапера вокруг интерфейса (твой второй пункт).

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

не вижу никакой горы в данном случае.

Взял тривиальный пример и радостно рассказываешь ,что в этом случае гор нет. Ну ок, только вот практика далека от твоих сферических рассуждений. Сколько на агде будет занимать доказательство ВТФ? А может легко быть и такое, что доказательство сведется вообще к одной из нерешенных мат. проблем :)

1) Это не Haskell98 и даже не Haskell2010 — если уж использовать расширения GHC

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

то сразу GHC 7.8 в котором это уже можно (?) сделать

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

но GHC это зависимые типы — http://stackoverflow.com/questions/12961651/why-not-be-dependently-typed#1324....

Опять подмена понятий. Ну и что что ГДЕ-ТО ТАМ в GHC есть какие-то фичи, которые может и дают зависимые типы? Я же этих фич не использовал. Все, что я делал - это старая добрая System f_w - полиморфные функции и операторы над типами (Plus тут костыльно сделанный оператор над типами, как раз).

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

Разница между омегой и зависимыми типами в том, что в омеге любое представление терма типом известно наперед на уровне компайлтайма, а вот в зависимых типах - может быть и неизвестно. Например, если аргумент шаблона требует подставить число, то нам _надо_ подставить число. Когда шаблон последний раскроется - там должен быть конкретный number. Аналогично и с моим примером на хаскеле - когда тайпчек будет произведен, то все эти массивы будут иметь _четко заданную длину_. Не может быть массива, длина окторого не будет выведена во время тайпчека. А в случае зависимых типов там может и не быть конкретный number, там может быть некоторый терм типа number (любой), значение которого на момент компиляции неизвестно (возможно, это будет четный number, или там нечетный, или 0 < number < 10, или вообще _любой_ number (например, если его вводит пользователь)).

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

Ничего не понял.

Твои проблемы. Я же не виноват в том, что ты понимаешь, чем отличается полиморфизм от зависимых типов.

size_t в шаблоне это обычный size_t, никакой не сахар.

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

Стратегия вычислений не macro-like

Ага, конечно :)

Иксперт в треде.

Ну и мне всё равно — я пишу программу с шаблонами которая компилируется или нет, что там внутри происходит меня не волнует (но на макросы не похоже, см. выше).

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

Вот это — http://en.wikipedia.org/wiki/Intuitionistic_type_theory#.CE.A0-types, там даже пример такой же (Vec),

Вобщем я выше все объяснил.

В «простой полиморфной лямбде» этого нет.

Есть.

Что такое «обычный полиморфизм» я не знаю.

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

«макросы обычные syntax-rules» над «типизированной лямбдой» это в раздел НФ.

Замечательно объяснять вещи, в которых не разбираешься, «разделом НФ». Ну дурак - он и есть дурак.

А тут я показываю рекурсивную шаблонную структуру / функцию <typename, size_t> -> typename / Set → ℕ → Set, без всяких разночтений.

Что и есть полиморфизм.

Опять же, в обычном полиморфном (параметрически, с подтипированием) этого нет

Есть, конечно же. Я даже показал пример на хаскеле. Тебе переписать его на System f_w (хотя хаскель и есть System f_w ... ну да ладно), чтобы уже совсем никаких сомнений не осталось? Или ты начнешь рассказывать, что System f_w имеет «элементы зависиимых типов»? :)

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

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

просто обычная техника это звать ::type или ::value

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

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

Дурашка, ты же написал код, но даже не понимаешь как он работает. тт. Ничего там нету «изнутри наружу». Шаблоны в плюсах вообще так не умеют (в отличии от макросов, кстати - их такой-то матерью можно заставить навыворот раскрываться), они только обычную макроподстановку умеют. Хоть ты ужом вертись, хоть что делай - но кроме стратегии обычной макрпоодстановки пплюсы ни во что CANNOT INTO

3) Тут типы вместо термов же для Nat.

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

let m = read
if (m = 1) {
  let v1 = Array<int, m>(0)
  print(v1[0])
}

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

У тебя в плюсах тоже типы вместо термов для Nat.

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

Вот даже в твоем любимом хаскеле про это написано: http://ghc.haskell.org/trac/ghc/wiki/TypeNats/Basics

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

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

я не анонимус, но тоже отвечу: racket, ссала.

scala выглядит страшно со всех сторон, вообще: java, pascal, haskell, io, ruby - все в одном флаконе. Как по мне, чисто эстетически уродливое создание.

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

Ну, вот мне чисто теоретически интересно, могут ли получиться статически типизированные lisp-like macro? Т.е. это такой статически (фаза проверки - например компайл пользовательского выражения) типизированный eval. Так бывает? :)

java, pascal, haskell, io, ruby - все в одном флаконе

и можно понапихать еще! это самое замечательное!

а еще можно юзать Jetbrains MPS и смешивать всё подряд (но вначале это «всё подряд», к сожалению, придется самостоятельно переписать под MPS.. хотя, многое уже есть, слышал про C++)

Я вообще фанат скалы -.-

И racket, как единственный язык, в котором есть человеческая макросистема. Ну для меня racket - это как хаскель для теоркатофагов.

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

А вообще все от предметной области зависит, конечно.

слышал про C++)

У С++ хотя бы есть историческое оправдание.

А ты тот же anonymous, что quasimoto дискутировал?

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

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

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

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

А с чего вдруг сомнения? Из того что я фонат скалы, у которой статическая типизация, внезапно? :)

А с чего вдруг сомнения? Из того что я фонат скалы

Да :)

у которой статическая типизация, внезапно? :)

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

Я вообще в скале вижу такой современный с++. Со всеми плюсами и недостатками такого положения.

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

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

Ой, не скалу ли я описал сейчас? :)

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

Вообще, если о макросах, то глядя на тот же racket (ну а больше не на что, если говорим про макросы)

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

я вижу, что можно ограничить возможности макросов в плане произвольной трансформации АСТ

С какой целью?

но расширить (или сделать более удобными через продуманный АПИ) возможности работы с лексическим контекстом

Можно пример словами?

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

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

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

Например?

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

Да, я об этом.

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

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

Это может стандартный метод решения каких-либо проблем (который будет применяться в языке часто и без опаски)

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

это может быть инструмент разработчика языка

Закрытый от пользователей? Типа у нас тут есть ридер-макросы но вам определять свои нельзя, как в clojure? :)

вынесение языков фич в библиотеку

?

повышенная гибкость компилятора и т.п.)

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

это может быть средство написания дслей

DSL = новая семантика + (возможно) новый синтаксис. Т.е. это обычные макросы и есть.

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

Это вроде то же самое.

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

Спорно.

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

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

С какой целью?

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

Можно пример словами?

Сейчас, чтобы чего-то в лексический контекст добавить, изменить и использовать, приходится генерить свои defie/define-syntax - по-нормальному надо все это делать через вызовы соответствующего АПИ в экспандере, Без генерации. Потому что реально-то код нам не нужен - он тут вторичен и генерится побочно, чтобы решить задачу околольным путем. Через АПИ будет и понятнее и короче и более гибко и больше возможностей и вообще всем лучше.

Да, я об этом.

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

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

Естественно, не обязательно. Для начала нам нужны аннотации, которые будут указывать, какие переменные макрос внедряет/переопределяет в лексическом контексте. Это в динамическом ЯП даже, тут типов нет вообще :)

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

Ну, это кодогенерация будет.

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

Закрытый от пользователей? Типа у нас тут есть ридер-макросы но вам определять свои нельзя, как в clojure? :)

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

?

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

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

Да всем понятно, потому что по факту в этом смысле все современные языки используют макросы - есть некий kernel language, в который рассахаривается host-язык.

DSL = новая семантика + (возможно) новый синтаксис. Т.е. это обычные макросы и есть.

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

Спорно.

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

В хаскеле если убрать дефолтную лень, убрать монады

В хаскеле - монады способ взаимодействия с hello-real-world, что взамен их?

и провести ревизию расширений

Ну, это эволюционный процесс. Развитие haskell, кстати, сильно напоминает развитие python - и там, и там «добродушные пожизненные диктаторы» давно ушли за рамки компетентности и ориентирования в проблемах современности (я исхожу из достаточно подробных и качественных интервью SPJ и Гвидо, напечатанных в «Coders at Work»). Но сами проекты развиваются демократично, в процессе разработки haskell присутствует аналог PEP и обсуждений вокруг да около, это позитивно.

сделать _нормальный_ полиморфизм вместо этих тайпклассов

Нормальный это какой? Или как где? Что не так с тайпклассами (признаюсь, я еще не до конца прокрутил возможные варианты их anti-usecase'ов, но на поверхностный взгляд - они кажутся прекрасными по сравнению с «обычным» ооп)?

Ой, не скалу ли я описал сейчас? :)

Начнем с того, что у нее синтаксис еще более вырвиглазный, чем у хаскеля, платформочка не айс, встроенный в язык xml это вообще как понимать? Если scala вся из себя такая декларативная, то нафейхоа там ооп вообще? У меня в последнее время возникают серьезные сомнения в его нужности. Это конечно все мое имхо, основанное на достаточно с поверхностным ознакомлением со скалой. Но я в ней, кажется, видел даже неявно приведение типов *omg*.

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

Я реально не понял этой аналогии...

В хаскеле - монады способ взаимодействия с hello-real-world, что взамен их?

Линейные типы, как в Clean. А вообще польза от отделения эффектов весьма сомнительна.

Ну, это эволюционный процесс.

Причины понятны, но результата это не меняет.

Нормальный это какой? Или как где?

Генерики с человеческой ad-hoc перегрузкой.

Что не так с тайпклассами (признаюсь, я еще не до конца прокрутил возможные варианты их anti-usecase'ов, но на поверхностный взгляд - они кажутся прекрасными по сравнению с «обычным» ооп)?

В этом и проблема, что «по сравнению с обычным ООП». Подтипирование (ООП) - отдельно, ad-hoc полиморфизм - отдельно, а тайпклассы - попытка одной жопой усидеть на двух стульях.

Начнем с того, что у нее синтаксис еще более вырвиглазный

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

платформочка не айс

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

Если scala вся из себя такая декларативная, то нафейхоа там ооп вообще?

Тут не понял вопроса. ООП (подтипирование, это же плюсовое ООП, а не смолтолковское) - вполне декларативная концепция,

Но я в ней, кажется, видел даже неявно приведение типов *omg*.

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

Нет смысла называть какие-то общие проблемы типа «кодогенерации» или «расширения синтаксиса». Макросы никто для кодогенерации или расширения синтаксиса не использует, Таких проблем вообще ни перед кем никогда не стоит. Проблемы всегда более конкретны.

Нет смысла называть какие-то общие проблемы типа «кодогенерации» или «расширения синтаксиса».

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

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

Да.

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

Потерянные возможности можно, как ты говоришь, вынести в специальный API.

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

Оно и сейчас, вроде, так используется в том же racket. Даже в доке куча примеров на макросах, от которых возникает вопрос нафейхоа? Имхо это все неудачно. Для применения макросов вместо фвп имхо должна быть нормальная аргументация перед примером. Вообще у рэкета в документации ментальные косяки на тему тех же вебсерверов с генерацией html на sexp - так никто не делает и показывать это вредно и некомпетентно. Могли бы написать хотя бы какой-то мини вебфреймворк и показать преимущества языка, но нет - пацаны завязли в эпохе cgi. Хотя бы скопировали что ле один из популярных фреймворков для вебни. И orm показали бы с прозрачной трансляцией из sexp в sql, а так несерьезно.

Хочешь какую-то фичу, типа type famylies - написал библиотеку. И не надо ждать пока кто-то из мейнтейнеров на горе свистнет

У тебя конкретные какие-то есть proposals оформленные или так, чисто на интуитивном уровне?

есть некий kernel language, в который рассахаривается host-язык.

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

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

Это почему еще? Есть мнение что совсем мелкий сахарок нафиг не нужен или под него можно приспособить макросы «для написания полноценных дсэлей» с небольшим ущербом для сахарка, чтоб еще неповадней было.

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

И для одного языка необходимо будет писать стопицот макростем, нафиг это надо?

Линейные типы, как в Clean.

Не знаю, не смотрел.

Нормальный это какой? Или как где?

Генерики с человеческой ad-hoc перегрузкой.

Т.е. «человеческий полиморфизм» это как в плюсах? :)

Если scala вся из себя такая декларативная, то нафейхоа там ооп вообще?

Тут не понял вопроса. ООП (подтипирование, это же плюсовое ООП, а не смолтолковское) - вполне декларативная концепция,

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

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

Странно все это, я еще посмотрю конечно, но со стороны это звездецовая жесть все.

Это не общие проблемы

Да это вообще не проблемы. Это методы решения проблем, причем даже не методы - а целые обширные классы методов.

Потерянные возможности можно, как ты говоришь, вынести в специальный API.

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

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

А никто и не применяет макросы вместо ФВП. Это разные инструменты для решения разных задач. Надо применять макросы _вместе_ с ФВП, а не _вместо_ ФВП :)

Вообще у рэкета в документации ментальные косяки на тему тех же вебсерверов с генерацией html на sexp

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

У тебя конкретные какие-то есть proposals оформленные или так, чисто на интуитивном уровне?

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

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

Ну сути не меняет, point ты понял.

Это почему еще?

Да вот так.

Есть мнение что совсем мелкий сахарок нафиг не нужен

Ну вон в соседнем треде один товарищ сокрушается, что в скале нету сахарка для монад и прям вот из-за этого плохо все. А с макросами - проблема на 10 строк.

под него можно приспособить макросы «для написания полноценных дсэлей» с небольшим ущербом для сахарка

В этом-то плане конечно да, можно, но в результате будут набигать и кричать «вашими макросами можно выстрелить в ногу, блаблабла». А сахарными макросами не выстрелишь особо.

И для одного языка необходимо будет писать стопицот макростем, нафиг это надо?

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

Не знаю, не смотрел.

Прелесть в том, что там можно сделать то же IO, но, в отличии от хаскеля, его можно типизировать. В хаскеле то оно ad-hoc работает. Типа «зуб даем, ничо не сломается». А в Clean несломаемость IO-монадки можно на уровне типов гарантировать.

Т.е. «человеческий полиморфизм» это как в плюсах? :)

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

Странно все это, я еще посмотрю конечно, но со стороны это звездецовая жесть все.

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

Очень веселое утверждение, честно.

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

А так в той же скале вон иммутабельность по дефолту. Везде val val val. То есть тут ООП как способ композиции методов. Классы - это такие проагрейженные модули.

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

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

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

Bound checking же — куча багов на эту тему, пока это либо баги, либо проверки в рантайме на _каждую_ операцию типа at. А данный пример делает at без проверок в рантайме, но с выводом того что весь синтаксический регион хороший в плане значений индексов — вместо кучи проверок на каждую операцию (там цикл, например) будет одна проверка на весь регион.

На самом деле это настолько же банально, как и сделать assert(i < n) на весь «регион» и использовать небезопасный operator[] (при условии, что i не уедет), просто с проверками на уровне системы типов (точно не уедет).

А ВТФ доказывать не нужно в программировании, давай не будем переводить стрелки — в ЯП зависимые типы используются (или ещё нет :)) для одного, в пруф ассистентах — Почему компьютеры не проверяют корректность доказательств математических теорем? (комментарий), http://www.ams.org/notices/200811/tx081101370p.pdf.

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

Возьмём для примера аксиомы тайпклассов хаскеля — их знают, но в языке их как бы нет (RULES это другое), так вот, для большинства функторов и т.п. эти теоремы доказываются просто типа там id или const, такого рода вещи. Короче, я вижу наоборот — многие вещи которые знают и имеют в виду без зависимых типов с зависимыми типами доказываются элементарно. Ну а если что-то совсем не доказывается — ну и ладно, не будет это доказывать вообще.

Понял разницу?

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

Твои проблемы.

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

id : P(A : Type). P(_ : A). A — так? При этом concat : P(A : Type). P(n : Size). P(m : Size). P(_ : Array A n). P(_ : Array A m). Array A (n + m).

То есть

The system \lambda \Pi 2 of second order dependent types is obtained from \lambda \Pi by allowing quantification over type constructors. In this theory the dependent product operator subsumes both the \to operator of simply typed lambda calculus and the \forall binder of System F.

id : \forall a. a -> a из SystemF переводится в систему с зависимыми типами, \forall и -> заменяется P. В системе с зависимыми типами есть concat, есть она в SystemF?

Whereas simply typed lambda calculus has variables ranging over functions, and binders for them, System F additionally has variables ranging over types, and binders for them.

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

System Fω does not permit mappings from values to types (Dependent types), though it does permit mappings from values to values ( abstraction), mappings from types to values (abstraction, sometimes written ) and mappings from types to types ( abstraction at the level of types)

Тоже не вижу.

При этом ты не можешь подставить терм типа size_t на то место - только значение типа size_t

Я могу подставить терм. То есть нужно подставить терм не в нормальной форме? Ок, любые арифметические операции, вообще вызовы любых constexpr функций и т.д. — нормально подставляется. Один из разработчиков CLang говорил, что constexpr как раз был самой сложной в реализации фичей из всего C++11 (сложнее лямбд и variadic, например).

Вобщем я выше все объяснил.

Так ты много чего «объяснял», особенно про SystemF периодически (и неправда).

Есть.

Напиши тип concat.

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

Terms depending on types, or polymorphism. System F, aka second order lambda calculus, is obtained by imposing only this property.

То есть SystemF, но пусть будет вся левая грань. А правая — уже зависимые типы (там есть P). Осталось рассказать как в системах левой грани типы могут зависеть от термов, то есть как там пишутся вещи которые я показывал (функции с ... term ... -> type и зависимостями).

Тебе переписать его на System f_w (хотя хаскель и есть System f_w ... ну да ладно), чтобы уже совсем никаких сомнений не осталось?

Перепиши, пожалуйста.

Замечательно объяснять вещи, в которых не разбираешься, «разделом НФ».

Ну так где оно — типизированная лямбда и макросы syntax-rules? Racket? И что, получается array, concat и n_vector (CIC не прошу)?

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

Ты забавно придумываешь мне образ :) Хотя ТК и Баез (ссылка на баеза в треде, офигеть просто o_0, но я-то тут причём, это всё октонионы :)) мне как-то более-менее ||, ничем не особеннее прочих вещей.

Ничего там нету «изнутри наружу».

Ну по идее да — static_assert B2 не успевает сработать, так как срабатывает он у A, но B2 раскрывается раньше A, то есть сверху опять.

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

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

в плюсах можно циферки писать вместо Zero/Succ

Ну нет же, там любые термы, просто compile-time (constexpr) и это tradeoff.

Вот даже в твоем любимом хаскеле про это написано

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