Sml Церковный вывод цифрового типа

Question

У меня есть это выражение в SML, и мне нужно найти его наиболее общий тип. При запуске через компилятор я получаю то, что показано ниже. Как мне найти наиболее общий тип не только этой функции, но и других функций, таких как церковные цифры, функция "два".

val one = fn f => (fn x => f x)

Почему тип этого:

('a -> 'b) -> 'a -> 'b

Answer 1

Что вы делаете, вы применяете процесс, который называется вывод типа Хиндли-Милнера.

Общий принцип состоит из трех этапов:

1. Сначала мы назначаем неопределенные типы (написано 'Z, 'Y, 'Xи т. д.) к переменным и выражениям.

   • Если выражение использует переменную, которой мы уже присвоили тип, то мы используем это. Например, если three уже был связан с типом int, затем в val nine = three * threeмы знаем, что three имеет тип int,
   • Если выражение использует переменную, которой мы уже присвоили нетривиальную схему типов (т.е. она полиморфна), то мы используем эту схему, но заменяем каждую переменную типа неопределенным типом. Например, если first уже был связан с типом 'a * 'b -> 'a, затем в val firstOfFirst = fn quartet => first (first quartet)мы назначаем один first тип 'Z * 'Y -> 'Z а другой тип 'X * 'W -> 'W,
   • Если в выражении используется новая связанная переменная (fn или же rec), тогда все вхождения этой переменной должны иметь один и тот же тип - в этот момент полиморфизм запрещен. Например, в fn f => (f 1, f "one") (что приводит к ошибке типа), мы изначально назначаем все вхождения f единственный тип 'Z, (Ошибка типа приводит к тому, что позже нам нужно уточнить это до int -> 'Y а также string -> 'Yи это противоречиво. Это потому, что Standard ML не поддерживает первоклассный полиморфизм.)

   В вашем примере val one = fn f => (fn x => f x)мы можем назначить f тип 'Z, а также x тип 'Y,

2. Затем мы выполняем объединение типов, где мы идентифицируем различные части типов различных подвыражений, которые должны соответствовать. Например, если мы знаем, что f имеет тип 'Z -> real и это i имеет тип intтогда, если мы увидим f iмы можем "объединить" 'Z с int и сделать вывод, что f имеет тип int -> real,

   • Существует множество деталей объединения типов, но я думаю, что все они в значительной степени соответствуют вашим ожиданиям, поэтому я не буду вдаваться в них.

   В вашем примере, так как f применяется к xмы можем объединить 'Z с 'Y -> ...и в конечном итоге назначить f тип 'Y -> 'X, Таким образом, выражение в целом имеет тип ('Y -> 'X) -> 'Y -> 'X,

3. Наконец, мы выполняем обобщение типов. Как только мы выполнили все унификации, которые можно выполнить - как только мы вывели все, что мы можем о типах - мы можем смело заменять неопределенные типы переменными связанного типа. В вашем случае это позволяет нам назначить one схема типов ∀ αβ . (α → β) → α → β (что означает "для любого и всех типов α и β, one имеет тип (α → β) → α → β"). В стандартных обозначениях ML мы не включаем явную часть"∀ αβ"; мы просто пишем ('a -> 'b) -> 'a -> 'b,

Answer 2

Я не очень понимаю ваш вопрос, поэтому я просто догадываюсь...

Если я определю первые церковные функции нумерации в REPL:

val c0 = fn f => fn x => x
val c1 = fn f => fn x => f x
val c2 = fn f => fn x => f (f x)
val c3 = fn f => fn x => f (f (f x))
val c4 = fn f => fn x => f (f (f (f x)))

... а затем посмотрите на их типы:

val c0 = fn : 'a -> 'b -> 'b
val c1 = fn : ('a -> 'b) -> 'a -> 'b
val c2 = fn : ('a -> 'a) -> 'a -> 'a
val c3 = fn : ('a -> 'a) -> 'a -> 'a
val c4 = fn : ('a -> 'a) -> 'a -> 'a 

... после 2-й функции появляется тип ('a ->'a) -> 'a -> 'a. Это общий тип, который вы ищете?

Тип первых двух функций отличается только тем, что алгоритм определения типа выбирает наиболее общий тип. А для первой функции 'a -> 'b -> 'b - более общий тип, как (' a -> 'a) ->' a -> 'a. Но вы всегда можете дать подсказку компилятору, используя аннотацию типа:

val c0 : ('a -> 'a) -> 'a -> 'a = fn f => fn x => x
val c1 : ('a -> 'a) -> 'a -> 'a = fn f => fn x => f x

... и все ваши функции теперь должны иметь одинаковый тип.