A couple of basic questions (for me and the wiki)

  1. val vs var with dependent types
    Why is ok to “get” some dependent type info this way:
    val [n:int] ptmp = mystr1_of_mystr(strtmp)
    but not this way:
    val _ = p->size := (p->size - p->pos + 1)

  2. Stack allocation
    val tmp = 1
    val tmp = 2
    // Internally, is it now the case that we have allocated two integers in
    memory on the stack?

  3. Possibly more to come soon …

For 1) I’m sorry, I had a typo I didn’t correct in the email. It should be:

// This is ok:
val [n:int] ptmp = mystr1_of_mystr(strtmp)
// but not this
val _ = [n:int] p->data := mystr1_of_mystr(strtmp)

I suppose an acceptable approach is to write a prffun to get info about
dependent information.

For 2) then, is there any case where one could get in to memory efficiency
trouble by performing multiple bindings to the same name?

‘[n:int] ptmp’ is a pattern.

[n:int] p->data := mystr1_of_mystr(strtmp)

It is not that this cannot be supported. However, adding new syntactic
features like this is quite involved (given the already very rich and
complex syntax of ATS).

is there any case where one could get in to memory efficiency trouble by
performing multiple bindings to the same name?

It is conceivable but highly unlikely in my opinion as the underlying
compiler optimization is straightforward to implement.

  1. I don’t understand the question.
  2. It depends on the actually compilation. In this case, none is allocated
    due to constant propagation.