Open leifhelm opened 1 year ago
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.
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*))
Yes, something like that.
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 inlist_vt
.I came up with the following solutions:
Solution 1
If I understand correctly a
_unfold
type corresponds to adatconptr
(void*
in C) that points to a struct which corresponds to the constructor. For example forlist_vt
list_vt_cons_unfold(l0, l1, l2)
points to a struct oft@ype
andptr
. So wouldn't it be sensible to be allowed to access these variables given the corresponding proofs exist (e.g.a@l1
orptr?@l2
).For example tuple accessor syntax could be used to inspect a partially broken
_unfold
type.0
could be the base pointer tol0
and the rest to the fields of the struct.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:So for example there could be function
list_vt_cons_pstruct
that turns alist_vt_cons_unfold
and the proofs into alist_vt_cons_pstruct
.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 theinsord
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 ofp
should bet@ype
or something else. Implementation oftakeout_node_at
: