Получение типа выражения в SML

Я новичок в sml и пытаюсь понять, как получить тип выражения.
Я прочитал Получение выражения типа в ML, и я пытаюсь повторить то, что он сделал, чтобы получить мое выражение, но я не могу понять один отрывок.

Выражение, которое я пытаюсь вывести:

fn x => fn y => fn z => z(z(y x))

Я делаю следующее:

fn x : T1 => fn y : T2 => fn z : T3 => z(z(y x)) : T4

В этот момент должно быть

T2 = T1 -> T5                       //y x
T3 = T5 -> T6                       //z(y x)
T3 = T6 -> T7                       //z(z(y x))

вот где я думаю, что я делаю ошибку.

Также должно быть ограничение, например

T7 = T4 or T6 = T4.

Я не уверен и не ясен в этом вопросе.

Заранее спасибо за помощь.


types sml ml smlnj
person AscaL    schedule 03.04.2014    source источник

Ответы (1)


arrow_upward
1
arrow_downward

Вы уже присвоили T4 z(z(y x)), поэтому мы можем использовать его в последнем уравнении.

T3 = T5 -> T6                       //z(y x)
T3 = T6 -> T4                       //z(z(y x))

Так как T5 -> T6 = T6 -> T4, то T5 = T6 и T6 = T4.

person n. 1.8e9-where's-my-share m.    schedule 03.04.2014
comment
Спасибо за ответ, не могли бы вы объяснить, как T5 = T6 и T6 = T4? Мне не очень понятно. Извините, я не уверен, что я тупой или что-то в этом роде. - person AscaL; 04.04.2014
comment
Одна составная вещь T5 -> T6 равна другой составной вещи T6 -> T4, их соответствующие части также равны. - person n. 1.8e9-where's-my-share m.; 04.04.2014
comment
Большое спасибо, у меня были сомнения по этому поводу, но я решил это. Спасибо. - person AscaL; 04.04.2014