История изменений

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

*Авторы 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.

Ну так вот у тебя куча своих 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.

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

И мне совсем не нужно передавать одну на место другой, а если нужно — должны быть общие на всех интерфейсы (теории), эквивалентность доказывать не нужно (ну то есть если ты не метаешься между iterator из std и range из 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 будет.

Не надо.