Sml типа путаница

Question

У меня есть эта функция:

fun x (u,v,w) = (u::[v])::w; 

который получает тип возврата

fn: 'a * 'a * 'a list list -> 'a list list 

Может кто-нибудь объяснить мне, как этот тип генерируется из функции? Спасибо!

Редактировать: Также как я могу назвать эту функцию?

Answer 1

:: принимает два аргумента - один слева и один справа. Если его левый аргумент имеет тип t, то его правый аргумент должен быть типа t list.

Таким образом, :: имеет тип ('a * 'a list) -> 'a list, как t является произвольным, и, таким образом, представлен в 'a.

Если у вас есть код (u::[v]), поэтому, вы говорите, что SML u : t и 'v : t для некоторого типа t. Это выражение тогда равно t list, и поэтому для использования его в качестве левого аргумента в :: правильный аргумент w должен иметь тип t list list.

Это значит, что тип (u::[v])::w составляет t list list для некоторых t.

В итоге:
u : t
v : t
w : t list
(u::[v])::w : t list list,

все для некоторого типа t.

Таким образом, тип x равен ('a * 'a * 'a list) -> 'a list list, так как t является произвольным.

Чтобы вызвать эту функцию, вы можете сделать что-то вроде x(1,2,[3,4]), что дало бы список [[1,2],[3,4]].