Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[ elab ] Make %runElab expressions have unrestricted quantity #2021

Open
wants to merge 1 commit into
base: main
Choose a base branch
from

Conversation

buzden
Copy link
Contributor

@buzden buzden commented Oct 17, 2021

According to #1436, we can't have a runtime-values of types like forall a. List a -> Nat. But consider we need to pass a list of types including one like above to an elaboration script. Now we don't have such an ability. This PR enables it.

Anyway, elaboration scripts work during compilation, why not them to have an access to erased values?

Copy link
Member

@gallais gallais left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What happens if you write an elab script that returns \x => x at type (0 _ : a) -> a?
Are you able to use it to implement

escape : (0 _ : a) -> a
escape = %runElab myscript

?

@buzden
Copy link
Contributor Author

buzden commented Oct 18, 2021

What happens if you write an elab script that returns \x => x at type (0 _ : a) -> a? Are you able to use it to implement

escape : (0 _ : a) -> a
escape = %runElab myscript

?

No! I've changed rig of input of %runElab, not of its result.


This code

escScr : Elab $ (0 _ : a) -> a
escScr = check $ ILam EmptyFC M0 ExplicitArg (Just `{x}) `(a) `(x)

esc : (0 _ : a) -> a
esc = %runElab escScr

expectedly gives an error:

Error: While processing right hand side of esc. x is not accessible in this context.

RunElab0:19:65--19:66
 17 |
 18 | escScr : Elab $ (0 _ : a) -> a
 19 | escScr = check $ ILam EmptyFC M0 ExplicitArg (Just `{x}) `(a) `(x)
                                                                      ^

And even declaration like

escDecl : Name -> Elab Unit
escDecl name = declare [                                              
                 IDef EmptyFC name [                   
                   PatClause EmptyFC
                     -- lhs
                     (IApp EmptyFC (IVar EmptyFC name) (IBindVar EmptyFC "x"))
                     -- rhs
                     `(x)
                 ]  
               ] 

%runElab escDecl `{esc}

expectedly fails with

Error: While processing right hand side of esc. x is not accessible in this context.

RunElab0:31:24--31:25
 27 |                    PatClause EmptyFC
 28 |                      -- lhs
 29 |                      (IApp EmptyFC (IVar EmptyFC name) (IBindVar EmptyFC "x"))
 30 |                      -- rhs
 31 |                      `(x)
                             ^

while expectedly typechecking for

0 esc' : (0 _ : a) -> a

%runElab escDecl `{esc'}

I can add those above as an additional test case.

@buzden buzden force-pushed the fix-rig-for-runelab-expr branch from 1f45f78 to 76f3b3b Compare October 18, 2021 20:03
@buzden
Copy link
Contributor Author

buzden commented Oct 19, 2021

I disagree that bringing erased values to non-erased context should be impossible for elaboration scripts. Moreover, they should sometimes do this in some sence: consider an elaboration script for derivation of default Show implementations: it brings constructor names to runtime, this is bringing erased (in some sence) values to the runtime.

That's why I think your test that expects "escaping" to fail, should not pass. The fact that it passes looks like a bug to me. Moreover, I ran into similar bug when during quoting instead of passed value a part of elaboration script was quoted. But for now I didn't manage to make a minimal example showing this for reporting as an issue. This bug seems to appear when %runElab is used for expressions and does not appear when it's used for declarations.

Anyway, this bug is irrelevant to this PR.

@andrevidela
Copy link
Collaborator

andrevidela commented Nov 2, 2021

@buzden I'm not sure what you are replying to but I think I can bring in some intuition about what is happening with erased quantities. Especially your statement

bringing erased values to non-erased context should be [allowed] for elaboration scripts.

erased means the value never appears at runtime, that also means that it should be allowed to be used at compile-time just fine. Since elaborator scripts are executing at compile time it feels natural to expect them to have access to erased multiplicity values. However, the values they have access to cannot be part of computations that appear at runtime. Think of the following example:

0 erased : String
erased = "Ikari"

computeOrder: String -> String
computeOrder = "Get in the robot " ++

main : IO ()
main = putStrLn (computerOrder erased)

you wouldn't expect this program to typecheck, but you would expect the following to work

main : IO ()
main = putStrLn (computerOrder "Shinji")

The only difference between those two programs is that we have inlined the call to erased in the second one. How is this related to elaboration? it's because this kind of operation can be done with elaborator reflection since it just takes a tree and returns another tree. This puts us in either of two positions:

  • The program transformation from the first program to the second one is legal, elaboration should have access to erased values, and the linearity checker is wrong to make n inaccessible
  • The program transformation is incorrect, elaboration should not have access to erased values, linearity checker is correct to avoid leaking erased values

Like every complex issue, the real answer is "it depends", what this tree operation represents is "a program that is executable at compile type but might result in a different runtime representation". Because the runtime representation is changed the multiplicty cannot be 0 but because it's accessible exclusively at compile-time, it should be allowed to be 0-ish. So we are looking at a different kind of resource tracking if we want to make this property explicit, one that can describe "compile-time only" operations but can have an effect on the runtime.

TBD if something like that ever shows up (I'm working on it but I have also lots of other things going on :)). In the meantime, making n inaccessible makes it consistent with the rest of the design around quantities, that is: erased values never leak into the runtime

PS: If you want the explanation without runtime/compile time intuition, page 3 of the QTT paper, the App rule makes it clear that you can never have anything be 0 and not have either the function be marked as 0 or it's argument be marked as 0 due to σ ′ = 0 ⇔ (π = 0 ∨ σ = 0)

@buzden
Copy link
Contributor Author

buzden commented Nov 2, 2021

@andrevidela Thank you for the detailed elaboration on this. Let me just clarify that my original sentence had the meaning that I personally agree with the first position you list, i.e. I personally think that

  • The program transformation from the first program to the second one is legal, elaboration should have access to erased values, and the linearity checker is wrong to make n inaccessible

Now I see that there is another opinion, it was not obvious. I thought of erased values not as those which are prohibited to be at runtime, but as those which by default are not present at runtime (but could if something forces this).

After your brought both options explicitly, I've thought that maybe we need two kinds of elaboration scripts, of "safe" and "unsafe" flavours, one being unable to bring erased values to runtime, the other being able to do so. The problem is amplified by the fact that elaboration scripts can produce values that are meant to be present only at runtime, as it's shown in #2088.

My mistake was to start this discussion in this PR because this PR does not change what is accessed to elaboration script during %runElab. This PR only makes us able to have elaboration script values to be erased.

@gallais
Copy link
Member

gallais commented Nov 2, 2021

I think this change blurs / is due to a blurring of the line between erased values and staging.
I'm not comfortable making a decision on this. I guess we could ask @edwinb to weigh in.

@andrevidela
Copy link
Collaborator

Sorry for the late reply, in my experience with QTT and different semantics for quantity semirings there is a clear distinction between staging semantics and use semantics. It is true that the waters are muddied for things like elaborator reflection but what this indicates is that more research is needed in order to make things work correctly.

@buzden I suggest we talk about this on discord, I have a lot of work in progress in this area and we can probably find a middle ground between what we need to provide as a toolkit and what is an acceptable feature in terms of type safety

@buzden buzden force-pushed the fix-rig-for-runelab-expr branch 2 times, most recently from 3ae7ce0 to 2d3a97f Compare November 8, 2021 13:04
@buzden buzden force-pushed the fix-rig-for-runelab-expr branch from 2d3a97f to 297ca96 Compare November 23, 2021 18:24
@gallais gallais force-pushed the main branch 2 times, most recently from 20718fd to 2c9bf24 Compare February 3, 2022 18:41
@buzden buzden force-pushed the fix-rig-for-runelab-expr branch from 297ca96 to deee51f Compare January 13, 2023 19:38
@buzden buzden force-pushed the fix-rig-for-runelab-expr branch from deee51f to c1dbf8a Compare March 22, 2023 19:39
@gallais
Copy link
Member

gallais commented Aug 1, 2023

Okay I think I have come around to this. Particularly because quote already has type:

quote : (0 _ : val) -> m TTImp

Once the merge conflict has fixed I am happy to merge it.

@buzden buzden force-pushed the fix-rig-for-runelab-expr branch 2 times, most recently from bfc90b4 to 10f3237 Compare August 1, 2023 13:07
@gallais gallais assigned gallais and unassigned gallais Aug 10, 2023
@gallais
Copy link
Member

gallais commented Aug 10, 2023

I tried to fix the evaluation issue we are getting in elab-util
but could not find the issue. :/

@buzden
Copy link
Contributor Author

buzden commented Aug 10, 2023

but could not find the issue. :/

What do you mean? Do you mean you didn't find the cause?

A couple of experiments from me: I changed existing bot to top in ProcessRunElab and it suddenly did not change anything (the original cause was changing ElabMode from InExpr to InType, but it seems that the reason is different anyway).

Then I added every namespace from allImported to nestedNS like here and suddenly errors changed: the original script that did not reduce to Elab did this, but after that I had the following errors (I haven't worked them out yet).

@buzden buzden force-pushed the fix-rig-for-runelab-expr branch from 10f3237 to dfe6f0e Compare August 10, 2023 13:25
@gallais
Copy link
Member

gallais commented Aug 10, 2023

Sorry, my wording was poor: I could not find a fix for the build issue.

@buzden
Copy link
Contributor Author

buzden commented Aug 13, 2023

Fresh news! I found out that this non-reducing behaviour happens only in failing block and only when quantity is omega (i.e., it works not only for 0, but for 1 too). @gallais, as an author of the failing block checks, can this information give you any clue on what's going on?

Oh, and I added a shorter test that shows the strange behaviour of elab-util failing as reflection022.
UPD: sorry, reflection022 is not very correct yet (it reveals another bug), I need to rework it a bit. But information above is still valid.

@gallais
Copy link
Member

gallais commented Aug 14, 2023

Very interesting. The main code for the typechecking phase is in processFailing in
TTImp.ProcessDecls.

Could it be that a hole was delayed and we hit it in checkDelayedHoles?
Should we instead try to rerun the delayed problems in case they're now solvable?

@buzden
Copy link
Contributor Author

buzden commented Aug 14, 2023

Could it be that a hole was delayed and we hit it in checkDelayedHoles?

Once I allowed typechecker to see all imports publicly and I indeed got ?delayed instead of the whole elaboration script (but that was not under the failing block): https://github.com/buzden/Idris2/actions/runs/5820206080/job/15781485413#step:5:52

@buzden buzden force-pushed the fix-rig-for-runelab-expr branch from e79afbc to 491629c Compare September 15, 2023 09:12
@buzden buzden force-pushed the fix-rig-for-runelab-expr branch 3 times, most recently from de82e35 to 759f227 Compare December 30, 2023 00:02
@buzden buzden force-pushed the fix-rig-for-runelab-expr branch from 759f227 to 584eb1e Compare January 31, 2024 13:02
@buzden buzden force-pushed the fix-rig-for-runelab-expr branch from 584eb1e to 3a2c41c Compare May 31, 2024 11:12
@buzden
Copy link
Contributor Author

buzden commented Jun 5, 2024

Just for a record: the reason of this quantity-related behaviour of underreduction is found by @AlgebraicWolf, but it is not obvious how to make all this work without reducing too much. The problem and directions of solution have been discussed on the latest weekly meeting in Discord, and are investigated at the moment.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants