Функция, которая применяет свой аргумент к себе? - PullRequest
Новая
       38

Функция, которая применяет свой аргумент к себе?

7 голосов
/ 06 февраля 2012

Рассмотрим следующую функцию SML: 

fn x => x x

Это приводит к следующей ошибке (Standard ML of New Jersey v110.72): 

stdIn:1.9-1.12 Error: operator is not a function [circularity]
  operator: 'Z
  in expression:
    x x

Я могу понять, почему это не разрешено - например, я не совсем уверен, как записать, каким будет его тип - но это не совсем бессмысленно; например, я мог бы передать ему функцию идентификации и вернуть ее обратно.

Есть ли название для этой функции? (Есть ли способ выразить это в SML?)

Ответы [ 2 ]

7 голосов
/ 06 февраля 2012

Нет способа выразить эту функцию на языке с ML-подобной системой типов.Даже с функцией идентификации это не сработает, потому что первый x и второй в x x должны быть разными экземплярами этой функции типа (_a -> _a) -> (_a -> _a) и _a -> _a соответственно для некоторого типа _a.

На самом деле системы типов предназначены для запрета таких конструкций, как 

(λx . x x) (λx . x x)

в нетипизированном лямбда-исчислении.В динамически типизированной языковой схеме вы можете написать эту функцию: 

(define (apply-to-self x) (x x))

и получить ожидаемый результат 

> (define (id x) x)
> (eq? (apply-to-self id) id)
#t
4 голосов
/ 07 февраля 2012

Подобные функции часто встречаются в комбинаторах с фиксированной запятой. например одна форма Y комбинатора написана λf.(λx.f (x x)) (λx.f (x x)). Комбинаторы с фиксированной запятой используются для реализации общей рекурсии в нетипизированном лямбда-исчислении без каких-либо дополнительных рекурсивных конструкций, и это является частью того, что делает нетипизированное лямбда-исчисление Тьюринг-полным.

Когда люди разработали лямбда-исчисление простого типа , которое представляет собой наивную систему статического типа поверх лямбда-исчисления, они обнаружили, что больше нельзя писать такие функции. Фактически, невозможно выполнить общую рекурсию в простом типе лямбда-исчисления; и, следовательно, лямбда-исчисление с простым типом больше не является полным по Тьюрингу. (Одним интересным побочным эффектом является то, что программы в простом типе лямбда-исчисления всегда завершаются.)

Настоящие статически типизированные языки программирования, такие как Standard ML, нуждаются во встроенных рекурсивных механизмах для решения проблемы, таких как именованные рекурсивные функции (определенные с помощью val rec или fun) и именованные рекурсивные типы данных.

Все еще возможно использовать рекурсивные типы данных для имитации чего-то вроде того, что вы хотите, но это не так красиво.

По сути, вы хотите определить тип как 'a foo = 'a foo -> 'a; Однако это не допускается. Вместо этого вы оборачиваете его в тип данных: datatype 'a foo = Wrap of ('a foo -> 'a);

datatype 'a foo = Wrap of ('a foo -> 'a);
fun unwrap (Wrap x) = x;

Как правило, Wrap и unwrap используются для преобразования между 'a foo и 'a foo -> 'a и наоборот.

Всякий раз, когда вам нужно вызвать функцию для себя, вместо x x, вы должны явно написать (unwrap x) x (или unwrap x x); то есть unwrap превращает его в функцию, которую можно затем применить к исходному значению.

P.S. Другой язык ML, OCaml, имеет возможность включить рекурсивные типы (обычно отключенные); если вы запускаете интерпретатор или компилятор с флагом -rectypes, то можно написать что-то вроде fun x -> x x. По сути, за кулисами средство проверки типов определяет места, где необходимо «обернуть» и «развернуть» рекурсивный тип, а затем вставляет их для вас. Я не знаю ни о какой реализации Standard ML, имеющей аналогичную функциональность рекурсивных типов.

...