Η-разложение в чисто функциональном языке

В OCaml законно иметь в .mli:

val f : 'a -> 'a
val g : 'a -> 'a

и .ml:

let f x = x
let g = f

Однако в F # это отклоняется:

eta_expand.ml(2,5): error FS0034: Module 'Eta_expand' contains
    val g : ('a -> 'a)    
but its signature specifies
    val g : 'a -> 'a    

The arities in the signature and implementation differ. The signature specifies that 'g' is function definition or lambda expression accepting at least 1 argument(s), but the implementation is a computed function value. To declare that a computed function value is a permitted implementation simply parenthesize its type in the signature, e.g.
    val g: int -> (int -> int)
instead of
    val g: int -> int -> int.

Обходным путем является η-расширение определения g:

let g x = f x

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

Есть ли какой-либо недостаток систематического η-расширения?

Два ответа ускользают от вопроса о η-расширении:-), и вместо этого предположим, что я добавляю круглые скобки вокруг своего функционального типа. Это связано с тем, что, по-видимому, F # различает уровень ввода между "истинным" определением функций (как λ-выражения и вычисляемые определения, как в частичных приложениях); предположительно это связано с тем, что λ-выражения непосредственно отображаются в функции CLR, тогда как вычисляемые определения сопоставляют делегирование объектов. (Я не уверен в этой интерпретации и буду признателен, если кто-то, кто очень хорошо знаком с F #, может указать на справочные документы, описывающие это.)

Решение заключалось бы в систематическом добавлении скобок ко всем типам функций в .mli, но я боюсь, что это может привести к неэффективности. Другим было бы обнаружение вычисленных функций и добавление в скобки соответствующих типов в .mli. Третьим решением было бы η-развернуть очевидные случаи и заключить в скобки другие.

Я недостаточно осведомлен о внутренних функциях F #/CLR, чтобы измерить, какие из них несут существенную производительность или сопрягают штрафы.

Ответ 1

Теоретически тип функции F # 'a -> 'b -> 'c является тем же типом, что и 'a -> ('b -> 'c). То есть, несколько функций аргументов представлены с использованием карри в форме F #. Вы можете использовать тот, который ожидается в большинстве случаев, например, при вызове функции более высокого порядка.

Однако, по практическим соображениям, компилятор F # действительно различает типы - мотивация заключается в том, что они представлены по-разному в компилированном .NET-коде. Это влияет на производительность, а также совместимость с С#, поэтому полезно сделать это различие.

Функция Foo : int -> int -> int собирается скомпилироваться как член int Foo(int, int) - компилятор не использует валютную форму по умолчанию, потому что это более эффективно при вызове Foo с обоими аргументами (более общий случай) и это лучше для взаимодействия. Функция Bar : int -> (int -> int) будет скомпилирована как FSharpFunc<int, int> Bar(int) - фактически с использованием карри-формы (и поэтому более эффективно вызывать ее только с одним параметром, и ее будет сложно использовать с С#).

Кроме того, F # не рассматривает типы как равные, когда речь идет о сигнатурах - подпись задает тип, но здесь также указывается, как должна собираться функция. Файл реализации должен обеспечивать функцию правильного типа, но - в этом случае - также из правой скомпилированной формы.

Ответ 2

Интересно, что мой fsi дает более полезное сообщение об ошибке:

/test.fs(2,5): error FS0034: Module 'Test' contains
    val g : ('a -> 'a) but its signature specifies
    val g : 'a -> 'a The arities in the signature and implementation differ. 
          The signature specifies that 'g' is function definition or lambda expression 
          accepting at least 1 argument(s), but the implementation is a computed 
          function value. To declare that a computed function value is a permitted 
          implementation simply parenthesize its type in the signature, e.g.
        val g: int -> (int -> int) instead of
        val g: int -> int -> int.

Если вы добавляете скобки для получения g :('a -> 'a), все в порядке