Andy Melnikov (nponeccop) wrote,
Andy Melnikov
nponeccop

Влажные мечты о категорной имплементации математики

У меня давно была мечта - чтобы было такое компактное здание математики, где определения и теоремы даются в одну строчку из более общих. Не важно в каком виде (формального текста, естественного текста, интерактивной тулзы).

Условно, что монада - это моноид в категории эндофункторов, такой птичий язык, сепульки-сепулькарии-сепуление, но без циклов.

Сегодня столкнулся с проблемой, что в Coq нет доки по структурной коиндукции и коиндуктивным типам.

Нет чтобы просто сказать, что СЕПУЛЬКАРИИ — устройства для сепуления структурная корекурсия встроена в ядро, продуктивность фикспоинтов коалгебр постулируется, а ключевое слово CoFixpoint просто говорит коку, что дальше у нас Мю Ню и коалгебра.

Вместо этого у них целый туториал как официальная дока, где рассусоливают на 5 страницах что-то про guardedness. Тьфу на них.
Tags: fp, programming, все пидарасы а я
Subscribe

  • Post a new comment

    Error

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.
  • 4 comments