ATS - datatype declaration parametrized by `int` sort

111 Views Asked by At

I would like to declare an ATS datatype representing a fixed point number with given precision and point. Here is how I thought it should be done:

datatype fixed (t:int, n:int) = {n:nat} fixed (t, n) of (t)

Here I am thinking as though int represents the "sort" of all integer-like types, which is convenient for doing arithmetic operations. {n:nat}, I think, declares that fixed is a dependent type parametrized by the natural number n, which will indicate the bit index for which the point occurs. Then fixed (t, n) indicates that the type itself is parametrized by the integer type, t, that we choose and the index value n, and the constructor must be applied to some element of the type t. Clearly, my understanding is flawed, because I receive the following error after running 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)

This is strange to me because I intended t to be of the sort int. What would be the proper way to declare this datatype?

1

There are 1 best solutions below

0
Hongwei Xi On

How about:

datatype fixed (int(*sort*)) = {n:nat} fixed (n) of (int(*type*))

The confusion may be due to int being both a sort and a type in ATS.