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
Den lördag 25 april 2020 kl. 21:34:57 UTC+2 skrev 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
>
>
> On Friday, April 24, 2020 at 3:52:39 PM UTC-4, August Alm wrote:
>>
>> 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/950bb533-a1ff-407f-887b-75316b3e00b9%40googlegroups.com.
