η-ekspansja w czystym języku funkcjonalnym

Question

W SML, jest to legalne mieć w .mli:

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

i .ml:

let f x = x 
let g = f 

Jeszcze w F #, to zostanie odrzucony:

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. 

Jednym z rozwiązań jest η-rozszerzenie definicji g:

let g x = f x 

Jeśli mój kod jest czysto funkcjonalne (bez wyjątków, bez skutków ubocznych, itp) powinno to być odpowiednik (w rzeczywistości, to może być jeszcze lepiej w odniesieniu do polimorfizmu, w zależności od tego, jak język uogólnia typy: w SML aplikacje cząstkowe nie generują funkcji polimorficznych, ale ich η-ekspansja nie).

Czy istnieje jakakolwiek wada systematycznej rozbudowy η?

Dwie odpowiedzi wymykają się pytaniu o rozszerzenie η :-), a zamiast tego sugerują dodanie nawiasów wokół mojego typu funkcjonalnego. Dzieje się tak, ponieważ, jak widać, F # rozróżnia na poziomie pisania pomiędzy "prawdziwą" definicją funkcji (jak wyrażenia λ i wyliczone definicje, jak w aplikacjach częściowych); prawdopodobnie jest tak dlatego, że wyrażenia λ bezpośrednio mapują się do funkcji CLR, podczas gdy obliczone definicje odwzorowują obiekty delegowane. (Nie jestem pewny tej interpretacji i będę wdzięczny, jeśli ktoś bardzo znany z F # mogłyby wskazywać odwoływać dokumenty opisujące ten.)

Rozwiązaniem byłoby systematycznie dodać nawiasy do wszystkie typy funkcyjne w .mli, ale Obawiam się, że może to prowadzić do nieefektywności. Innym rozwiązaniem byłoby wykrycie obliczonych funkcji i dodanie nawiasów odpowiednich typów w .mli. Trzecim rozwiązaniem byłoby η-rozwinięcie oczywistych przypadków i nawrócenie pozostałych.

Nie jestem wystarczająco zaznajomiony z obiektami F #/CLR, aby zmierzyć, które z nich powodują znaczną wydajność lub łączą się z karami.

Answer 1

ciekawe mój fsi daje bardziej pomocny komunikat o błędzie:

/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. 

Jeśli dodać nawiasy, aby uzyskać g :('a -> 'a) wszystko jest w porządku

Answer 2

W teorii, F # Funkcja typ 'a -> 'b -> 'c jest tego samego typu jak 'a -> ('b -> 'c). Oznacza to, że wiele funkcji argumentu jest reprezentowanych za pomocą curried formularza w F #. Możesz użyć takiego, w którym w większości przypadków oczekuje się czegoś innego, np. podczas wywoływania funkcji wyższego rzędu.

Jednak ze względów praktycznych kompilator F # rzeczywiście rozróżnia typy - motywacją jest to, że są one reprezentowane w różny sposób w skompilowanym kodzie .NET. Ma to wpływ na wydajność, a także na współdziałanie z C#, więc warto dokonać tego rozróżnienia.

Funkcja Foo : int -> int -> int zostanie skompilowany jako członek int Foo(int, int) - kompilator nie używa curry formularz domyślnie, ponieważ jest to bardziej efektywne, gdy dzwoni Foo z obu argumentów (więcej częsty przypadek), a lepiej jest współdziałanie .Funkcja Bar : int -> (int -> int) zostanie skompilowana jako FSharpFunc<int, int> Bar(int) - w rzeczywistości przy użyciu postaci curry (i dlatego bardziej wydajne jest wywoływanie jej za pomocą tylko jednego parametru i będzie ona trudna do użycia z C#).

To także dlatego F # nie traktuje typów jako równych, jeśli chodzi o sygnatury - podpis określa typ, ale tutaj również określa sposób kompilacji funkcji. Plik implementacji musi zapewniać funkcję odpowiedniego typu, ale w tym przypadku także właściwego skompilowanego formularza.