Алексей Махоткин

домашняя страница

Критика Standard ML — проверка типов при компиляции

Andrew W. Appel, «Критика Standard ML», оглавление

Программисты делают ошибки. Даже если они доказали, что алгоритм корректен в том или ином формальном или неформальном смысле, все равно слишком сложно избежать ошибок при его трансляции в конкретную формальную нотацию языка программирования. Так как я особенно неловок в плане программирования, то, возможно, я допускаю больше ошибок, чем средний программист.

Итак, мне нужно найти все ошибки и исправить их. Любая помощь, которую мне сможет при этом оказать среда разработки принимается с благодарностью. На практике я обнаружил, что львиная доля моих ошибок обнаруживается на стадии компиляции при проверке типов ML. Эти ошибки довольно просто исправить, потому что:

  • компиляция занимает меньше времени, чем компиляция и запуск;
  • во время одиночной компиляции можно найти несколько ошибок компиляции; найти несколько ошибок при одиночном запуске (или даже при одной компиляции и нескольких запусках) гораздо сложнее;
  • ошибки компиляции можно обнаружить независимо от входных данных; ошибки времени выполнения могут не быть обнаружены, пока программа не обработает много наборов входных данных;
  • ошибки компиляции часто сопровождаются полезными разъяснениями; ошибки времени выполнения гораздо сложнее диагностировать.

Наконец, типизация при компиляции (особенно элегантная система типов ML) помогает мне упорядочить понимание собственной программы, так что, может быть, я вообще сделаю меньше ошибок.

Интересно заметить, что большинство языков из «математической» семьи имеют систему типов стадии выполнения (в Lisp, Scheme, Smalltalk, APL, и т. д.), тогда как языки типа Algol имеют проверку типов на стадии компиляции. Возможно, это потому, что в «математических» языках есть сборка мусора; сборщики мусора требуют во время выполнения информацию о типах, чтобы отслеживать доступные объекты; так как во время выполнения доступны данные о типах, есть большой соблазн использовать её; или же, может быть, никто не знал, как сделать хорошую «математическую» проверку типов, пока не была изобретена система типов ML. Конечно, проверка типов на стадии выполнения замедляет выполнение программы, но «математические» языки никогда не ставили себе основной целью «сырую» производительность. В ML отсутствие проверки типов во время выполнения обеспечивает более эффективные реализации: подробнее это будет обсуждаться ниже.

Comments