What is ”kind” on ATS2?

Google Group
1

A kind (or t-kind) is essentially a name for an external type.
The keyword ‘tkindef’ introduces a t-kind. Here is an example:

https://github.com/githwxi/ATS-Postiats-contrib/blob/master/contrib/libats-/hwxi/cstream/SATS/cstream.sats

This is largely an obscure feature. You don’t really need to use t-kind;
you can use ‘t@ype’ instead.On Sunday, January 4, 2015 12:23:13 AM UTC-5, Kiwamu Okabe wrote:

Hi all,

Sometimes, I encounter that I should wrap C language datatypes with
ATS2’s strong types.
ATS2 can’t understand size of the type using simply wrapping.

However, ATS2 prelude can easily manage the size of type “uint64”,
while body of the “uint64” is defined at C language.
I guess it realizes on ATS2 “kind” mechanism.

What is ”kind” and “tkindef” on ATS2?

// File: prelude/basics_sta.sats 
tkindef 
uint64_kind = "atstype_uint64" 
typedef 
uint64_0 = g0uint (uint64_kind) 
typedef 
uint64_1 (i:int) = g1uint (uint64_kind, i) 
stadef uint64 = uint64_1 // 2nd-select 
stadef uint64 = uint64_0 // 1st-select 
stadef uInt64 = [i:nat] uint64_1 (i) 

// File: prelude/SATS/integer_fixed.sats 
stadef uint64knd = uint64_kind 

// File: prelude/CATS/integer_fixed.cats 
typedef uint64_t atstype_uint64 ;

Thank’s,

Kiwamu Okabe at METASEPI DESIGN

2

A t-kind is essentially an abstract type that is solely needed for its name.

As I mentioned in an earlier message, this feature is obscure and should be
avoided. It is also readily avoidable.On Wednesday, May 13, 2015 at 11:29:50 AM UTC-4, Yannick Duchêne wrote:

Le dimanche 4 janvier 2015 08:12:50 UTC+1, gmhwxi a écrit :

A kind (or t-kind) is essentially a name for an external type.
The keyword ‘tkindef’ introduces a t-kind. Here is an example:

https://github.com/githwxi/ATS-Postiats-contrib/blob/master/contrib/libats-/hwxi/cstream/SATS/cstream.sats

This is largely an obscure feature. You don’t really need to use t-kind;
you can use ‘t@ype’ instead.

In basics_sta.sats, it seems to be used to introduce atstype_…,
exclusively.

3

A kind (or t-kind) is essentially a name for an external type.
The keyword ‘tkindef’ introduces a t-kind. Here is an example:

https://github.com/githwxi/ATS-Postiats-contrib/blob/master/contrib/libats-/hwxi/cstream/SATS/cstream.sats

This is largely an obscure feature. You don’t really need to use t-kind;
you can use ‘t@ype’ instead.

In basics_sta.sats, it seems to be used to introduce atstype_…,
exclusively.