Covalue

В конце статьи авторы обозревают свои достижения: интеграцию с SMT-автоматизированной системой субтипов, реализацию QITs, неявные преобразования между функциями на типах разной степени факторизованности. Кроме того, остался еще ряд примеров, которыми они спешат поделиться: реализация модульной арифметики, факторизованная система полярных координат, лямбда-исчисление со вшитым eta-равенством. В качестве ограничений называются: отсутствие function extensionality, GADTs/QIFs и неинтуитивные сообщения об ошибках. Работу над этими моментами, а также над автоматическим выводом фактор-типов авторы оставляют на будущее.

www.tgoop.com/covalue/82

1.9K viewsFeb 10, 2024 at 09:01

В конце статьи авторы обозревают свои достижения: интеграцию с SMT-автоматизированной системой субтипов, реализацию QITs, неявные преобразования между функциями на типах разной степени факторизованности. Кроме того, остался еще ряд примеров, которыми они спешат поделиться: реализация модульной арифметики, факторизованная система полярных координат, лямбда-исчисление со вшитым eta-равенством. В качестве ограничений называются: отсутствие function extensionality, GADTs/QIFs и неинтуитивные сообщения об ошибках. Работу над этими моментами, а также над автоматическим выводом фактор-типов авторы оставляют на будущее.

BY Covalue