Реализация функционального языка программирования с линейными типами

Чистые функциональные языки часто рассматриваются как консерватинвые расширения $\lambda$-исчисления и используют его для формализации понятия вычисления. Соответствие Карри-Говарда утверждает, что между термами $\lambda$-исчисления с зависимыми типами и формулами интуционистской логики предикатов есть однозначноее соответсвие, таким образом, меняя логику, можно получать системы типов с различными свойствами. Эта идея привела к появлению множества фунциональных и императивных языков программирования с различными системами типов. Как правило, такие языки используют систему типов для улучшения выразительности и для проверки безопасности программ, и редко используют их для выполнения различных оптимизаций относительно используемой памяти и времени выполнения программ. В общем виде, редукция $\lambda$-термов не зависит от типизации, являясь разновидностью символьным переписыванием. Однако реальные реализации языков программирования не являются абстрактными машинами и подвержены ограничениям реального мира и существующего аппаратного обеспечения. Мы рассматриваем идею использования нетривиальных систем типов не только для улучшения выразительности и безопасности программ, но и для создания лучших оптимизирующих компиляторов. Мы приводим реализацию функционального языка программирования с линейными типами в качестве подтверждения данной идеи. Мы основываем нашу работу на недавних исследования в области теории языков программирования, а также на существующих индустриальных решениях. Мы расширяем существующих язык программирования Quill и приводим его реализацию. Идеи, рассмотренные в данной работе, могут быть применения к другим функциональным языкам с нестрогой моделью вычислений. Недавний расцвет интереса к функциональному программированию, а также популярность таких языков как Rust, показывает, что исследования в данном направлении будут также интересны и в применении к императивным языкам.