Expose fields of _unfold dataviewtype

[leifhelm]

I read your book "Introduction to Programming in ATS" and I wondered if there is a way to not use a unsafe cast in the takeout_node_at function in the section about Quicksort in list_vt.

I came up with the following solutions:

Solution 1

If I understand correctly a _unfold type corresponds to a datconptr (void* in C) that points to a struct which corresponds to the constructor. For example for list_vt list_vt_cons_unfold(l0, l1, l2) points to a struct of t@ype and ptr. So wouldn't it be sensible to be allowed to access these variables given the corresponding proofs exist (e.g. a@l1 or ptr?@l2).

For example tuple accessor syntax could be used to inspect a partially broken _unfold type. 0 could be the base pointer to l0 and the rest to the fields of the struct.

fun{a:t@ype} set_tail{n:nat}{l0,l1,l2:addr}
    (pf1: a@l1, pf2: ptr?@l2 | xs: list_vt_cons_unfold(l0, l1, l2), tail: list_vt(a, n)): list_vt(a, n+1) = let
  val () = !(xs.2) := tail
  prval () = fold@ xs
in xs end

Pattern matching could also be used to realize this feature. Maybe even a combination of both.

Solution 2

It seems to me that _pstruct is just a _unfold bundled with the appropriate proofs like demonstrated in this viewtype:

vtypedef list_vt_cons_pstruct(a:t@ype, p:type) = [l0,l1,l2:addr] (a@l1, p@l2 | list_vt_cons_unfold(l0, l1, l2))

So for example there could be function list_vt_cons_pstruct that turns a list_vt_cons_unfold and the proofs into a list_vt_cons_pstruct.

fun{a:t@ype, p:type} list_vt_cons_pstruct{l0,l1,l2:addr}
  (pf1: a@l1, pf2: p@l2 | xs: list_vt_cons_unfold(l0, l1, l2)): list_vt_cons_pstruct(a, p)

Runtime wise this is the identity function so it should have no penalty.
This approach would also eliminate the passing around of additional pointers when using an _unfold type as one could just create a _pstruct type. (For example in the insord function from insertion sort). This would eliminate the data duplication that is common practice now when using _unfold plus a bunch of pointers as all information is available from the base pointer.
I am a beginner in ATS so maybe the type of p should be t@ype or something else.
Implementation of takeout_node_at:

fun{a:t@ype} takeout_node_at{n:int}{k:nat | k < n} .<k>.
  (xs: &list_vt(a, n) >> list_vt(a, n-1), k: int k) : list_vt_cons_pstruct(a, ptr?) =
if k > 0 then let
    val+ @list_vt_cons(x, xs1) = xs
    val res = takeout_node_at<a>(xs1, k-1)
    prval () = fold@ (xs)
  in res end
else let
    val+ @list_vt_cons(x, xs1) = xs
    val nx = xs
    val () = xs := xs1
  in
    list_vt_cons_pstruct(view@x, view@xs1 | nx)
  end

[githwxi]

Yes, you are right. The unsafe cast in my code can be replaced with safe code. Both of your solutions should work. What I would really like to support is a way to do it automatically. A big issue with ATS is that it imposes too much of a burden on the programmer for writing safe and efficient code.

[leifhelm]

Do you mean something like a safe cast where the compiler looks for the proofs itself:

val xs = cast@{list_vt_cons_pstruct(a, ptr?)}(nx (*list_vt_cons_unfold*))

[githwxi]

Yes, something like that.