Effects of proofs on types as a side effect

[Yannick Duchêne]

Here is sample, what’s important is in `g` marked `<-- here`:

        staload UN = "prelude/SATS/unsafe.sats" // Prerequisite.

        viewtypedef t = () -<cloptr> int // Prerequisite.

        fn h(): t = let

           val v = 1

        in lam(): int => v end

        // `g` evaluates `f` and then frees it.

        fn g(f: &t >> t?): int = let

           val r = f()

           val _ = cloptr_free($UN.castvwtp0(f))

           prval p = view@ f  // <-- here

        in r end

        var f = h()

        val v = g(f)

The presence of `prval p = view@ f` produce a type error in `in r end`, which is not about `r`, rather about `>> t?` which is treated as something returned too.

I’m surprised this proof which does not go outside the function, can change the returned type of `f`.

I encountered other similar effects, including one without proof, this one is the simplest one.

For the anecdote, I came to this while testing if there are ways to free the cloptr without an unsafe cast.

[Hongwei Xi]

It will be okay if you put 'p' back:

          // `g` evaluates `f` and then frees it.
          fn g(f: &t >> t?): int = let
             val r = f()
             val _ = cloptr_free($UN.castvwtp0(f))
             prval p = view@ f  // <-- here

             prval () =    view@f := p
          in r end

>>val _ = cloptr_free($UN.castvwtp0(f))

The above line is safe. We just need to find a better way to name it :)

--
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-users+unsubscribe@googlegroups.com.
To post to this group, send email to ats-lang-users@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/acad14e7-3f3b-4daf-9105-78864b00034a%40googlegroups.com.

[Yannick Duchêne]

Le vendredi 3 août 2018 22:11:51 UTC+2, gmhwxi a écrit :

It will be okay if you put 'p' back:

          // `g` evaluates `f` and then frees it.
          fn g(f: &t >> t?): int = let
             val r = f()
             val _ = cloptr_free($UN.castvwtp0(f))
             prval p = view@ f  // <-- here
             prval () =    view@f := p
          in r end

So `view@` peaks something?

The `view@f := p` is what is called “view restauration”, isn’t it? That’s something I not yet investigated.

 

>>val _ = cloptr_free($UN.castvwtp0(f))

The above line is safe. We just need to find a better way to name it :)

What about just moving it out of `unsafe.sats` 

I did not knew it is safe, I will have a new look at it. Thanks for the point.

[Yannick Duchêne]

Le vendredi 3 août 2018 22:17:24 UTC+2, Yannick Duchêne a écrit :

So `view@` peaks something?

Oops, I wanted ti say “peek”  instead of “peak”

[Yannick Duchêne]

Yes, I’m silly: view@ is subject to linear logic. 

[Hongwei Xi]

view@f refers to the linear proof (of some at-view)

attached to 'f'. Note that view@f is a left-value.

>>What about just moving it out of `unsafe.sats`

Then we have to find a typing rule for doing it. We should

do this safely in ATS3.

--

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-users+unsubscribe@googlegroups.com.
To post to this group, send email to ats-lang-users@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/1ffee64c-fcfa-473c-98cd-a2d28b60c8d0%40googlegroups.com.

[Yannick Duchêne]

Le vendredi 3 août 2018 22:33:59 UTC+2, gmhwxi a écrit :

Then we have to find a typing rule for doing it. We should

do this safely in ATS3.

Sometime I wonder how far or how close ATS3 will be to ATS2. Anyway, ATS2 will be there for some time, at the least for the time of a complete transition. 

[Hongwei Xi]

Here is what I have in mind at this moment:

ATS3 = ATS2 + meta-programming

Type inference plays a big role to provide support for meta-programming.

--

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-users+unsubscribe@googlegroups.com.
To post to this group, send email to ats-lang-users@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/b5c30994-725b-4214-9780-cbe1c19972d7%40googlegroups.com.

[Yannick Duchêne]

Le samedi 4 août 2018 16:43:28 UTC+2, gmhwxi a écrit :

Here is what I have in mind at this moment:

ATS3 = ATS2 + meta-programming

Type inference plays a big role to provide support for meta-programming.

That’s fine :)