Я часто вижу код, похожий на следующую строку в ATS:
val xs = g0ofg1(xs)
Функция g0ofg1 выглядит как некий кастинг. Что он на самом деле делает?
Я часто вижу код, похожий на следующую строку в ATS:
val xs = g0ofg1(xs)
Функция g0ofg1 выглядит как некий кастинг. Что он на самом деле делает?
Это перегруженный символ.
В ATS есть много типов, для которых существуют индексированные и неиндексированные варианты.
int(i)
(для некоторых i
сорта int
) и int
. Оба типа предназначены для целых чисел, но первый индексируется сортировкой int
.string
(просто строка) и string(n)
(строка с индексом длины)g0ofg1
предназначен для преобразования индексированного типа в неиндексированный. Это castfn, поэтому с этой операцией не связаны затраты времени выполнения.
g1ofg0
предназначен для перехода в другом направлении: от неиндексированного к индексированному типу.