Я хотел бы объявить тип данных ATS, представляющий число с фиксированной точкой с заданной точностью и точкой. Вот как я думал, что это должно быть сделано:
datatype fixed (t:int, n:int) = {n:nat} fixed (t, n) of (t)
Здесь я думаю, что int представляет «сортировку» всех целочисленных типов, что удобно для выполнения арифметических операций c , {n:nat}, я думаю, объявляет, что fixed является зависимым типом, параметризованным натуральным числом n, которое будет указывать битовый индекс, для которого возникает точка. Тогда fixed (t, n) указывает, что сам тип параметризован выбранным нами целочисленным типом t и значением индекса n, и конструктор должен быть применен к некоторому элементу типа t. Понятно, что мое понимание неверно, потому что я получаю следующую ошибку после запуска acc arithmetic.dats:
arithmetic.dats: 6:60-61
6| datatype fixed (t:int, n:int) = {n:nat} fixed (t, n) of (t)
^
error: the static expression is of the sort
t@ype
patsopt(TRANS2): there are [1] errors in total.
exit(ATS): (1025)
Это странно для меня, потому что я намеревался t, чтобы быть int. Как правильно объявить этот тип данных?