Все на теже типовые темы и про "проверку индексов"

kouzdra — 10.06.2016 К http://kouzdra.livejournal.com/3027485.html?view=comments

Норот видимо не понимает о чем идет речь:

Напомню, что в Паскале при обращении к массиву индексы компилятору проверять не надо. Проверка там выполняется (если надо) при преобразовании integer к индексному типу массива l..u

То есть если ты опишешь индексную переменную сразу как l..u - то никаких run-time проверок в простых случаях (типа цикла от l до u) и не надо.

Ну так вот тип 1..10 в этих терминах и есть { i : int | i >= 1 && i <= 10 }

Диапазонный тип как раз и есть частный встроенный ad hoc в язык случай refined types.

Отличие от Паскаля только в том что неявные приведения с run-time проверкой не предполагаются. С другой стороны - средства для доказательства того что тип в действительности такой намного мощнее - включают в себя кроме прочего general purpose дедуктивную систему. И если компилятор не способен сам убедиться что "все хорошо" - есть масса способов ему это "подсказать" (вплоть до явного выписывания прямого доказательства).

Оставить комментарий

Популярные посты:

• Ранее
• Архив