Например, если компьютер 10111100хранится в одном конкретном байте ОЗУ, как компьютер узнает, что он интерпретирует этот байт как целое число, символ ASCII или что-то еще? Данные типа хранятся в соседнем байте? (Я не думаю, что это будет так, поскольку это приведет к использованию вдвое больше...
Я начинаю личное библиографическое исследование по алгоритмам проверки типов и хочу несколько советов. Какие алгоритмы, стратегии и общие методы проверки типов наиболее часто используются? Меня особенно интересуют сложные алгоритмы проверки типов, которые были реализованы в широко известных строго...
Я работаю над компилятором для конкатенативного языка и хотел бы добавить поддержку вывода типов. Я понимаю Хиндли-Милнера, но я изучаю теорию типов по ходу дела, поэтому не знаю, как ее адаптировать. Является ли следующая система надежной и достоверной? Термин - это литерал, композиция терминов,...
Предположим, я хочу построить операционную систему на основе очень маленького собственного нижнего ядра, которое действует как интерпретатор / среда выполнения управляемого кода, и большего верхнего ядра, скомпилированного с неродным машинным языком (байт-код Java, CIL и т. Д.). Примерами подобных...
Мне нравится все, что происходит во время компиляции, и мне нравится идея, что, как только вы скомпилируете программу, вы получите много гарантий относительно ее выполнения. Вообще говоря, статическая система типов (Haskell, C ++, ...), похоже, дает более сильные гарантии во время компиляции, чем...
Если функция имеет тип возврата of ( нижний тип ), это означает, что она никогда не вернется. Это может, например, выйти или бросить, обе довольно обычные ситуации. Предположительно, если функция имеет параметр типа ⊥, она никогда не сможет (безопасно) быть вызвана. Есть ли когда-нибудь причины для...
Мне стало известно, что стоимость вывода типа в функциональном языке, таком как OCaml, может быть очень высокой. Утверждение состоит в том, что существует последовательность выражений, такая, что для каждого выражения длина соответствующего типа экспоненциально зависит от длины выражения. Я...
Так что в настоящее время я иду через книгу HoTT с некоторыми людьми. Я утверждал, что большинство индуктивных типов, которые мы увидим, можно свести к типам, содержащим только зависимые типы функций и вселенные, взяв тип рекурсора как вдохновение для эквивалентного типа. Я начал обрисовывать, как...
В « Концепциях языков программирования» Джон Митчелл пишет, что статическая проверка типов обязательно является консервативной (чрезмерно строгой) из-за проблемы остановки. Он приводит в качестве примера: if (complicated-expression-that-could-run-forever) then (expression-with-type-error) else...
Coq включает в себя выражения let на своем основном языке. Мы можем переводить выражения let в приложения, подобные этому: let x : t = v in b ~> (\(x:t). b) v я понимаю, что это не всегда работает, потому что значение vне будет доступно при проверке типов b. Однако это можно легко исправить с...