Стандартная полиморфная сортировка ML

Question

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

Начала вопрос

Полиморфной Сортировка

Эта функция выполняет вставки сортировку списка принимает в качестве аргументов функции сравнения меньше и список л элементов, отсортированных. Код компилируется и работает правильно:

fun sort(less, nil) = nil | 
    sort(less, a : : l) = 
     let 

fun insert(a, nil) = a : : nil | 
    insert(a, b : : l) = if less(a,b) then a : : (b: : l) 
            else b : : insert(a, l) 

in 
    insert(a, sort(less, l)) 
end; 

Каков тип функции сортировки? Вкратце объясните, включая тип вставки вспомогательной функции. Вам не нужно запускать алгоритм ML на этот код; просто объясните, почему обычный программист ML ожидал, что код будет иметь этот тип. () Вопрос)

Я получил тип функции сортировки (запустив код в интерпретаторе SML), но я просто не могу получить вторую часть о вставке.

Тип функции сортировки:

val sort = fn : ('a * 'a -> bool) * 'a list -> 'a list 

Любая помощь будет принята с благодарностью.

Answer 1

То, что вы выяснили тип sort путем «обмана», делает следующий шаг труднее; не используйте ярлыки.
(. Никто никогда не узнал ничего от выглядывает в ответ)

Но вот как вы могли бы выяснить insert:

Вы знаете из

val sort = fn : ('a * 'a -> bool) * 'a list -> 'a list 

, что второй аргумент sort является 'a list ,

В

insert(a, sort(less, l)) 

вы можете сразу увидеть, что он имеет некоторый тип (X * Y) -> Z для некоторогоX, Y и Z.

Вы передаете первый элемент второго аргумента sort - a - как первый аргумент insert.
Вторым аргументом sort является 'a list, первым элементом этого списка является 'a.
Так X является 'a, и теперь мы знаем, что insert является ('a * Y) -> Z для некоторыхY и Z.

Второй аргумент insert - sort(less, l) - хорошо известен; это 'a list.
Итак, мы теперь знаем, что Y является 'a list и insert является ('a * 'a list) -> Z для некоторыхZ.

Все, что остается возвращаемый тип, а с

insert(a, sort(less, l)) 

что sort возвращается, он должен иметь тот же тип возвращаемого sort.
So Z является 'a list.

В целом, тип insert «s является

('a * 'a list) -> 'a list