Я разрабатываю интерпретатор функционального языка программирования, который использует систему типов Хиндли-Милнера.
Вопрос в том, где должны возникать (обнаруживаться) ошибки типов?
Например, если я применяю значение типа Integer к функции типа Bool -> Integer, это, очевидно, ошибка типа. Всегда ли это может обнаружить вывод типа?
Я предполагаю, что средство вывода типа не всегда полностью знает типы выражений, т.е. в процессе вывода. Следовательно, некоторые ошибки, обнаруженные средством вывода типа, будут ошибочными, а некоторые ошибки не будут обнаружены.
Однако оценщик выражений должен правильно обнаруживать ошибки типов, потому что оценщик полностью знает типы выражений.
Если механизм вывода типов не может правильно обнаруживать ошибки типов, то как статически типизированные интерпретируемые языки, такие как OCaml, обрабатывают проверку ошибок статического типа?
