Вывод типа для полиморфной рекурсии, закодированной как рекурсия модуля

Question

Стандарт ML не имеет полиморфной рекурсии. Добавление рекурсии к языку модуля позволяет нам восстанавливать полиморфную рекурсию как особый случай, используя фиксированные точки endofunctors. Например:

signature SEQ = 
sig 
    type 'a seq 

    (* operations on sequences *) 
end 

functor BootstrapSeq (S : SEQ) = 
struct 
    datatype 'a seq 
    = Nil 
    | Zero of ('a * 'a) S.seq 
    | One of 'a * ('a * 'a) S.seq 

    (* operations on sequences *) 
end 

structure rec Seq = BootstrapSeq (Seq) 

Известно, что полиморфная рекурсия делает вывод типа неразрешимым. Однако определение функтора уже содержит информацию о частичном типе, а именно, подпись его аргумента. Является ли эта информация достаточной для повторения типового вывода?

Answer 1

Да, поскольку подпись обеспечивает «прямое объявление» полиморфного типа, поэтому его не нужно выводить рекурсивно. Кроме того, вам не нужен функтор, вы можете напрямую связать рекурсивную структуру. Но это требует аннотации подписи и, следовательно, составляет то же самое.