s
Size: a a a
2021 March 29
AT
Карри-Говарда-Ламбека.
С категорными языками программирования всё ещё туго, так что Ламбек пока отдыхает. 😂
s
Лямбда-исчисление уже достаточно категорно. Но если очень хочется, есть https://github.com/jameshaydon/lawvere
s
В принципе, это по большей части переизобретение tacit programming.
AG
кто-то срочно должен вбросить про изоморфизм Карри Ховарда
карри-говард для логических языков тоже работает, только там вычисление это не cut elimination, а proof search
ВМ
я в силу своего дилетантства пытался через него увязать логические и функциональные языки как раз, но судя по всему как всегда вбросил нечто что сам не до конца понял ещё)
AG
Карри-Говарда-Ламбека.
карри-говарда-ламбека-скотта-тарского-стоуна-хинтикки
AG
я в силу своего дилетантства пытался через него увязать логические и функциональные языки как раз, но судя по всему как всегда вбросил нечто что сам не до конца понял ещё)
s
О, спасибо. А есть что-нибудь про логическое программирование со стороны теорката?
AG
О, спасибо. А есть что-нибудь про логическое программирование со стороны теорката?
卜
В Prolog нет типов. И системы модулей тоже нет.
В Mercury сделали типизацию Пролога
AT
卜根
В Mercury сделали типизацию Пролога
Только не Пролога, а Mercury. 😊
AT
Ещё Cur смутно припоминается...
s
λProlog, Makam...
AG
макам это одна из реализаций лямбда-пролога
AG
еще есть teyjus, elpi и abella
AT
Чё-то опять PLD чат сюда протёк... 😂
s
макам это одна из реализаций лямбда-пролога
Синтаксис другой по крайней мере.
РС
книжка афигенная, кстати, спасибо.
единственное не совсем понял как описание грамматики они хранят
единственное не совсем понял как описание грамматики они хранят
Так что, есть идеи?:)