Make {Us,,S}Progs more uniform

[davidweichiang]

With @HerbertMcSnout's blessing to go ahead with more cleanups, here's a set of changes that makes {Us,,S}Progs more consistent with one another and with Ctxt, possibly paving the way to unifying some of them.

There used to be several cases that stored argument types and result types separately (instead of as a TpArr). Removing these simplified the code in many places, but complexified it in some others, especially AffLin, which was using this fact to pass over top-level arrows (cf. #87).

[ccshan]

I think git(hub) is confused about squashed commits? And doesn't realize that 5916b720a39d53169aa10c6219ffd256bc5d76dd is included in c3283f13ba5db2cd2a87c064231d88bf61a8236f?

[davidweichiang]

Yes, this is a really annoying thing about squash merges. Sorry about that.

[davidweichiang]

I'm sure there must be a way to rebase to hide those commits, but every time I have tried, it has never ended well.

[davidweichiang]

The logic that used to be in argifyProg, which checked when a define's body had fewer lambdas than its type had arrows, was deleted and needs to be put back.

I can think of three options:

1. Restore this logic to argifyProg by rolling this PR back to just commit https://github.com/diprism/perpl/pull/94/commits/c409d5ad6ec904db3a2106212532a353d7ef5d2c (eliminate Scheme). Maybe even change ProgExtern to have separate argument and return types as well. There's a nice symmetry in having ProgFun, ProgData, TmVarG, and TpData all have a list of arguments.
2. Move this logic to both affLinProg and prog2fgg. I think what this would look like is a fancier version of splitLams that also looks at the type to figure out how many lambdas there should be.
3. Do (2) and furthermore move the logic in argify (TmApp...) to happen on the fly in both affLin and term2fgg (using a fancier version of splitApps). I think this means that Argify would just go away.

[ccshan]

I understand the original motivation of Argify is to help AffLin handled curried global functions so that a <,()> level doesn't need to be introduced for each lambda level. This has to look at the lambdas in the term, not the arrows in the type, because define f = \x. factor 2 in \y. ... is different from define f = \x. \y. factor 2 in ... in terms of what happens when f is applied just to True then discarded. Someone "fancier" who looks at the type Bool->Bool->Bool and decides there should be 2 lambdas can't transform the former definition of f to the latter. (Similarly, define f = factor 2 in \x. \y. ... is yet different in terms of what happens when let g = f in discard g.)

Given that this is an impure language, it would be reasonable for us to encourage uncurried functions (e.g., by changing example programs, and by allowing \(x,y). ... in syntax) and reduce the need for Argify. But ProgFun still needs to have at least one argument, to optimize away the top level of <,()> due to the parenthesized sentence at the end of the last paragraph.

I'm reminded of https://www.microsoft.com/en-us/research/publication/make-fast-curry-pushenter-vs-evalapply/ but I haven't read it for a while...

[ccshan]

Remind me, can we just disallow nonuse of functions and additive tuples, and make the automatic introduction of recursive discard functions the only job of AffLin?

[davidweichiang]

Remind me, can we just disallow nonuse of functions and additive tuples, and make the automatic introduction of recursive discard functions the only job of AffLin?

I'm not understanding this question...do you mean you want the programmer to write calls to discard but not have to implement discard?

[ccshan]

Remind me, can we just disallow nonuse of functions and additive tuples, and make the automatic introduction of recursive discard functions the only job of AffLin?

I'm not understanding this question...do you mean you want the programmer to write calls to discard but not have to implement discard?

No, I mean suppose we simply require linear use of any type containing arrow or additive tuple. But we allow nonlinear use of a type even if it contains recursion. So the transformation would leave types unchanged, and merely insert discard (and copy?) calls as needed. Would that be convenient for the programmer?

[davidweichiang]

The bugs pointed out above should be fixed now (by implementing fix 2). However, it's still worth discussing whether 1 or 3 are better solutions.

[davidweichiang]

This is a dead end unless some other major change is made, in which case the merge would probably be a mess! Closing.