kouzdra (kouzdra) wrote,
kouzdra
kouzdra

Category:

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

К 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 дедуктивную систему. И если компилятор не способен сам убедиться что "все хорошо" - есть масса способов ему это "подсказать" (вплоть до явного выписывания прямого доказательства).
Subscribe

  • Post a new comment

    Error

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.
  • 53 comments