Странность равенства списка SML

Question

У меня есть этот бит кода:

fun foldr2(f, x::xs) =
    if xs = [] then
      x
    else
      f(x, foldr2(f, xs))

С сигнатурой типа

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

Выглядит довольно просто, требуется функция, которая работает над типами равенства и спискомтипа равенства в качестве аргументов из-за сравнения xs = [].Однако по какой-то причине он работает на вводе, таком как (op +, [2.3, 2.7, 4.0]), когда в SML / NJ вещественные числа не являются типом равенства.Может ли кто-нибудь помочь мне пролить свет на то, почему происходит это волшебство?

Answer 1

Я полагаю, что это связано с магическим способом, которым + перегружен для реалов. Для меня это почти на грани того, чтобы быть ошибкой компилятора, хотя я должен был бы взглянуть на определение SML97, чтобы точно понять, каким должно быть правильное поведение. Перегрузка над + - это что-то вроде неприятного темного угла в SML, ИМХО.

Например, если вы определяете функцию типа real * real -> real и передаете ее в качестве аргумента foldr2, вы получите ожидаемую ошибку типа:

fun f (x : real * real) = 134.5
foldr2 (f, [1.4, 2.25, 7.0])
  stdIn:8.1-8.29 Error: operator and operand don't agree [equality type required]

Вы даже можете вызвать ошибку типа, если просто добавите аннотацию типа к op +, что в основном привело меня к выводу, что перегрузка + вызывает таинственный эффект.