Современный ЯП с системой типов как в Ada

Scala: https://github.com/fthomas/refined

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

А в каком языке при считывании числа с stdin пользователь не может подсунуть туда строку из букв? Всё, ты обречён что угодно считать строкой и только, никаких тебе чисел, ни в каком языке программирования.

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

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

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

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

емнип это называется контрактное программирование.

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

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

Нельзя, мне лень.

Значит не было.

Могу описать словами

Ничего не понял. Либо я тупой, либо вы звиздите. Но компайл-тайм проверок не видно в упор.

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

Чушь какая, это в любом языке со строгими типами так. Из stdin приходит int, чтобы положить его в свой тип нужно кастануть, иначе type mismatch. Само-то кастование происходит в рантайме, т.о. никакой поддержки языка не требуется (тупо пишем функцию которая всё проверяет).

А как там в аде, арифметика на диапазонах есть? Можно сложить два значения Month_type?

Но компайл-тайм проверок не видно в упор.

В компайлтайме будет проверка на наличие валидации. Если валидации нет - будет ошибка о неперехваченном исключении.

смысл в том, что

x = read()
if (valid(x)) {
    f(x); // f работает корректно когда предикат на х истинный
} else {
    *process error*
}

x = read()
try {
    f(new Validated(x)) // f работает с типом Validated, конструктор которого внутри проверяет valid(x) и кидает NoValid при невалидном х
} catch (NoValid e) {
    *process error*
}

В компайлтайме будет проверка на наличие валидации.

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

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

Всмысле нет? Есть. Проверка в компайлтайме гарантирует, что в f не попадет невалидный х.

Всмысле нет?

В прямом смысле. В Ada, в Pascal и, емнип, в Modula-2, если пользователь определял подтип, скажем Day=1..31, а затем пробовал присвоить переменной типа Day значение 0 или 32, то компилятор делал проверки прямо в компайл-тайм. И отказывался компилировать такой код.

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

Вы (ну или другой анонимный эксперт) утверждали, что проверки в compile-time можно делать и в Java. Показать, естественно, не смогли.

Вы (ну или другой анонимный эксперт) утверждали, что проверки в compile-time можно делать и в Java. Показать, естественно, не смогли.

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

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

Сударь, вы вообще-то читать умеете? Или вам важно доказать, что верблюд здесь не вы?

Повторите на Java вот этот пример, может быть тогда поймете о идет речь.

Повторите на Java вот этот пример, может быть тогда поймете о идет речь.

Validated0To1 a;
a = 2; //ошибка
a = new Validated(2) //ошибка

на уровне компиляции гарантируется, что в а никогда не попадет ничего кроме 0 и 1. Не скомпилируется такой код.

a = new Validated(2) //ошибка

Ошибка во время трансляци?

VHDL :-)

ну таки да, он на аде и основан

Validated0To1 a;
a = 2; //ошибка

Присвоить объекту ссылочного типа целочисленную константу — это сильно, да.

Речь идет вот о чем: https://ideone.com/LtCpZ8 Здесь ошибка выдается в ран-тайм. Без каких-либо предупреждений в компайл-тайм.

Тогда как в Ada/Pascal/Modula-2 компилятор для b выдал бы предупреждение или даже ошибку.

Речь идет вот о чем: https://ideone.com/LtCpZ8 Здесь ошибка выдается в ран-тайм.

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

catch(Exception e)

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

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

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

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

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

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

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

https://ideone.com/OaZDdz

Ошибка именно что вылетает и ловиться в ран-тайме.

Вообще говоря, там нету ошибки (просто try-блок написан криво). В b не прилетело никакой некорректной переменной, компилятор статически это гарантировал. И написать код такой, чтобы в b такая переменная прилетела - не получится (естественно если перехватфывать нормально а не на Exception да еще и throws в main)

Это что, конкурс альтернативно-одарённых?

Нет, лучше уж в клуб переехать - там хоть понятно, что это 6-я палата...

Компилятор в данном случае статически гарантирует, что в переменную не попадет значение, выходящее за диапазон. Какие еще гарантии и проверки тебе нужны?

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

https://ideone.com/OaZDdz

Сударь, а вас не смущает то, что даже корректную с прикладной точки зрения строку не удается скомпилировать:

Main.java:28: error: unreported exception IntFrom0to1.InvalidValueException; must be caught or declared to be thrown
			IntFrom0to1 a = new IntFrom0to1(0);

Ась?

В b не прилетело никакой некорректной переменной, компилятор статически это гарантировал.

Компилятор гарантировал не это. Компилятор гарантировал то, что исключение будет либо обработано, либо продекларировано в секции throws. Не больше, не меньше.

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

Но! Что самое важное, все проверки передаваемых в IntFrom0to1 значений будут осуществляться _только_ в ран-тайм. Только в ран-тайм!

А ведь вы обещали сделать такие проверки в Java в компайл-там.

Очевидно, что вы просто не знаете, что такое проверки в компайл-там, отсюда и попытка завязаться на checked exceptions. Но это не то, что вас просили показать.

Сударь, а вас не смущает то, что даже корректную с прикладной точки зрения строку не удается скомпилировать:

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

Компилятор гарантировал не это. Компилятор гарантировал то, что исключение будет либо обработано, либо продекларировано в секции throws. Не больше, не меньше.

Именно. Что нам и требовалось.

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

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

Но! Что самое важное, все проверки передаваемых в IntFrom0to1 значений будут осуществляться _только_ в ран-тайм. Только в ран-тайм!

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

x = read()
f(x)

x = read()
if (valid(x)) {
    f(x)
} else {
    ....
}

Какие еще нужны статические проверки и гарантии нужны?

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

Нет, не смущает.

Занавес. Расходимся.

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

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

https://ideone.com/4HqluM

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

В рассматриваем примере проверки происходят _во время компиляции_. Как минимум потому, что никаких проверок в рантайме вообще быть не может, если программа не запущена. Какие еще нужны проверки во время компиляции, которых там нету? Можно конкретно? Что именно должен проверить компилятор в дополнение к тому, что он проверяет в указанной реализации (корректность кода)?

Но там нет ошибки. В b некорректного значения не прилетело, проверка во время компиляции это гарантировала.

В рассматриваем примере проверки происходят _во время компиляции_.

В рассматриваемом примере во время компиляции происходят проверки секции throws.

Конкретные значения _всегда_ проверяются в ран-тайме.

В Ada/Pascal/Modula-2 проверка значений возможна не только в ран-тайме (если вовремя компиляции не известно, например, читается во время работы откуда-нибудь), но и в компайл-тайме, если значение известно во время компиляции. Например, если значение задается прямо константой в коде. Пример такого был показан в самом начале темы, ссылку на пример вам уже давали, но несложно и повторить, вот — читать до просветления.

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

Но там нет ошибки. В b некорректного значения не прилетело, проверка во время компиляции это гарантировала.

Посмотрите еще раз, внимательный вы наш. Компилятор может проверить только секции throws, но не может проконтролировать правильность выбрасывания исключений. Программист ошибся с написанием проверки и в IntFrom0to1 можно подсунуть некорректное значение, и компилятор здесь бессилен.