ats - g0ofg1 是什么意思？

Question

我经常在 ATS 中看到类似以下行的代码：

val xs = g0ofg1(xs)

函数 g0ofg1 看起来像是某种类型的转换。它实际上是做什么的？

Answer 1

这是一个重载符号。

ATS 中有许多类型，其中存在索引和非索引变体。

• 例如，存在int(i)（对于某些i排序int）和int。两种类型都用于整数，但前者是按int排序索引的。
• 另一个例子：string(just a string) and string(n)(length-indexed string)

g0ofg1用于将索引类型转换为非索引类型。它是一个 castfn，所以这个操作没有与之相关的运行时成本。

g1ofg0是朝着另一个方向发展：从非索引类型到索引类型。