is ptr_get0 from introduction implementable.

[Scott Murphy]

Hello!

I am skipping around the introduction to ats book and am having fun.

I keep getting stuck on this though from the book:

fun{a:t@ype}
ptr_get0 {l:addr} (pf: a @ l | p: ptr l): (a @ l | a)

From http://ats-lang.github.io/DOCUMENT/INT2PROGINATS/HTML/INT2PROGINATS-BOOK-onechunk.html#introduction-to-views-and-viewtypes

I have tried thinking of how to implement this and can't seem to get it right.

I have tried using the implentation of ptr_get from prelude

SATS:

fun{a:vt0p}
ptr_get{l:addr}
  (pf: !INV(a) @ l >> a?! @ l | p: ptr l):<> a

DATS:

implement
{a}(*tmp*)
ptr_get(pf | p) = !p

Obviously those type signatures are different!

Is the ptr_get0 from the introduction implementable? 

If so could someone show me an example implementation?

Thanks!

[Richard]

Not sure if this is completely correct however, it typechecks

extern fun {a:t@ype}

ptr_get0 {l:addr} (pf: a @ l | p: ptr l): (a @ l | a)

implement {a} ptr_get0 {l} (pf | p) = (pf | A) where { val A = !p }

[Scott Murphy]

Thank you so much.

So the binding with val A is what forces pf to be considered

consumed.

I have tried:

fun{a:t@ype}
ptr_get0 {l:addr} (pf: a @ l | p: ptr l): (a @ l | a) = (pf|!p)

and seen the consumption error so many times but wasn't sure exactly what consumption meant!

[Hongwei Xi]

>>(pf | !p)

This does not work because type-checking is performed from

left to right. So you need

let val x = !p in (pf | x) end

--
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 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/9689d6a2-2dfb-4110-b8e1-c8e616b35696%40googlegroups.com.

[Scott Murphy]

Okay so binding has nothing to do with proof consumption then? 

Maybe I understand now lol.

[Hongwei Xi]

Not sure if I understand your question.

When constructing (pf | !p), 'pf' is kept and then !p could no longer find the view it needs

in order to fetch the data. So the data needs to be fetched first: let val x = !p in (pf | x)

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/3f188543-4655-42ca-8696-bb371641172f%40googlegroups.com.

[Scott Murphy]

What is meant by kept?

[Hongwei Xi]

'kept' : pf is held by the type-checker and no longer available when '!p'  is type-checked.

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/b6c63a79-458e-4e3a-b981-e2adbae17819%40googlegroups.com.

[Scott Murphy]

thank you!