В чём профит от Eiffel...

как в статике будет проверятся то что индекс не выходит за границы массива?

if idx >= 0 && idx < arr.len() {
    // здесь точно всё нормально
}

не?

Не, я не об этом. Представим что вот этого куса кода и нет. Вопрос: будет ли ругаться анализатор и на что.

Это к вопросу что не получатся ли в итоге зависимые типы («idx зависит от arr»).

Представим что вот этого куса кода и нет. Вопрос: будет ли ругаться анализатор и на что.

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

Это к вопросу что не получатся ли в итоге зависимые типы («idx зависит от arr»).

Брать информацию из предусловия или определения типа - разница не принципиальная.

Никакие зависимые типы для проверки выхода за пределы массива не нужны. Простейший Хаскель:

module SafeArray (SafeIdx, SafeArray, checkIdx, at) where

data SafeArray a = ...

newtype SafeIdx a = SafeIdx a

at :: SafeArray a -> SafeIdx Int -> a
at a (SafeIdx i) = unsafeAt a i

checkIdx :: SafeArray a -> Int -> Maybe (SafeIdx Int)
checkIdx a i | i >= 0 && length a > i = Just (SafeIdx i)
             | True = Nothing

Поскольку конструктор SafeIdx не экспортирован, единственный способ создать SafeIdx — с помощью ф-ции checkIdx:

main = do
  i<- getUserInput
  let a = SafeArray ...
    x = a `at` i -- Type error
    x' = case checkIdx a i of
             Nothing -> ...
             Just i' -> a `at` i' -- Ok. Safe indexing with zero runtime overhead.

Safe indexing with zero runtime overhead.

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

Ну, даже в таком простейшем примере индекс можно повторно использовать, например, с zero overhead ©. Для более интересных случаев доказательства делаются с помощью арифметики Пеано на тайп-левеле. Это тоже всё возможно в обычном хаскеле.

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

Не знаю, как ты с помощью арифметики Пеано докажешь, что safeIdx + 1 дает safeIdx, но спорить не стану.

Это интересно, но, по сути, это обычная обёртка над int. Я бы не назвал это контрактом.

Это не совсем «надстройка». В данном случае конструктор SafeIdx играет роль приложенного к значению доказательства определённого свойства этого значения.

Поскольку конструктор SafeIdx не экспортирован, единственный способ создать SafeIdx — с помощью ф-ции checkIdx:

Я совсем не копенгаген в Haskell, но что будет, если x' после получения будет применен к другому экземпляру SafeArray того же типа?

Т.е. что-то вроде:

main = do
  i<- getUserInput
  let b = SafeArray ...
    let a = SafeArray ... -- The same type as 'b'
      x = a `at` i -- Type error
      x' = case checkIdx a i of
             Nothing -> ...
             Just i' -> b `at` i' -- ???

?

Я понимаю. Просто тут нет никакой магии :(.

http://ideone.com/W03hVR

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

Да, косяк. См. пост выше, в нём нет такой ошибки.

Уй, уж лучше я простым if это сделаю... Не пойми не правильно, идея хорошая, но столько простыни писать ради одной проверки... Лучше бы линтер научили такие проблемы ловить.

Да, косяк.

Вообще-то этот косяк известен еще со времен, когда стало понятно, что есть два типа итераторов над коллекциями: внешние и внутренние. Внешние итераторы хороши известны по итераторам из C++ного STL. Ваш пример с SafeIdx — это всего лишь еще одна вариация на тему внешнего итератора.

А можно все сделать более вменяемо. Через те же контракты, как тут выше писали.

Контракты надо писать, об этом можно забыть. А если линтер натренировать то не забудешь.

Контракты надо писать, об этом можно забыть

Ну, линтер можно натренировать и на это.

По сравнению с boost — детский лепет. А простыня — это вся «библиотека». Её использование довольно просто, см. main.

А простой if забудут.

А как бы ты отлавливал такое в своем языке? Пытался бы до рантайма определить потенциальный выход за границы? Если длина массива и индекс задаются пользователем уже на ходу.

/* здесь обращение к arr[idx] вызывает возмущение компилятора */

if ((idx >= 0) && (idx < n)) {
    /* а здесь все нормально */
    arr[idx] = 0;
    /* или не очень */
    arr[idx-1] = 0;
}

Я бы добавил в систему типов понятие «диапазон допустимых значений». Ну а idx-1 это обычная анонимная переменная, для неё верны все те же рассуждения.

На практике я пока этого делать не буду потому хочу сильно ограничить набор фич для первого релиза (если он вообще будет).

Т.е. проверка при каждом инкременте.

С int и зависимыми типами тоже проверка будет, разница только в том, что без проверки не скомпилируется.

Чтобы без проверки это нужно array<T, size_t> для массивов и fin<size_t> для индексов.

на arr[idx-1] = 0 надо ругаться, из условия не следует, что это будет работать. Отследить это вполне реально. Зависимыми типами. Или контрактами(они потенциально ничем не хуже, но для человека выглядят более понятно).

С int и зависимыми типами тоже проверка будет

Не знаю про зависимые типы, но зачем, например, здесь проверка?

for (int i = 0; i < arr.size(); i++)
  /*  ... */;

Здесь проверка и так есть каждую итерацию. Зависимые версии паттерн-матчинга (dependent pattern matching), if, for и т.п. создают контексты с доказательствами, i >= 0 && i < size в данном случае, operator[] принимает явно int и неявно (implicit & instance arguments) такое доказательство, оно есть в контексте — ок, иначе ошибка компиляции.

Здесь проверка и так есть каждую итерацию

Нет.

void f(int i, int& n);

void g(int size, int& n) {
    for (int i = 0; i < size; ++i)
        f(i, n);
}

смотри -S (cmpl в теле, например). Ну и семантически (что только и важно анализатору) она там, как иначе-то.

http://en.wikipedia.org/wiki/For_loop#Traditional_for-loops

http://stackoverflow.com/questions/1242185/loop-condition-evaluation

^ even a thing! :)

А если ты про первую итерацию, то там i = 0, то есть контекст — i == 0 || i < size откуда i < size (если size >= 0, при i = size = 0 выполнения не происходит). Вообще недостаточно, нужно ещё i >= 0, так что index_t вместо int с вычитанием которое тоже требует неявного доказательства. Плюс ситуацию усложняется мутабельностью i и, следовательно, контекста.

но зачем, например, здесь проверка?

А это, тут нет понятия итератора там или энумерации? Мне кажется, в большинстве случаев когда я вижу такую конструкцию людям просто нужен «питонячий» enumerate(arr). Я вообще стараюсь избегать прямой адресации в массиве если какой-нить enumerate, zip или reduce решают задачу. Ну просто чтобы избежать ошибок с индексами которые до сих пор распространены в ПО.

Нет.

Почему нет? Какой-нить __attribute__(__pure__)? Это cpp?

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

Не, я не об этом. Представим что вот этого куса кода и нет. Вопрос: будет ли ругаться анализатор и на что.

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

Это к вопросу что не получатся ли в итоге зависимые типы («idx зависит от arr»).

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

Просто зависимые типы имеют ряд недостатков:

1. язык типов в общем не обязательно соответствует языку, на котором пишем программу

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

3. сам конструкция искусственна и непонятна

Брать информацию из предусловия или определения типа - разница не принципиальная.

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

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

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

Да нет, никакое это не доказательство. Просто выбран безопасный интерфейс. То же самое можно сделать вообще на динамике.

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

С int и зависимыми типами тоже проверка будет, разница только в том, что без проверки не скомпилируется.

Разница в том, сколько раз будет проверка. С зависимыми типами - один единственный. Без них - на каждое использование.

Ну да, как только зафиксировали доказательствами что терм имеет хитрый подтип (зависимый тип, ограничение предикатом) «обычного» типа, так он во все функции требующие такой подтип может спокойно передаваться без проверок — Σ(x : T, p(x)) < T не сложнее принципиально чем T < Maybe(T) (= Im какой-нибудь f : A -> Maybe T), одна проверка и Σ(x : T, p(x)) или T из Maybe(T) летит во все функции. Больше автоматической дедукции в контекстах и логического подтипирования утверждений — проще фиксировать доказательства. Для мутабельности — система эффектов, операция последовательного control flow разделяет контексты, мутации являются эффектами модифицирующими утверждения между контекстами, эффекты функций описываются так же в сигнатурах.

(зависимый тип, ограничение предикатом) «обычного» типа

Вообще, это refinement type, а не dependent. dependent начинаются тогда, когда в правило вывод добавляется (pred(T1) => pred(T2)) => (T1 <: T2)

По дефолту же T1 = T2 при совпадении и T1 <: T2 только by definition.

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

Нет.

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

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

да

Σ(x : T, p(x)) не зависимый? Это тип термов T для которых выполняется предикат p, Σ-тип, зависимая версия типа произведения — населить можно только парами из значения и пруфа свойства этого значения, тип второго поля кортежа зависит от терма из первого поля (Π-тип тогда — зависимая версия типа степени, тип результата зависит от терма аргумента).

https://scholar.google.com/scholar?cites=5046950720097564665

Σ(x : T, p(x)) не зависимый?

Зависимый. Но это эмуляция - значения этого типа будут парами из элемента и доказательства, в то время как само Х имеет тип T. В случае refinement type у нас конкретно х будут нужного типа, никаких доказательств не надо.

Там было

терм имеет хитрый подтип (зависимый тип, ограничение предикатом) «обычного» типа

если без доказательств, то кто тогда будет доказывать это хитрое свойство?

Σ-тип или изоморфный W-тип могут представлять собой желаемый подтип (подобъект, то есть нужное вложение в исходный T). Стороннее утверждение FOL тоже может дать нужный подтип в модели, но тогда либо особого вида, либо кто-то должен автоматически проводить proof search, а кто-то — содействовать (т.к. оно неразрешимо).

Хотя если без Π/импликации, то, наверное, вполне без доказательств можно.

если без доказательств, то кто тогда будет доказывать это хитрое свойство?

А зачем его доказывать?

Σ-тип или изоморфный W-тип могут представлять собой желаемый подтип (подобъект, то есть нужное вложение в исходный T).

Могут. Просто смысл в том, что все то же самое можно сделать без зависимых типов, на refinements.

но тогда либо особого вида

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

http://en.wikipedia.org/wiki/Rice's_theorem

f : Integer -> {x : Integer | произвольный предикат(x)}
f = произвольная частично-рекурсивная функция

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

Например, http://frama-c.com/ использует http://frama-c.com/download/acsl.pdf для спецификаций, а бакенды — как автоматические пруверы (неразрешимый но практически полезный proof search), так и ручные пруф ассистенты и интерактивные пруверы, http://krakatoa.lri.fr/#provers, http://why3.lri.fr/#provers.

1. в том, что это целостный «метод Eiffel», а язык — это так, DSL транслируемый в сишечку, с поддержкой этого метода проектирования и разработки. Если читал книжки Мейера, то «метод Eiffel» — это метод ОО проектирования и разработки. К нему имеет отношение BON (Business Objects Notation) в поддержку , вместо UML и RUP. Кратко можно охарактеризовать как : seamless переход от кода, к документации (краткой форме класса с интерфейсами) и нотации диаграмм. IDE тоже в поддержку метода.

2. в том, что IDE EiffelStudio умеет AutoTest и прочие ништяки поддержки жизненного цикла разработки. проектирование по контракту — тоже в эту тему. хотя вот недавний Albatross в общем, тоже напоминает контракты из Эйфеля.

3. в том, что оно прозрачно транслируется в Си. то есть: Эйфель-система — это открытая, прозрачно расширяемая система, поддерживающая полный цикл: проектирование, спецификации, проверка корректности, кодирование, документацию и deploy.

сравни с костылями из C++ и статическми анализаторами отдельно, UML моделлерами отдельно, доксигеном отдельно, инсталляторами, системами сборки — отдельно.