Hi!
Jumping straight to it, consider the following types
(here [a: t0ype+], say):
node0_t(a) = @{entry = a, next = ptr}
and
node1_t(a) = [l: addr] @{entry = a, next = ptr(l)}
Using the pure cast-functions [g1ofg0_ptr] and
[g0ofg1_ptr] I can write down corresponding pure
functions [g1ofg0_node] and [g0ofg1_node] to pass
back and forth between the two types. However, say
I'd like to define something like singly linked lists
(or segments) using views and introduce the view
node_v(a, l, l_next) =
@{entry = a, next = ptr(l_next)} @ l
In light of the equivalence of [node0_t(a)] and
[node1_t(a)], there should be a corresponding way
to pass between the view
node0_t(a) @ l
and
[l_next: addr] node_v(a, l, l_next)
My concrete question is: Is there a way to do so
without brute-forcing it with an "extern prfun" (left
without implementation)?
More generally, if [a1] and [a2] are "equal", then the
views [a1 @ l] and [a2 @ l] should be "equal". I know
equality of types is very tricky business but at least
in the case above it should somehow be enforced, I
think. There are many such cases is ATS, where we
have a non-dependent incarnation and a dependently
typed incarnation of the "same" type.
ptr vs [l: addr] ptr(l)
int vs [n: int] int(n),
list(a) vs [n: nat] list(a, n),
and so on.
[g0ofg1] and [g1ofg0] are overloaded to cover most
of these. But for translating between the corresponding
at-views?
Best wishes,
August
--
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 [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/a8d31e62-315e-4fe3-a22c-fb0f1a874f0f%40googlegroups.com.
