Bluish Coder

The ATS programming language has a powerful type and proof system to enable safe construction of programs. Sometimes there is a need to cast a value from one type to another. ATS provides a feature that enables the programming to write their own rules specifying what can be cast. This becomes important when converting types from non-dependent typed values to dependantly typed values and dealing with conversion of proofs. This post goes through some common examples.

A casting function is introduced using the keyword castfn. It only has a declaration - there is no implementation or body of the casting function. From a value perspective there is no change to the actual value being cast, only to the type. It is effectively the identity function except for the type change. This means the cast is only allowed for types that are the same size, typically a machine word. There is no runtime overhead for using a casting function.

Standard Types

The following example ATS program attempts to add an integer to an unsigned integer value:

#include "share/atspre_define.hats"
#include "share/atspre_staload.hats"

implement main0() = let
  val x: uint = 5u
  val y: int = x + 5
in
  println!("y=", y)
end 

This results in a type error:

$ patscc -o c2 c2.dats
c2.dats: 133(line=6, offs=16) -- 138(line=6, offs=21):
         error(3): the symbol [+] cannot be resolved as no match is found.
c2.dats: 124(line=6, offs=7) -- 130(line=6, offs=13):
         error(3): the pattern cannot be given the ascribed type.
c2.dats: 124(line=6, offs=7) -- 130(line=6, offs=13):
         error(3): mismatch of static terms (tyleq):
The actual term is: S2Eerrexp()
The needed term is: S2Eapp(S2Ecst(g0int_t0ype); S2Eextkind(atstype_int))

The error is saying that the operator + has no matching implementation for the types provided. It is expecting an int but got something else.

The addition operator requires the two arguments to be of the same type. A casting function can be added to cast the unsigned integer to an integer:

#include "share/atspre_define.hats"
#include "share/atspre_staload.hats"

extern castfn int_of_uint(x: uint): int

implement main0() = let
  val x: uint = 5u
  val y: int = int_of_uint(x) + 5
in
  println!("y=", y)
end

This compiles and runs:

$ patscc -o c3 c3.dats
$ ./c3
y=10

A castfn looks very much like a fun declaration. It requires the name of the casting function, the argument it expects and a return type. There is no implementation as mentioned earlier. The compiler will convert the type of the argument to that of the return type. Another example follows showing conversion to a floating point value:

#include "share/atspre_define.hats"
#include "share/atspre_staload.hats"

extern castfn double_of_uint(x: uint): double

implement main0() = let
  val x: uint = 5u
  val y: double = double_of_uint(x) + 5.0
in
  println!("y=", y)
end

The castfn can have any name but most of the ATS prelude follows a format of including the 'from' and 'to' types in the name.

Dependent Types

Conversion between dependently typed values and non-dependently typed values are a common use of casting functions. For example:

val x: [n:int] size_t n = string1_length("hello")
val y: int = x + 1 // Error here, mismatch between dependent and non-dependent int

The type of x is dependently typed in that it has a type index of sort int for the length of the string. It is also of type size_t but the snippet expects an int. A castfn allows casing away the dependent type index and converting the type at the same time:

 #include "share/atspre_define.hats"
 #include "share/atspre_staload.hats"

 extern castfn int0_of_size1 {n:int} (x: size_t n): int

 implement main0() = let
   val x: [n:int] size_t n = string1_length("hello")
   val y: int = int0_of_size1(x) + 1
 in
   println!("y=", y)
 end 

Note the use of the '0' and '1' suffixes used for the type names in the castfn. This is an idiom in ATS naming where a '0' means not dependently typed and '1' means it has a dependent type.

It's possible to go in the other direction, casting from a non-dependent typed value to a dependently type value. This is an example of code that won't compile and needs a cast:

val x: int = 5
val y: [n:int] size_t n = x

This fails due to x and y being different types. Adding a cast function to convert the int to a size_t and including a type index will allow it to compile:

#include "share/atspre_define.hats"
#include "share/atspre_staload.hats"

extern castfn size1_of_int0 (x: int): [n:int] size_t n

implement main0() = let
  val x: int = 5
  val y: [n:int] size_t n = size1_of_int0(x)
in
  println!("y=", y)
end

Here the castfn adds an existential variable to the return type (the '[n:int]' part) to attach a type index of "unspecified integer value' to the type.

Another common use of casting functions is to convert different string types. A string is a non dependently typed string and a string1 is a dependently typed string with the length of the string as a type index. For example, arguments on a command line are string, but if a string function is called on it then there is a type error:

implement main0(argc, argv) =
  if argc > 1 then let
      val s: string = argv[1]
      val n = string1_length(s)
    in
      ()
    end
  else
    ()

Using a castfn can convert the string to a string1:

#include "share/atspre_define.hats"
#include "share/atspre_staload.hats"

extern castfn string1_of_string (s: string): [n:int] string n

implement main0(argc, argv) =
  if argc > 1 then let
      val s: string = argv[1]
      val n = string1_length(string1_of_string(s)) 
    in
      ()
    end
  else
    ()

Casting linear types

Types can be cast to and from linear types. When programming with strings in ATS you often deal with string which does not need to be manually free'd and strptr which is a linear type and needs to be manually free'd. Sometimes you want to treat a strptr as a string to call a string based function. An example is:

#include "share/atspre_define.hats"
#include "share/atspre_staload.hats"

extern fun strdup(s: string): [l:addr] strptr l = "ext#"
extern castfn strptr_to_string {l:addr} (s: !strptr l): string

implement main0() = let
  val s: [l:addr] strptr l = strdup("hello world")
  val n = string0_length(strptr_to_string(s))
  val _ = strptr_free(s)
in
  ()
end

This example needs to be compiled passing '-DATS_MEMALLOC_LIBC' to tell ATS to use the standard C malloc/free calls.

$ patscc -DATS_MEMALLOC_LIBC -o c8 c8.dats

For the purposes of this example I use a FFI function to call the C strdup function to copy a static string to a linear string that needs to be free'd. Note that the castfn does not consume this linear type (evidenced by the '!' prefixing the type name in the argument). This is dangerous because we can store the return value of the cast and use it after the free:

val oops = strptr_to_string(s)
val _ = strptr_free(s)
val _ = println!(oops)

The danger can be restricted by using locally scoped cast functions:

val n = string0_length(strptr_to_string(s)) where {
          extern castfn strptr_to_string {l:addr} (s: !strptr l): string
        }

Now strptr_to_string can only be used within that local block of code. Cast functions can be dangerous so need some care. There are various prelude casting functions for performing these types of conversions already.

Prelude unsafe casts

The prelude has an 'unsafe' module with a casting polymorphic function which can be used instead of defining casting functions for trivial things. There are also functions for converting strptr to string, etc. The equivalent of the previous example would be:

#include "share/atspre_define.hats"
#include "share/atspre_staload.hats"

staload UN = $UNSAFE

extern fun strdup(s: string): [l:agz] strptr l = "ext#"

implement main0() = let
  val s: [l:agz] strptr l = strdup("hello world")
  val n = string0_length($UN.strptr2string(s))
  val _ = strptr_free(s)
in
  ()
end

Basic type casting can be done using the cast function:

#include "share/atspre_define.hats"
#include "share/atspre_staload.hats"

staload UN = $UNSAFE

implement main0() = let
  val x: uint = 5u
  val y: int = $UN.cast{int}(x) + 5
in
  println!("y=", y)
end 

The swiss army knife of unsafe casting functions are castvwtp0 and castvwtp1. They can be used for casting linear types. The string example previously can use this:

val s: [l:agz] strptr l = strdup("hello world")
val n = string0_length($UN.castvwtp1{string}(s))
val _ = strptr_free(s)

castvwtp1 will not consume the input argument whereas castvwtp0 will. Looking through the prelude/SATS/unsafe.sats file will give an idea of the range of available functions.

The examples in this post are somewhat contrived in that there are standard prelude functions for doing most everything already. The need to cast string to string1 and strptr are reduced due to specific functions being available for those types. However it is useful to learn to use the castfn functionality and it is handy for one-off local casts, or defining protocols using proofs to ensure safe casting to and from types.