(Я уверен, что на этом сайте уже был дан ответ, но поиск наводнен концепцией вызова free() для переменной в C.)
Я натолкнулся на термин "eta reduction", который был определен как f x = M x ==> M, если x "не является свободным в M". Я имею в виду, я думаю, что я понимаю суть того, что он пытается сказать, похоже, что вы делаете, когда вы конвертируете функцию в бесшумный стиль, но я не знаю, что означает квалификатор о том, что x не является бесплатным.
Вот пример:
\f -> f x
В этой лямбде x - свободная переменная. В принципе, свободная переменная - это переменная, используемая в лямбда, которая не является одним из аргументов лямбда (или переменной let). Это происходит вне контекста лямбда.
Это означает, что мы можем изменить:
(\x -> g x) to (g)
Но только если x не является свободным (т.е. не используется или является аргументом) в g. В противном случае мы создадим выражение, которое ссылается на неизвестную переменную:
(\x -> (x+) x) to (x+) ???
Хорошо, вот соответствующая статья Википедии, для чего это стоит.
Краткая версия заключается в том, что такие определения верят в тело выражения лямбда с использованием заполнителя, такого как "M", и поэтому должны дополнительно указать, что переменная, привязанная этой лямбда, не используется в том, что представляет собой заполнитель.
Таким образом, "свободная переменная" здесь примерно означает переменную, определенную в некоторой двусмысленной или неизвестной внешней области - например, в выражении типа \y -> x + y, x является свободной переменной, но y не является.
Это сокращение касается удаления лишнего слоя привязки и немедленного применения переменной, которая (как вы, вероятно, себе представляете), действительна только в том случае, если рассматриваемая переменная используется только в одном месте.