At-views and isomorphisms

[August Alm]

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

[gmhwxi]

Yes, we should support:

If T1 <= T2 then T1@l <= T2@L

There is a subtyping relation <= on types.

T1 <= T2 means that T1 is a subtype of T2, which

means a value of T1 can be treated as a value of T2.

The safe cast function can be declared as:

castfn cast_safe (pf: T1 <= T2 | x: T1): T2

For each type constructor, there should be a corresponding

subtyping rule.

However, constructing subtyping proofs is very tedious and should

be automated. In ATS2, casting is unsafe as no proof is required.

By the way, the various g0ofg1/g1ofg0 functions are just hacks. I have

removed these functions in ATS3. Such functions are needed in ATS2

primarily for the sake of selecting template implementations based on

(dependent) types. In ATS3. template selection is based on the erasures

of dependent types, which are algebraic (that is, no quantifiers are involved).

More later.

Cheers!

--Hongwei

[August Alm]

Hi,

Thank you for answering! It clarified the issue.

Right, I often find myself reaching for the non-dependent

incarnations of types when dealing with templates. The

less-than-smooth interplay between dependent types and

templates is my main source of errors. I've learnt some

work-arounds, like using abstract types, but it I still stumble

with it. So, I'm very much looking forward to ATS3! =)

Best wishes,

August