> Было бы интересно узнать, чем бы тебе мог быть практически полезен Паша если бы у вас всё получилось.
вот это хороший вопрос. Задача Паши была сделать кодировку Черча (неприменимую в продакшине из-за неэффективности) для зависимой теории с построениями теормов индукции. Это невыполнимая задача, потому что в нашем ядре нет вообще ничего кроме чистой лямбды. Поэтому мы обогатили кодировку типов всеми необходимыми нам свойствами и скомпилировали терм индукции, который вычисляется как лимит тождественного функтора в категории алгберы заданного индуктивного типа. Другими словами построено равенство, модель теории категорий и на ней написали взятие лимитов, как микропрограмма для прошивки в чистой лямбде. Вот для этого и был нужен Паша.
![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png)
timeasmymeasure
no subject
Date: 2016-09-04 03:14 am (UTC)вот это хороший вопрос. Задача Паши была сделать кодировку Черча (неприменимую в продакшине из-за неэффективности) для зависимой теории с построениями теормов индукции. Это невыполнимая задача, потому что в нашем ядре нет вообще ничего кроме чистой лямбды. Поэтому мы обогатили кодировку типов всеми необходимыми нам свойствами и скомпилировали терм индукции, который вычисляется как лимит тождественного функтора в категории алгберы заданного индуктивного типа. Другими словами построено равенство, модель теории категорий и на ней написали взятие лимитов, как микропрограмма для прошивки в чистой лямбде. Вот для этого и был нужен Паша.