Search code examples
ats

What is the meaning of g0ofg1?

I often see code like the following line in ATS:

val xs = g0ofg1(xs)

The function g0ofg1 looks like some kind of casting. What does it actually do?

Solution

  • This is an overloaded symbol.

    There are many types in ATS for which there exist an indexed and a non-indexed variant.

    • For instance, there exists int(i) (for some i of sort int) and int. Both types are for integers, but the former is indexed by int sort.
    • Another example: string (just a string) and string(n) (length-indexed string)

    g0ofg1 is for converting an indexed type into a non-indexed one. It's a castfn, so this operation has no runtime cost associated with it.

    g1ofg0 is for going in the other direction: from non-indexed to indexed type.