<> in first part of function return type

[Brandon Barker]

This is probably obvious or something I just missed, but I see it now and then, e.g. the "<>" in the function below

fun string_get_char_at

  {n:int}

  {i:nat | i < n} (

  str: string n, i: size_t i

) :<> c1har

  = "atspre_string_get_char_at"

[gmhwxi]

:<> means that this functions is pure, that is, it does not cause observable effects.

[Chris Double]

As well as :<> meaning pure there are various other things that can appear between the '<>' symbols. I describe some of them here:

<http://www.bluishcoder.co.nz/2010/06/13/functions-in-ats.html>

Basically:

!exn - the function possibly raises exceptions
!ntm - the function possibly is non-terminating
!ref - the function possibly updates shared memory
0 - the function is pure (has no effects)
1 - the function can have all effects
fun - the function is an ordinary, non-closure, function
clo - the function is a stack allocated closure
cloptr - the function is a linear closure that must be explicitly freed
cloref - the function is a peristent closure that requires the garbage collector to be freed.
lin - the function i slinear and can be called only once
prf - the function is a proof function

These can be combined, eg. <lincloptr1>.

Are there any I've missed or got wrong?

[gmhwxi]

I think you've got all of them :)

In ATS2, there is also '!wrt', which indicates that a function may write to a location it owns. For instance, ptr_set incurs such an effect. In contrast, '!ref' means reading from or writing to a location that one knows exists but does not own.

[Brandon Barker]

I was looking over list.sats and noticed what looked like a sort called "eff". Is this a sort exclusively for function effects?

[gmhwxi]

Yes. Exclusively for function effects.

[Yannick Duchêne]

From a practical point of view, what is the difference between !wrt and !ref. Both looks the same to me, so I must be missing something.

[Hongwei Xi]

Basically,

!ref means using (reading or writing) a pointer shared with others;

!wrt means writing via a pointer owned by oneself.

Code that generates !ref is not safe in general to be used in multithreaded

programming.

--
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-users+unsubscribe@googlegroups.com.
To post to this group, send email to ats-lang-users@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/af5d5fe2-f316-4d31-a445-2bb7297b7994%40googlegroups.com.

[Yannick Duchêne]

I see, sharing is the key word which says it all.

I was also wondering if !wrt implies the function is not pure in the functional sense. A function may be pure while using memoization, so writing memory. Is this related to effect or not related? Or alternatively, do ATS cares about it? (I mean, pure in the functional sense)

[Vanessa McHale]

I usually have seen "pure" used to mean "referentially transparent," that is, given the same inputs it will always yield the same outputs. I don't think that either would qualify, though I'm not familiar enough with ATS to say definitively.

As for memoization: that can definitely be done purely, but that is not the same as writing to a pointer.

--

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/1e07d542-a035-432d-a78b-985745d2e156%40googlegroups.com.

[Hongwei Xi]

Say we define that a function is pure if its evaluation cannot affect

the evaluation of any other functions. Then a function can be pure even

if it may cause the !wrt effect.

I have to say that ATS2, as it is implemented now, does not track effects

in a sound way.

--

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-users+unsubscribe@googlegroups.com.
To post to this group, send email to ats-lang-users@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/1e07d542-a035-432d-a78b-985745d2e156%40googlegroups.com.

[Yannick Duchêne]

Yes, that’s too what I understand of pure in the functional sense.

[Yannick Duchêne]

If the intended semantic is sound, that’s not the worst.

Anyway, thanks for the notice, that’s good to know.

[Yannick Duchêne]

Le mardi 5 juin 2018 03:35:57 UTC+2, gmhwxi a écrit :

I have to say that ATS2, as it is implemented now, does not track effects

in a sound way.

Is below an example ?

        viewtypedef t = () -<clo> void

        fn f(): t = let // Does not compile, just type‑check.

           in lam@() =<0> ()  // <-- here

           end

        var g:t = f()

        val () = g()

        var h:t = lam@() => ()// <-- here

        val () = h()

In the first place marked “<-- here” , the “pure” effect needs to be specified to type check, it is not required in the second place.

[Hongwei Xi]

>>viewtypedef t = () -<clo> void

The type 't' is very special: it does not have a known size!

Such a type (like a flat array type) can only be used for call-by-reference.

>>var h:t = lam@() => ()// <-- here

'var h:t' means that the size of 'h' is that of the size of 't'.

It does NOT mean that only a value of the type 't' can be

stored in 'h'.

--
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-users+unsubscribe@googlegroups.com.
To post to this group, send email to ats-lang-users@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/19f17083-54af-49b9-9c1f-32ed6f1d6701%40googlegroups.com.

[Yannick Duchêne]

Le samedi 4 août 2018 16:38:00 UTC+2, gmhwxi a écrit :

[…]

>>var h:t = lam@() => ()// <-- here

'var h:t' means that the size of 'h' is that of the size of 't'.

It does NOT mean that only a value of the type 't' can be

stored in 'h'.

Indeed, if I do what’s below, the function effect must be set to pure:

        typedef t = () -<clo> void

        var h = (lam@() =<0> ()):t

I was not suspecting this, because when a mention to “master type” was made some times ago, I though the typing rules for initialisation, was like with `val`, and I added this a long time ago in my notes, about `val`:

> `val x = e:T`: typical of annotations, checks `e` is of type `T`.

> `val x:T = e`: checks `e` is of a subtype of `T`.

So I was surprised about `var h:t = lam@() => ()`

However, although it triggers another error, for type checking, with what is below, the function effect is required to be pure:

        val h:t = lam@() =<0> ()  // For a test only, otherwise requires to be an l‑value.

Values and variables differ more than I suspected.

I will need a deeper look at it and to review every thing with this question in mind.

[Yannick Duchêne]

Le samedi 4 août 2018 16:38:00 UTC+2, gmhwxi a écrit :

'var h:t' means that the size of 'h' is that of the size of 't'.

It does NOT mean that only a value of the type 't' can be

stored in 'h'.

To check it:

        typedef t = @{a=int}

        typedef u = @{b=int}

        var a:t = @{a=0}

        var b:u = a  // Type‑checks! Fails if `val` instead of `var`.