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. On Sun, Oct 28, 2018 at 9:07 PM Vanessa McHale <[email protected]> wrote: > 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? > On 10/28/18 6:05 PM, Hongwei Xi wrote: > > 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. > > > > > > On Sun, Oct 28, 2018 at 4:03 PM Vanessa McHale <[email protected]> > wrote: > >> 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 >> -- >> 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 [email protected]. >> To post to this group, send email to [email protected]. >> 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 >> <https://groups.google.com/d/msgid/ats-lang-users/4aba91ab-220c-ddc5-544c-f8c0a85abd27%40iohk.io?utm_medium=email&utm_source=footer> >> . >> > -- > 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 [email protected]. > To post to this group, send email to [email protected]. > 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/CAPPSPLr_MWMvrytD1UX%2Be63FfyCP4mb%2Br8G67xR2gm30s3AtNA%40mail.gmail.com > <https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLr_MWMvrytD1UX%2Be63FfyCP4mb%2Br8G67xR2gm30s3AtNA%40mail.gmail.com?utm_medium=email&utm_source=footer> > . > > -- > > > > *Vanessa McHale* > Functional Compiler Engineer | Chicago, IL > > Website: www.iohk.io <http://iohk.io> > Twitter: @vamchale > PGP Key ID: 4209B7B5 > > [image: Input Output] <http://iohk.io> > > [image: Twitter] <https://twitter.com/InputOutputHK> [image: Github] > <https://github.com/input-output-hk> [image: LinkedIn] > <https://www.linkedin.com/company/input-output-global> > > > 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 > > -- > 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 [email protected]. > To post to this group, send email to [email protected]. > 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/9c490b6b-7f2a-68c2-444c-4e5d9e47ad6d%40iohk.io > <https://groups.google.com/d/msgid/ats-lang-users/9c490b6b-7f2a-68c2-444c-4e5d9e47ad6d%40iohk.io?utm_medium=email&utm_source=footer> > . > -- 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 [email protected]. To post to this group, send email to [email protected]. 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/CAPPSPLooydXsYSx0CCgpu8OMN9K%2BXS_yE6331FJ9t-CC2CJEqw%40mail.gmail.com.
