Andy Melnikov (nponeccop) wrote,
Andy Melnikov
nponeccop

Category:

Как мы аксиому индукции лепили

Если кто не знает, zeit_raffer, maxim и я лепим язык с зависимыми типами. В результате лента http://fprog.ru/planet/ в значительной степени состоит из нас. Где все остальные ФП-шники сидят?

Макс хочет переписать свою эрланговскую N2O-инфраструктуру на типизированный язык. Я хочу высокоуровневый фронтэнд к HNC. Оба хотим минимальную hackable кодобазу.

За основу взяли http://hackage.haskell.org/package/morte, который привлёк минимальностью - в частности, отсутствием индуктивных типов и равенства в core calculus.

Но оказалось, что в морте нет не только встроенных индуктивных типов, но и индукции как таковой. Из-за чего язык бесполезен, как язык с зависимыми типами. Например, нельзя даже доказать коммутативность булевского "или".

Более того, есть даже запретительный пейпер, который говорит, что индукции в λP не может быть никогда, при какой угодно кодировке индуктивных типов. Но у нас система отлична от λP, и zeit_raffer cомневается, что можно формализовать понятие "любой кодировки".

В-общем, он придумал альтернативный способ представить индукцию в нашей системе (расширении неиндуктивного Calculus of Constructions непредикативной цепочкой вселенных), формализовав кусок теории категорий, но термы получаются громоздкими, и чтобы сократить ручную работу, ща maxim пилит макросы.

Если в результате удастся запилить хотя бы Primitive Recursive Arithmetics, это будет прорыв и публикация. Вроде как всё на мази и есть наброски в Lean (хотя непонятно как - лин предикативный). Надеюсь, последние оставшиеся кирпичики не разрушат всё здание, как бывает в математике.
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.
  • 1 comment