kouzdra (kouzdra) wrote,
kouzdra
kouzdra

Category:

Еще про типы - пример из комментов:

http://kouzdra.livejournal.com/3028355.html?thread=101372035#t101372035
- Не всё может быть проверено в compile-time, боюсь. То есть в коде, который может быть представлен в виде конечного автомата и который вполне верифицируется, оно таки да. Но не в общем случае - а ну как генетический или иммунный или нейроалгоритм с рандомизатором? Правда я человек темный, может быть уже есть крутой math и на такой случай.

В Аде в compile-time может быть проверен выход за пределы диапазона, но только если значение выводимо именно на момент компиляции, а это мягко говоря не всегда так.

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

Во-вторых - один из самых простых методов такого объяснения - это именно явная проверка:
module My2

type byte = i:nat{0 <= i && i < 255 }

let read_int = FStar.IO.input_int

val read_byte : unit -> byte
let read_byte () = read_int ()

При компиляции ругается:
/my2.fst(8,19-8,30): Subtyping check failed; expected type byte; got type int

А если переписать:
exception InvalidByte
val read_byte : unit -> byte
let read_byte () = 
    let i = read_int () in
    if 0 <= i && i < 256 
    then i
    else raise InvalidByte


То все ок - точнее в том коде который тут наверху - тоже ругается - потому что там ошибка - верхняя граница байта неверно указана - но если поправить 255 на 256 как и надо - все ОК.

Но проверку самому надо написать - компилятор за тебя ее не сделает

PS: И дело не в том, что константы (и даже не в том, что арифметика - там в принципе можно и с любыми в принципе типами такие вещи писать):
exception InvalidRange
val read_range : l:int -> u:int -> i:int{l <= i && i <= u}
let read_range l u = 
    let i = read_int () in
    if l <= i && i <= u 
    then i
    else raise InvalidRange

val a : byte
let a = read_range 0 255

Тоже работает - и вовсе не потому что компилятор "инлайнит" - а именно потому что из типа read_range вытекает что его применение к 0 255 даст именно byte.

То есть с раздельной компиляцией это все точно так же работает

Ситуации, когда интеллекта компилятора действительно не хватит естественно тоже есть - но и там обычно можно компилятору "подсказать" "почему это правда" (то есть дать доказательство/схему доказательства, до которых он сам допереть не может)
Tags: компутерщина
Subscribe

  • Нафиг - нафиг...

    Мое отношение к "медицине" определяется тем, что она силком вытягивает из меня уже лет 35 довольно приличные деньги на свои "услуги". При этом на…

  • My comment to an entry 'Снова все о том же: вакцинация от Ковида' by mary_spiri

    Я полагаю все эти меры никак не оправдываемыми их результатом. Я сам не очень молодой — 55 — и подогаю риск смерти от вируса незначимым по сравнению…

  • Это жжж неспроста

    Йебанутые собачники - это все-таки диагноз: Водокачкин был заметен ебанутым собачничеством и любовью к "ножичкам". Тут вдруг разразился тоже…

  • 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.
  • 17 comments

  • Нафиг - нафиг...

    Мое отношение к "медицине" определяется тем, что она силком вытягивает из меня уже лет 35 довольно приличные деньги на свои "услуги". При этом на…

  • My comment to an entry 'Снова все о том же: вакцинация от Ковида' by mary_spiri

    Я полагаю все эти меры никак не оправдываемыми их результатом. Я сам не очень молодой — 55 — и подогаю риск смерти от вируса незначимым по сравнению…

  • Это жжж неспроста

    Йебанутые собачники - это все-таки диагноз: Водокачкин был заметен ебанутым собачничеством и любовью к "ножичкам". Тут вдруг разразился тоже…