Optional values in ATS

[gmhwxi]

ATS is a very rich programming language.

The datatype for optional values can be defined as follows:

datatype option (a:t@ype+) = Some of a | None of ()

Say we want to implement a function that returns the head of a given list:

fun{a:t0p}
list0_get_head (xs: list0 (a)): Option (a) =
  case+ xs of
  | list0_cons (x, _) => Some{a} (x) | list0_nil () => None ()

There is really no surprise here. The problem with optional values is that
they are heap-allocated and GC is needed to reclaim the memory they occupy.
If you do embedded programming, then you probably do not want to use them.

The following type is for linear optional values:

datavtype option_vt (a:vt@ype+) = Some_vt of a | None_vt of ()

Now the list0_get_head function can be implemented as follows:

fun{a:t0p}
list0_get_head (xs: list0 (a)): Option_vt (a) =
  case+ xs of
  | list0_cons (x, _) => Some_vt{a} (x) | list0_nil () => None_vt ()

Linear optional values are heap-allocated but they can be safely freed manually
(with no need for GC).

There is another version of optional values that are stack-allocated:

fun{a:t0p}
list0_get_head (xs: list0 (a), res: &a? >> opt(a, b)): #[b:bool] bool (b) =
  case+ xs of
  | list0_cons (x, _) => let
      val () = res := x
      prval () = opt_some{a}(res)
    in
      true
    end
  | list0_nil () => let
      prval () = opt_none{a}(res)
   in
      false
   end

Essentially, we have

opt (a, true) = a and opt (a, false) = a?

This is what I call safe C-style programming. The return value indicates
whether a valid value is stored in the call-by-reference argument [res]. There
is no safe way to use the value stored in [res] without first checking that the
returned boolean value is true.

There are plenty functions in libats that use 'opt'.

[Yannick Duchêne]

I'm exactly interested in this, and unfortunately, I feel I will have a hard time trying to understand and use this (red-face)

Where do I learn about `?` and `>>` and `&` and `#`? I remember I've seen `&` about linear types (in the docs), but not the others.

Is it required to use this?

Why is the datatype necessarily heap allocated? Why is the version with `opt`, stack allocated? Is this a consequence of the way they are each declared?

What about something like this:

sortdef reference = int
typedef reference = [r: reference] int(r)
typedef reference(r: reference) = int(r)
abstype element

stacst not_null(r: reference): bool
extern fun element{r: reference | not_null(r)}(r: reference r): element

Except for now I don't now how to use `t@ype` instead of `int` (which is really not what was intended) and i don't know where to define `not_null` (ATS don't want me to declare it as `extern`), do this form looks like something feasible?

[Yannick Duchêne]

Le jeudi 14 mai 2015 02:36:54 UTC+2, Yannick Duchêne a écrit :

[…] and i don't know where to define `not_null` (ATS don't want me to declare it as `extern`), […]

I'm unlucky with this one too:

stacst not_null(r: reference): bool
extern fun not_null(r: reference): [b:bool | b == not_null(r)] bool(b)

 It complains about a file_mode :-(

 

[Hongwei Xi]

extern fun not_null(r: reference): [b:bool | b == not_null(r)] bool(b)

The [r] in not_null(r) is unbound.

--
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 http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/73dd2c7e-accd-4648-ba12-8dd03db7c653%40googlegroups.com.

[Yannick Duchêne]

Le jeudi 14 mai 2015 03:15:41 UTC+2, gmhwxi a écrit :

extern fun not_null(r: reference): [b:bool | b == not_null(r)] bool(b)

The [r] in not_null(r) is unbound.

I figured it out later.

I came with another template:

sortdef reference = int
typedef reference = [r: reference] int(r)
typedef reference(r: reference) = int(r)

abstype element

stacst not_null(r: reference): bool
extern fun {q: reference} not_null(r: reference q): [b:bool | b == not_null(q)] bool(b)

extern fun element{r: reference | not_null(r)}(r: reference r): element

extern fun reference(k: string): reference

val r: reference = reference("foo")
val b: bool = not_null(r)
val () =
  if b then
    let val e: element = element(r)
    in () end

 

[gmhwxi]

If I understand you correctly, then I think what you
want to do is essentially like 'opt'.

opt(T, true) = T
opt(T, false) = T? // T? means uninitialized T

fun element (opt(T, true)): T // element is just identity

[Yannick Duchêne]

Le jeudi 14 mai 2015 03:52:28 UTC+2, gmhwxi a écrit :

If I understand you correctly, then I think what you
want to do is essentially like 'opt'.

Yes.

 

opt(T, true) = T
opt(T, false) = T? // T? means uninitialized T

fun element (opt(T, true)): T // element is just identity

 

Apart of the operators introduced here I don't (yet) understand, I have a strange feeling about “uninitialized”. What's the type of ``T?'' ?

[Hongwei Xi]

For every type T, T? is a type whose size is the same as T.

A value of the type T? can be any sequence of bytes occupying

a piece of memory of the size sizeof(T?).

--
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 http://groups.google.com/group/ats-lang-users.

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/83d4c71b-c1ad-41d4-bd15-2240a79c196c%40googlegroups.com.

[Yannick Duchêne]

Le jeudi 14 mai 2015 04:17:24 UTC+2, gmhwxi a écrit :

For every type T, T? is a type whose size is the same as T.

A value of the type T? can be any sequence of bytes occupying

a piece of memory of the size sizeof(T?).

So that's close to what I felt to guess.

I like the way `opt` is, it is close to an idiom I often have with Python, when I return a tuple of a value and a boolean, with a value which may be null of unterminated (which may still be useful for reporting) when the boolean is False.

On the other hand, I would like to have the option prevent any access to T when the boolean is false. That's why I asked about the type of T?

The size in bytes will not be relevant for JavaScript, but I understand with other target it means uninitialized bytes, and that's why preventing any access to it is important.

That's better to use the same idiom for a language like JavaScript, which does not know about size/memory representation and a language which do, like C.

I hope the template I posted does not too much looks like “garbage” in this thread.

I will investigate `opt` and `T?` or similar.

[gmhwxi]

>>I like the way `opt` is, it is close to an idiom I often have with Python, when I return a tuple of a value and a boolean, with a value which may be null of unterminated (which may still be useful for reporting) when the boolean is False.

Yes, programmers often design their own "type system" when programming in
a language like Python. Before switching to ML, I did something close to ad-hoc
typechecking when programming in LISP.