Types in ATS2

[Vanessa McHale]

Hi all,

Is there any literature on types in ATS such as &int? >> int?

fun ret_zero() : int =
  let
    fun initize(x : &int? >> int) : void =
      x := 0
    var ret: int
    val () = initize(ret)
  in
    ret
  end

I know that linear types are well-grounded in linear logic, but I know of no language that has this feature, and I cannot find any reference to it while skimming Girard's work...

Cheers

[Hongwei Xi]

Say you have a function of the interface:

fun foo(x: &T1 >> T2): T3

Internally, foo is given the following type:

fun foo{l:addr}(pf: T1@l | x: ptr(l)): (T2@l | T3)

The notation '&T1 >> T2' is referred to as before-and-after notation.

Here is a paper that contains a lot of technical details

on views and viewtypes:

http://www.ats-lang.org/Papers.html#VsTsVTs-2018-10-28

I came up with the original idea of viewtypes in ATS in the summer

of 2003. My plan back then was to finish an implementation first and then

write some papers. Fifteen years later, I am still working on the implementation :)

No longer so confident about working out a theoretical foundation for ATS.

An interesting idea is often a curse as it forces you to gamble on it.

--
You received this message because you are subscribed to the Google Groups "ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/4aba91ab-220c-ddc5-544c-f8c0a85abd27%40iohk.io.

[Vanessa McHale]

Thanks! What happens when you have

fun foo(x: &T1? >> T2): T3

rather than

fun foo(x: &T1 >> T2): T3

?

How does one handle uninitialized values? Is that just the ? modality?

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLr_MWMvrytD1UX%2Be63FfyCP4mb%2Br8G67xR2gm30s3AtNA%40mail.gmail.com.

--



Vanessa McHale
Functional Compiler Engineer | Chicago, IL

Website: www.iohk.io
Twitter: @vamchale
PGP Key ID: 4209B7B5






This e-mail and any file transmitted with it are confidential and intended solely for the use of the recipient(s) to whom it is addressed. Dissemination, distribution, and/or copying of the transmission by anyone other than the intended recipient(s) is prohibited. If you have received this transmission in error please notify IOHK immediately and delete it from your system. E-mail transmissions cannot be guaranteed to be secure or error free. We do not accept liability for any loss, damage, or error arising from this transmission

[Hongwei Xi]

fun foo(x: &T1? >> T2) : T3

means

fun foo(x: &(T1?) >> T2): T3

T1? is the uninitialized version of T1. Also, there is the subtype relation: T1 <= T1?

(if T1 is a non-linear type).

For every viewtype VT, there are V (linear) and T (non-linear) such that VT = (V | T).

This T can be referred to as VT?! in ATS.

Strictly speaking, only views can be linear. The linearity of a viewtype comes from the

view inside it.

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/9c490b6b-7f2a-68c2-444c-4e5d9e47ad6d%40iohk.io.