OCaml предава етикетирана функция като еквивалентност на параметър/маркиран тип функция

Да предположим, че функция g е дефинирана по следния начин.

utop # let g ~y ~x = x + y ;;
val g : y:int -> x:int -> int = <fun>
utop # g ~x:1 ;;
- : y:int -> int = <fun>
utop # g ~y:2 ;;
- : x:int -> int = <fun>
utop # g ~x:1 ~y:2 ;;
- : int = 3
utop # g ~y:2 ~x:1 ;;
- : int = 3

Сега има друга функция foo

utop # let foobar (f: x:int -> y:int -> int) = f ~x:1 ~y:2 ;;
val foobar : (x:int -> y:int -> int) -> int = <fun>

За съжаление, когато се опитам да осигуря g като параметър на foobar, той се оплаква:

utop # foobar g ;;
Error: This expression has type y:int -> x:int -> int
       but an expression was expected of type x:int -> y:int -> int

Това е доста изненадващо, тъй като мога успешно да currify g, но не мога да го предам като параметър. Търсих в Google и намерих тази статия, която не помага много. Предполагам, че това е свързано с основната система от типове на OCaml (напр. правила за подтипиране на обозначени типове стрелки).

Така че възможно ли е да се предаде g като параметър на foobar по какъвто и да е начин в OCaml? Ако не, защо не е позволено? Всякакви спомагателни статии/книги/статии биха били достатъчни.


functional-programming ocaml type-theory
person Xiao Jia    schedule 05.01.2014    source източник

Отговори (3)


arrow_upward
5
arrow_downward

Ключът е, че етикетите не съществуват по време на изпълнение. Функция от тип X:int -> y:float -> int наистина е функция, чийто първи аргумент е int, а втори аргумент е float.

Извикването на g ~y:123 означава, че съхраняваме втория аргумент 123 някъде (в затваряне) и ще го използваме автоматично по-късно, когато оригиналната функция g най-накрая бъде извикана с всичките си аргументи.

Сега разгледайте функция от по-висок ред като foobar:

let foobar (f : y:float -> x:int -> int) = f ~x:1 ~y:2.

(* which is the same as: *)
let foobar (f : y:float -> x:int -> int) = f 2. 1

Функцията f, предадена на foobar, приема два аргумента и float трябва да бъде първият аргумент по време на изпълнение.

Може би би било възможно да подкрепим вашето желание, но това би добавило малко режийни разходи. За да работи следното:

let g ~x ~y = x + truncate y;;
foobar g  (* rejected *)

компилаторът ще трябва да създаде допълнително затваряне. Вместо това от вас се изисква да го направите сами, както следва:

let g ~x ~y = x + truncate y;;
foobar (fun ~y ~x -> g ~x ~y)

Като цяло компилаторът OCaml е много лесен и няма да извърши този вид трудно за отгатване вмъкване на код вместо вас.

(И аз не съм теоретик на типа)

person Martin Jambon    schedule 05.01.2014
comment
Намирам за забавно, че fun ~y ~x -> g ~y ~x работи също толкова добре, но вашата форма вероятно е по-ясна за заетия четец на кодове. - person gasche; 05.01.2014

arrow_upward
2
arrow_downward

Мислете вместо типовете x:int -> y:float -> int и y:float -> x:int -> int. Твърдя, че не са от един и същи тип, защото можете да ги наричате без етикети, ако искате. Когато направите това, първият изисква int като първи параметър и float като втори. Вторият тип ги изисква в обратен ред.

# let f ~x ~y = x + int_of_float y;;
val f : x:int -> y:float -> int = <fun>
# f 3 2.5;;
- : int = 5
# f 2.5 3;;
Error: This expression has type float but an expression was
expected of type int 

Друго усложнение е, че функциите могат да имат някои етикетирани и някои немаркирани параметри.

В резултат на това етикетираните параметри на функция се третират като последователност (в определен ред), а не като набор (без присъщ ред).

Вероятно, ако изисквате всички параметри да бъдат етикетирани и премахнете възможността за извикване без етикети, бихте могли да накарате нещата да работят по начина, по който очаквате.

(Отказ от отговорност: Не съм теоретик на типа, въпреки че ми се иска да бях.)

person Jeffrey Scofield    schedule 05.01.2014

arrow_upward
2
arrow_downward

Тази клопка на етикетите в OCaml е описана подробно в Етикети и въведете inference подраздел на ръководството за OCaml, давайки пример, подобен на вашия.

Ако си спомням правилно, някои типови системи за етикети премахват това ограничение, но с цената на допълнителна цялостна сложност, която беше оценена като „не си струва“ за самия език OCaml. Етикетите могат да бъдат пренаредени автоматично в сайтове за приложение от първи ред, но не и при абстрахиране върху етикетирани функции (или използване на такива абстракции).

Можете да приемете вашия пример чрез ръчно ета-разгъване на етикетираната функция, за да се появи приложение с възможност за пренареждане (теоретик на типа би казал, че това е пренаписване на ета-преобразуване):

# let f ~x ~y = x+y;;
val f : x:int -> y:int -> int = <fun>
# let yx f = f ~y:0 ~x:1;;
val yx : (y:int -> x:int -> 'a) -> 'a = <fun>
# yx f;;
Error: This expression has type x:int -> y:int -> int
       but an expression was expected of type y:int -> x:int -> 'a
# yx (fun ~y ~x -> f ~y ~x);;
- : int = 1
person gasche    schedule 05.01.2014