Initialisation of a record

[Arets Paeglis]

Hi,

Assuming we have a record and its supporting definitions as follows,

abst@ype RT(int) = int
stadef Any = 0

typedef M = @{
    rt = {a: int} RT(a)
}

what is the proper way of initialising a value of type M? Doing 

val m = @{ rt = RT(Any) } : M

fails with error(2): the dynamic identifier [ReturnType] is unrecognized.

What am I doing wrong? Thanks in advance.

[gmhwxi]

{a:int} means universal quantification.
What you need is probably existential quantification:

[Arets Paeglis]

You're correct, although that didn't solve the issue itself (type
checking still fails with the same error).

Arets Paeglis
about.me/mindbound

> --
> You received this message because you are subscribed to a topic in the
> Google Groups "ats-lang-users" group.
> To unsubscribe from this topic, visit
> https://groups.google.com/d/topic/ats-lang-users/FnZmnzd6X38/unsubscribe.
> To unsubscribe from this group and all its topics, send an email to
> ats-lang-user...@googlegroups.com.
> To post to this group, send email to ats-lan...@googlegroups.com.
> Visit this group at https://groups.google.com/group/ats-lang-users.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/ats-lang-users/1a501552-85cd-45a8-81bc-07b2886df97e%40googlegroups.com.

[gmhwxi]

RT(Any) is a type (not a value).

You need something like:

extern
fun RT_of_int : {n:int} int(n) -> RT(n)

val m = @{ rt = RT_of_int(0) } : M

On Tuesday, October 18, 2016 at 11:03:31 PM UTC-4, Arets Paeglis wrote:

You're correct, although that didn't solve the issue itself (type
checking still fails with the same error).

Arets Paeglis
about.me/mindbound

On Wed, Oct 19, 2016 at 5:47 AM, gmhwxi <...> wrote:
>
> {a:int} means universal quantification.
> What you need is probably existential quantification:
>
>
> typedef M = @{
>    rt = [a:int] RT(a)
> }
>
>
>
> On Tuesday, October 18, 2016 at 10:44:11 PM UTC-4, Arets Paeglis wrote:
>>
>> Hi,
>>
>> Assuming we have a record and its supporting definitions as follows,
>> abst@ype RT(int) = int
>> stadef Any = 0
>>
>> typedef M = @{
>>     rt = {a: int} RT(a)
>> }
>>
>> what is the proper way of initialising a value of type M? Doing
>>
>> val m = @{ rt = RT(Any) } : M
>>
>> fails with error(2): the dynamic identifier [ReturnType] is unrecognized.
>>
>> What am I doing wrong? Thanks in advance.
>
> --
> You received this message because you are subscribed to a topic in the
> Google Groups "ats-lang-users" group.
> To unsubscribe from this topic, visit
> https://groups.google.com/d/topic/ats-lang-users/FnZmnzd6X38/unsubscribe.
> To unsubscribe from this group and all its topics, send an email to

> ats-lang-users+unsubscribe@googlegroups.com.
> To post to this group, send email to ats-lang-users@googlegroups.com.

[Arets Paeglis]

Thanks! That solves that.

Arets Paeglis
about.me/mindbound

>> > ats-lang-user...@googlegroups.com.
>> > To post to this group, send email to ats-lan...@googlegroups.com.

>> > Visit this group at https://groups.google.com/group/ats-lang-users.
>> > To view this discussion on the web visit
>> >
>> > https://groups.google.com/d/msgid/ats-lang-users/1a501552-85cd-45a8-81bc-07b2886df97e%40googlegroups.com.
>

> --
> You received this message because you are subscribed to a topic in the
> Google Groups "ats-lang-users" group.
> To unsubscribe from this topic, visit
> https://groups.google.com/d/topic/ats-lang-users/FnZmnzd6X38/unsubscribe.
> To unsubscribe from this group and all its topics, send an email to

> ats-lang-user...@googlegroups.com.
> To post to this group, send email to ats-lan...@googlegroups.com.

> Visit this group at https://groups.google.com/group/ats-lang-users.
> To view this discussion on the web visit

> https://groups.google.com/d/msgid/ats-lang-users/36f413ec-7575-4d2a-9817-ac45d08eaabd%40googlegroups.com.