Open epogrebnyak opened 4 years ago
Stoch, [05.01.20 19:49]
Выглядит супер, но я бы рекомендовал сделать уклон в типизацию языка
Stoch, [05.01.20 19:50]
На википедии есть лесенка по сложности через систему F и вплоть до до coc
Stoch, [05.01.20 19:52]
Например, лямбда с типами как бы реализуется в системе F, а с зависимыми типами - синтаксис категорной семантики, что дает большую выразительность
Re: @mbakhterev
Не знаю, важно это или нет, но это заблуждение, что lambda-абстракции определяют функции. Во-первых, lambda-абстракция - это просто один из конструкторов lambda-выражений. Во-вторых, от lambda-абстракции до функции путь очень длинный. Обычно терминология такая: выражения определяют процедуры, а некоторые процедуры определяют функции. В-третьих, lambda-выражение, которое в итоге задаёт функцию можно определить без lambda, например, при помощи комбинаторов.
Мне кажется, лучше просто написать: для того, чтобы определит функцию, не обязательно задавать её имя. Для этого можно воспользоваться lambda-абстракцией \x -> x + 1, такие функции будем называть анонимными. И этого достаточно. Lambda-функция - очень странный термин.
Lambda Calculus
A branch of mathematics that uses functions to create a universal model of computation.
http://dev.stephendiehl.com/fun/003_lambda_calculus.html