Дельфи. А что толку о такой проверки, Day_type[32] или как у тебя там, ругается, а Day_type[i+32] нет.

В каких ЯП ещё так можно (задавать/проверять диапазон значений не в runtime, а при компиляции)?

В Ada диапазон проверяется в рантайме.

range 1 .. 31;

проверять диапазон значений не в runtime, а при компиляции

как именно компилятор проверит что в stdin пришло 32?

Haskell?

http://learnyouahaskell.com/making-our-own-types-and-typeclasses

data Day = Monday | Tuesday | Wednesday | Thursday | Friday | Saturday | Sunday   
           deriving (Eq, Ord, Show, Read, Bounded, Enum)  

Что именно ты пытался доказать этим фрагментом?

В каких ЯП ещё так можно (задавать/проверять диапазон значений не в runtime, а при компиляции)?

В Java.

Это дешевый фокус, так вот компиляй,

procedure m is
  type t is range 0..1;
  a : t;
  i : integer;
begin
i := 0;  
a := i+2;
end m;

наивный чукотский юноша

m.adb:9:10: expected type "t" defined at line 3
m.adb:9:10: found type "Standard.Integer"

тем, что ты очередной раз пернул в лужу

Ты идею понял или тупишь?

как именно компилятор проверит что в stdin пришло 32?

Фи, stdin для плебеев.

кто из нас тупит?

procedure m is

  type t is range 0..1;

  a : t;

begin
  a := 1;
  a := a + 1;
end m;

> gnatmake m.adb 
gcc-4.6 -c m.adb
m.adb:9:10: warning: value not in range of type "t" defined at line 3
m.adb:9:10: warning: "Constraint_Error" will be raised at run time
gnatbind -x m.ali
gnatlink m.ali

perl6

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

anonymous, вы там рассчитайтесь на первый-второй..., нафига ты мне другой текст подсунул?

твоя «идея» 1 - не компилится; 2 - является заблуждением.

Что именно ты пытался доказать этим фрагментом?

тем, что ты очередной раз пернул в лужу

Тогда у тебя снова не получилось: «For a signed integer type, the exception Constraint_Error is raised by the execution of an operation that cannot deliver the correct result because it is outside the base range of the type». Надеюсь, не нужно объяснять, что исключение возбуждается в рантайме.

что исключение возбуждается в рантайме.

надеюсь не нужно объяснять, что компилер в компайлтайме проверил? или ты настолько туп, что ясные и понятные сообщения компилера для тебя египетские иероглифы?

А чем Ada не современный ЯП? Он не намного старше новоделов, а если брать реализацию gnat и последний стандарт то можно сказать ровесник. Ладно бы про С говорил, но Ada вполне современный язык и по фичам и по реализации.

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

надеюсь не нужно объяснять, что компилер в компайлтайме проверил?

Надеюсь, не надо объяснять, что проверка в компайл-тайме в общем случае не исключает необходимости проверки в рантайме?

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

Я настолько умен, что насквозь вижу твои детские попытки выдать частные случаи за общий.

Ну жабка, лучше ничего из кросплатформенного нету.

В Java уже можно сделать тип-диапазон с проверкой попадания значений в этот диапазон в компайл-тайм?

можно попробовать упороться атд, но зачем..?

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

Смотри refinement types, dependent types

А зачем вообще переносят какие-то проверки в compile-time?

Ну и да, хотелось бы посмотреть, как эти АТД будут выглядеть в Java. С проверками в compile-time.

А зачем вообще переносят какие-то проверки в compile-time?

ну типы --- это полезно.

а проверка на диапазон --- хз.

Ничего интересного кроме предупреждения, что в рантайме жопа может приключиться компилятор и не напишет

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

ATS

val xs = $list{int}(0, 1, 2)
val x0 = xs[0]
val h = 2;
val x3 = xs[h+10] 

Проверка компилятором конечно лучше чем ничего, но значений в явном виде в программе раз два и обчелся , все равно у тебя в исходнике присутствует что-то типа константы dwMonday , что уже в диапазоне, а не 1. А вот значением со стороны ввода с интерфейса или из сети будет число и ты обязан будешь обмануть компилятор приведением типа. Можно еще оператор = переопределить, чтобы совсем всех запутать, но задача по проверке остается, как бы ты её не зарывал и не маскировал фичами языка. Ну закроешь ты своей усиленной типизацией какой-то класс ошибок, не самых сложных, породишь кучу новых.

Любой маргинальный язык с dependent types.

Для C это можно сделать с помощью frama-c.

В каких ЯП ещё так можно (задавать/проверять диапазон значений не в runtime, а при компиляции)?

Т.е. значения ты будешь знать заранее?
Тогда везде, где есть препроцессор.

Для C это можно сделать с помощью frama-c.

ого, а как? я думал это не более чем статический анализатор

Proof assistant

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

Современный

Ada 2012 жы есть. Для нее 5 лет ваще не срок :)

Например: https://frama-c.com/jessie_tutorial_index.html#htoc11

Я настолько умен, что насквозь вижу твои детские попытки выдать частные случаи за общий.

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

Я настолько умен, что насквозь вижу твои детские попытки выдать частные случаи за общий.

Ну у него случай общий

Нет.

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

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

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

И компилятор выдаст ошибку если ты не проверишь это число на вхождение в диапазон.

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

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

В Java уже можно сделать тип-диапазон с проверкой попадания значений в этот диапазон в компайл-тайм?

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

Из дача

их задача

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

Допустим. И что? С точки зрения Ады код корректен. То, что во время исполнения он может возбудить Constraint_Error, соответствует RM.

$ cat m.adb

procedure m(i:integer) is
  type t is range 0..10;
  v: t;
begin
  v := t(i) + 1;
end m;
$ gnatmake m.adb && echo OK
OK
$ 

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

Java на разу не C-подобная, она Pascal-подобная.

Eiffel

Конкретно в джаве можно на чекед эксцепшенах.

Примерный код можно?

Когда речь заходит об Ada, то сразу вспоминается VHDL.

В каких ЯП ещё так можно

Паскаль же, причём сто лет как.

FPC тоже вполне себе кроссплатформенный.