8. Showing types¶

8.1. $showtype directive¶

xxx

8.2. Integer¶

We learned that the of literal 3 is int. By the way, we can directly watch the type of values using the $showtype. Let’s write following code named showtype_int.dats:

1
2
3
4
5

(* File: showtype_int.dats *)
val () = println! 3
val _ = $showtype 3

implement main0 () = ()

Then, compile it.

$ patscc showtype_int.dats
**SHOWTYPE**(/tmp/showtype_int.dats: 69(line=3, offs=19) -- 70(line=3, offs=20)): S2Eapp(S2Ecst(g1int_int_t0ype); S2Ecst(int_kind), S2Eintinf(3))

The console shows a message with **SHOWTYPE**. The message explains the type of integer literal 3, and “S2Eapp(S2Ecst(g1int_int_t0ype); S2Ecst(int_kind), S2Eintinf(3))” is a internal representation of the ATS’s type. However, it’s hard to read by a beginner. Let’s learn more detail.

• S2Ecst is a type constant (for instance, int, bool, list, etc.) For now, it introduces two type constants g1int_int_t0ype and int_kind.
• S2Eintinf is an infinite precision integer. For now, it introduces the constant 3.
• S2Eapp is an application term. For now, it applies two arguments int_kind and 3 to g1int_int_t0ype.

Let’s do pretty-print the message such like ATS code style.

g1int_int_t0ype(int_kind, 3)

That is the value of integer literal 3 is applied int type depending on integer literal 3. The type depending on some value is called as dependent type. Please read “Internal types” page at ATS2 wiki, if you understand more of the internal representation of dependent type.

We learned addition, subtraction and multiplication on integers. Create a new file int_op.dats to watch the type using $showtype directive.

1
2
3
4
5
6
7
8

(* File: int_op.dats *)
#include "share/atspre_staload.hats"

val () = println! ($showtype 3 + 4 * 2)
val () = println! ($showtype (3 + 4) * 2)
val () = println! ($showtype 2 - 3)

implement main0 () = ()

We can inject $showtype directive into ATS code such like int_op.dats, because the $showtype directive directly returns the argument. Let’s compile and run it.

$ patscc int_op.dats
**SHOWTYPE**(/tmp/int_op.dats: 92(line=4, offs=30) -- 101(line=4, offs=39)): S2Eapp(S2Ecst(g1int); S2EVar(4143->S2Eextkind(atstype_int)), S2Eapp(S2Ecst(+); S2EVar(4144->S2Eintinf(3)), S2EVar(4145->S2Eapp(S2Ecst(mul_int_int); S2EVar(4141->S2Eintinf(4)), S2EVar(4142->S2Eintinf(2))))))
**SHOWTYPE**(/tmp/int_op.dats: 133(line=5, offs=31) -- 143(line=5, offs=41)): S2Eapp(S2Ecst(g1int); S2EVar(4149->S2Eextkind(atstype_int)), S2Eapp(S2Ecst(*); S2EVar(4150->S2Eapp(S2Ecst(add_int_int); S2EVar(4147->S2Eintinf(3)), S2EVar(4148->S2Eintinf(4)))), S2EVar(4151->S2Eintinf(2))))
**SHOWTYPE**(/tmp/int_op.dats: 174(line=6, offs=30) -- 179(line=6, offs=35)): S2Eapp(S2Ecst(g1int); S2EVar(4152->S2Eextkind(atstype_int)), S2Eapp(S2Ecst(-); S2EVar(4153->S2Eintinf(2)), S2EVar(4154->S2Eintinf(3))))
$ ./a.out
11
14
-1

Result of running executable is intended by readers. However, the type printed by $showtype is more complex than simple integer literal. Let’s pretty-print the internal type representation of 3 + 4 * 2.

g1int(atstype_int, (3 + (mul_int_int(4, 2))))

First argument of g1int explains this type is int type. Second argument of g1int directly explains the calculation 3 + 4 * 2. mul_int_int is for the function doing multiplication on type-level. That is ATS’s dependent type knows how the value of int type is computed.

What kinds of situations is these dependent type good for?

xxx About division operator

8.3. Character string¶

xxx

8.4. Function¶

xxx