tgoop.com/covalue/82
Create:
Last Update:
Last Update:
В конце статьи авторы обозревают свои достижения: интеграцию с SMT-автоматизированной системой субтипов, реализацию QITs, неявные преобразования между функциями на типах разной степени факторизованности. Кроме того, остался еще ряд примеров, которыми они спешат поделиться: реализация модульной арифметики, факторизованная система полярных координат, лямбда-исчисление со вшитым eta-равенством. В качестве ограничений называются: отсутствие function extensionality, GADTs/QIFs и неинтуитивные сообщения об ошибках. Работу над этими моментами, а также над автоматическим выводом фактор-типов авторы оставляют на будущее.
BY Covalue
Share with your friend now:
tgoop.com/covalue/82