SA
в математике ничего не натянуто
Size: a a a
2020 December 21
SA
ты вообще в курсе сам о чем говоришь
SA
нетипизированное лямбда исчисление
грубо говоря сильнее чем та же теория множеств
и порождает ебань а не ту математику с которой можно иметь дело
там возможно циклические цепи если переводить на язык множеств и всякая хуйня
грубо говоря сильнее чем та же теория множеств
и порождает ебань а не ту математику с которой можно иметь дело
там возможно циклические цепи если переводить на язык множеств и всякая хуйня
VM
Натянута в том плане, что сначала появилось лямбда-исчисление, а потом его расширили до лямбда-исчисления с типами.
SA
так вот для того чтоб сделать что то эквивалентное
SA
они придумали типизированное лямбда исчисление
SA
так что не расширили а сузили
DP
это чатик по функциональному программированию и теории категорий? )
SA
название прочитай
SA
я слышал что если кто то что то знает то это вроде не плохо а наоборот
SA
вчера так было
SA
че то поменялось?
DP
название чего, телеграм группы? там про лисп. лиспы динамически типизированы, в лиспах есть опциональная типизация, некоторые лиспы умеют фп. что не так?
SA
все так
SA
а я еще знаю вот ту хуйню которую ты назвал
SA
и поэтому могу ее упоминать
SA
что касается контрактов то короче типы в том виде что они есть в с++ да не очень
SA
зависимые типы выглядят куда разумнее чем эти самые контракты которые че то вроде того но хуево и не до конца
DP
так пожалуйста, откуда такая агрессия?
DP
зависимые типы наверняка подразумевают что весь код соприкасающийся с ними должен быть типизирован, хотя бы в рамках одного модуля? просто контракты этого не подразумевают вообще