G
Т-34 85
что имеется в виду? Концепты, что-ли?
Size: a a a
2020 March 15
Т8
слишком геморрно их использовать, в большинстве случаев это оверкилл
p
Т-34 85
слишком геморрно их использовать, в большинстве случаев это оверкилл
Почему?
p
Это проверяется на этапе компиляции, а не в рантайме, если что
АВ
Типы с уточнением ("refinement types") от такого спасают.
На F*:
На F*:
val subtract_proof: a: Int -> b: Int -> c: Int -> Lemma (ensures(с = a - b))(Синтаксис я немного забыл, но не суть)
let subtract_proof a b = admit()
Тут написано c = a - b. Что если я ошибся и написал c = a + b? Или это надо дублировать в самой функции? Если дублировать, то тоже какой в этом смысл? Будет практически вынужденная копипаста.
В любом случае, компилятор сами имена не понимает без ИИ, и если subtract везде реализован через +, он не сможет сказать что что- то не так, если нет избыточности, благодаря которой можно увидеть противоречие.
В любом случае, компилятор сами имена не понимает без ИИ, и если subtract везде реализован через +, он не сможет сказать что что- то не так, если нет избыточности, благодаря которой можно увидеть противоречие.
G
Тут написано c = a - b. Что если я ошибся и написал c = a + b? Или это надо дублировать в самой функции? Если дублировать, то тоже какой в этом смысл? Будет практически вынужденная копипаста.
В любом случае, компилятор сами имена не понимает без ИИ, и если subtract везде реализован через +, он не сможет сказать что что- то не так, если нет избыточности, благодаря которой можно увидеть противоречие.
В любом случае, компилятор сами имена не понимает без ИИ, и если subtract везде реализован через +, он не сможет сказать что что- то не так, если нет избыточности, благодаря которой можно увидеть противоречие.
Модель программы описывается в системе типов. Если программа тайп-чекается, значит она работает так, как подразумевалось. Да, ошибку в системе типов (модели программы) тоже можно допустить (иначе говоря - неправильно из головы перенести модель в типы).
Т8
Это проверяется на этапе компиляции, а не в рантайме, если что
на этапе компиляции проверяются не сами значения, а возможность переменных иметь значения в рантайме. Подозреваю, что охренеешь это описывать, проще делать рантайм-проверки и тесты. Ну, и реализовать такой компилятор - нетривиальная задача
IJ
Тут написано c = a - b. Что если я ошибся и написал c = a + b? Или это надо дублировать в самой функции? Если дублировать, то тоже какой в этом смысл? Будет практически вынужденная копипаста.
В любом случае, компилятор сами имена не понимает без ИИ, и если subtract везде реализован через +, он не сможет сказать что что- то не так, если нет избыточности, благодаря которой можно увидеть противоречие.
В любом случае, компилятор сами имена не понимает без ИИ, и если subtract везде реализован через +, он не сможет сказать что что- то не так, если нет избыточности, благодаря которой можно увидеть противоречие.
Одно -- спецификация программы, другое-- программа.
p
Тут написано c = a - b. Что если я ошибся и написал c = a + b? Или это надо дублировать в самой функции? Если дублировать, то тоже какой в этом смысл? Будет практически вынужденная копипаста.
В любом случае, компилятор сами имена не понимает без ИИ, и если subtract везде реализован через +, он не сможет сказать что что- то не так, если нет избыточности, благодаря которой можно увидеть противоречие.
В любом случае, компилятор сами имена не понимает без ИИ, и если subtract везде реализован через +, он не сможет сказать что что- то не так, если нет избыточности, благодаря которой можно увидеть противоречие.
Пишешь
fn substract(a: int, b: int) -> c: int{c < a && c < b} { a + b }
И компилятор это не пропустит
fn substract(a: int, b: int) -> c: int{c < a && c < b} { a + b }
И компилятор это не пропустит
АВ
Пишешь
fn substract(a: int, b: int) -> c: int{c < a && c < b} { a + b }
И компилятор это не пропустит
fn substract(a: int, b: int) -> c: int{c < a && c < b} { a + b }
И компилятор это не пропустит
Даже если я напишу не a+b, а a-b, компилятор не пропустит, потому что при a = 0 или b = 0 условие не выполнится.
p
fn substract(a: int, b: int) -> c: int{c <= a && c < b && b >= 0 || c > a } { a - b }
К
Интереса ради. Существуют ли такие генераторы парсеров, которые бы на выходе давали код, схожий с рукописным без внешних зависимостей?
СЛ
Интереса ради. Существуют ли такие генераторы парсеров, которые бы на выходе давали код, схожий с рукописным без внешних зависимостей?
После этого можно будет смело идти за премией Абеля.
К
Почему? Есть какое-то принципильное препятствие в генерации, к примеру, парсера по методу рекурсивного спуска?
СЛ
Почему? Есть какое-то принципильное препятствие в генерации, к примеру, парсера по методу рекурсивного спуска?
Потому что это NP. Или вам нужен генератор парсеров, на которых только хеллоуворлд можно реализовать?
К
Конкретно сейчас мне ничего не нужно. Я выясняю, существует ли такое и если нет, то почему. Почему эта задача NP-полная? Почему человек решает эту NP-полную задачу? Или человек решает её в обход?
К
Или Вы под "hello world" подразумеваете грамматики, для которых воплотим разбор рекурсивным спуском?
AT
Интереса ради. Существуют ли такие генераторы парсеров, которые бы на выходе давали код, схожий с рукописным без внешних зависимостей?
Насчёт внешних зависимостей вообще не понятно - я не припоминаю генератора парсеров, который бы использовал внешние зависимости.
Насчёт человекочитаемости - сделать-то более-менее можно, просто у генераторов парсеров в приоритете скорость разбора и потребление памяти, а это противоречит человекочитаемости. Ну и вообще, не очень понятно зачем кому-то сильно вчитываться в сгенерированный код?..
Насчёт человекочитаемости - сделать-то более-менее можно, просто у генераторов парсеров в приоритете скорость разбора и потребление памяти, а это противоречит человекочитаемости. Ну и вообще, не очень понятно зачем кому-то сильно вчитываться в сгенерированный код?..
К
Во внешнюю зависимость я включаю и библиотеку поддержки(существенную по размерам), которая может идти в комплекте с генератором и которой не будет при ручном создании
К
Ну мой опыт написания рукописных парсеров, говорит о том, что рекурсивный спуск работает быстро и точно быстрей, чем делается многими распространёнными генераторами парсеров