Перечислить переменную перед именем функции и ограничениями в области видимости

Question

Недавно я заметил, что перед именем функции в объявлении функции допускается переменная типа. Но я не вижу, как он используется. Вот несколько примеров:

Poly/ML 5.5.2 Release 
> fun 'a print a = PolyML.print (a); 
val print = fn: 'a -> 'a 
> print "foo"; 
? 
val it = "foo": string 
> pint string "foo"; 
Error-Value or constructor (string) has not been declared 
Found near print string "foo" 
Static Errors 
> string print "foo"; 
Error-Value or constructor (string) has not been declared 
Found near string print "foo" 
Static Errors 
> val f : string -> string = print; 
val f = fn: string -> string 
> f "foo"; 
? 
val it = "foo": string 

Поэтому у меня есть несколько вопросов, основанных на этом. Во-первых, что является хорошим примером использования для переменной типа перед именем функции (в отличие от более распространенной переменной типа в аргументе или сигнатуре типа возврата). Кроме того, есть ли способ, чтобы указать, что я хочу, чтобы специализироваться на типе, как, как я могу с типом ?:

> type 'a t = 'a list; 
eqtype 'a t 
> type f = string t; 
type f = string t 

Я объявляю специализацию, создав новую переменную val f, с явной сигнатуры типа , но я не думаю, что это одно и то же. Например, исходя из приведенного выше примера типа, я ожидал, что смогу это сделать:

> val s = string print; 
Error-Value or constructor (string) has not been declared Found near string print 
Static Errors 

Но это не удается.

И, наконец, почему переменная типа спрятала тип аргумента внутри функции? Я только предполагаю, что это происходит вообще, потому что функция PolyML.print печатает знак вопроса (указав, что он не знает тип), а не фактическое значение. Даже когда я объявлял новую функцию f, которая явно ограничивала тип, она все еще не знала тип передаваемых переменных. (Хотя я уверен, что эта конкретная часть не имеет ничего общего с исходной переменной типа функции, а скорее переменной типа (неявный) по аргументу a.)

Answer 1

Идея наличия переменных типа сразу после fun заключается в том, что он использует последующие виды использования переменной типа. Рассмотрим различия между

> fun f x = 
# let 
#  fun I (y:'a): 'a = y 
# in 
#  I I 
# end; 
val f = fn: 'a -> 'b -> 'b 

и

> fun 'a f x = 
# let 
#  fun I (y:'a): 'a = y 
# in 
#  I I 
# end; 
Type error in function application. 
    Function: I : 'a -> 'a 
    Argument: I : 'a -> 'a 
    Reason: 
     Can't unify 'a to 'a -> 'a (Cannot unify with explicit type variable) 

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

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

И, наконец, обратите внимание на использование PolyML.print в качестве примера. Это не обычная полиморфная функция ML, а бесконечно перегруженная функция, которая печатает свой аргумент в зависимости от информации о типе во время компиляции. Это расширение Poly/ML, поэтому он находится в структуре PolyML, хотя print присутствовал в раннем проекте того, что стало стандартным ML.