как мне назначить выражение со свободными переменными типа, как я назначаю другие функции f как val x = f:? - PullRequest
1 голос
/ 07 марта 2020

как мне назначить выражение со свободными переменными типа, как я назначаю другие функции f как val x = f: ??

У меня есть

 fun curry f  x  y = f (x,y);
 val dummy = fn (x,y) => {a=x,b=y}  (* or anything with free type *)
 val dummCd = fn x=> fn y=> {a=x,b=y}

Я думал, что "пустышка карри" будет работать как "dummCd", но,

 dummCd
 val it = fn: 'a -> 'b -> {a: 'a, b: 'b}

и

 curry dummy:
 stdIn:13.1-13.8 Warning: type vars not generalized because of
   value restriction are instantiated to dummy types (X1,X2,...)
 val it = fn : ?.X1 -> ?.X2 -> {a:?.X1, b:?.X2}

Так что это становится бесполезным при назначении. Я могу сделать это:

 fun x a b =curry dummy a b ;  

но это немного неуклюже. Когда я помещаю то, что я делаю здесь, в функцию

 val a = fn tr => (fn a=> fn b=> tr a b)
 val x = a (curry dummy)
 val x = fn : ?.X1 -> ?.X2 -> {a:?.X1, b:?.X2}

, я получаю ту же проблему обратно. Как я могу назначить «пустышку карри», не используя дополнительные a и b? Я имею в виду

 val x =  a ( curry dummy )

, где a может быть функцией, а x ведет себя как dummCd

Спасибо за советы

1 Ответ

2 голосов
/ 08 марта 2020

К сожалению, вы не можете делать то, что хотите.

В стандарте ML '97 объявление значения может связывать переменную типа только в том случае, если правая часть привязки является неэкспансивным выражением. Это означает, что он соответствует очень ограниченному подмножеству синтаксиса выражения, которое не позволяет генерировать какие-либо новые ссылочные ячейки или имена исключений. Поскольку это проверка syntacti c, она вообще не учитывает определение curry; вы знаете, что curry не создает никаких ячеек ссылок или имен исключений (и поэтому val dummCd = curry dummy будет безопасным), но все, что компилятор видит в этой точке, это то, что curry dummy вызывает функцию что может делать такие вещи.

Так что если вы хотите, чтобы dummCd вызывался с произвольными типами (т. е. вы хотите, чтобы у него была схема нетривиального типа ∀αβ.α → β → {a: α, b: β} с переменными связанного типа), тогда вам необходимо объявить его, например, с помощью val dummCd = fn ... или fun dummCd ...; вы не можете просто написать val dummCd = ... с тем, что вы хотите, с правой стороны.

Стандартный ML '90 был немного более разрешительным в этом отношении - он закодировал соответствующую информацию о поведении curry в систему типов (помечая переменную типа как «императивную», например, '_a, а не 'a, если она была задействована в типах любых ячеек ссылок или имен исключений), и использовала эту информацию типа, чтобы решить, val dummCd = curry dummy должно быть разрешено связывать свои переменные типа - но эта система считалась слишком запутанной и сложной, тем более что она вынуждала детали реализации к сигнатурам, поэтому она была пересмотрена в стандарте ML '97 и заменена на текущую систему только для синтаксиса, где все переменные типа считаются обязательными.

...