Uniquify all Sprite preterms in [Chk-Lam]

[shingarov]

Here is another attempt at resolving #139.
Introducing λ-abstractions may result in disastrous name capture, as #testAlphaClash demonstrates.
This proposed fix uniquifies all λ-abstractions at [Chk-Lam] time.

[janvrany]

I need bit more time to have a closer look, but 2 nitpicks:

• why some #rename:to: use ^self class ... and other refer to class directly? See for instance EFun >> rename:to: and EIf >> rename:to:
• In Smalltalk/X codebase there's a convention of using ^ self subclassResponsibility (note the return) when method is supposed to return some useful value. If it is "procedure" (in Pascal sense), there's no return. I find this useful.

Will have a closer look tomorrow, but so far I like it.

[shingarov]

why some #rename:to: use ^self class ... and other refer to class directly?

This is an artefact of monkey-copying from upstream, searching for a compromise between maximizing similarity with the upstream (in case we need to investigate something, we bump into "wait a sec, how did this work in Haskell?") and writing sensible Smalltalk (especially when there is code duplication, like in the case you mentioned above the same code path is shared when traversing both subclasses). A big part of the problem is #62 , in Haskell it's possible to have a kind of "automatic visitors": if a complex object responds to the same visitation protocol as its constituents, the visitor can automatically recurse into each constituent, this is called deriving Functor. In Smalltalk we have to write "visitation descent" by hand.

[shingarov]

convention of using ^ self subclassResponsibility (note the return) when method is supposed to return some useful value

Useful indeed. I am not sure what to do in our situation. MachineArithmetic has become a rather large codebase, and it's not following the ^ convention. If we try to start following it now, my fear is that it may cause even more confusion: when I am looking at a particular sender of subclassResponsibility how do I know whether this particular presence or absence of ^ is on purpose?

[janvrany]

This is an artefact of monkey-copying from upstream, searching for a compromise between maximizing similarity with the upstream (in case we need to investigate something, we bump into "wait a sec, how did this work in Haskell?") and writing sensible Smalltalk

I see. Do we want to unify it?

Useful indeed. I am not sure what to do in our situation. MachineArithmetic has become a rather large codebase

OK, forget it for now. This needs much broader conversation about how to host our code in ST80 (or ST15/ST20). We're not the first ones to have this problem, NewSpeak had it in its early stages too. This is an engineering problem but I feel it needs addressing sooner than later or things become much worse.

[shingarov]

Do we want to unify it?

I think the real fix would be to somehow resolve #62 (which is not today). As to fixing the symptom, we had this conversation with jmv a couple of weeks ago, didn't we?

[janvrany]

Consider following, admittedly pathological, code:

/*@ val f : x:int => int[y | y == (x + 1)] */
let f = (x) => {
	let x = x + 1;
	x
};

This typechecks in upstream sprite but not once this PR is applied.
This is because rename machinery turns

ELet (SpriteDecl (Bind ""x"") (ΛEApp (ΛEApp (EImm (ECon (PBin (BPlus ())))) («x»)) (ECon (PInt (1))))) (EImm («x»))

into

ELet (SpriteDecl (Bind ""x"") (ΛEApp (ΛEApp (EImm (ECon (PBin (BPlus ())))) («x__ß410»)) (ECon (PInt (1))))) (EImm («x__ß410»))

(note the last EImm which is wrong`.

If I change out x′ := x spriteλuniquify. to x′ := x it typechecks (but of course breaks the original test for #139)

[janvrany]

Following should fix the above issue:

ELet >> rename: a to: b
	decl bind id ~= a ifTrue:[
		^ELet
			decl: (decl rename: a to: b)
			expr: (expr rename: a to: b)		
	] ifFalse:[
		^ELet
			decl: (decl rename: a to: b)
			expr: expr
	].

[shingarov]

Following should fix the above issue

Hmm... I think in this "pathological" case (actually the pathology in your inner let x = x+1 in x, I vaguely remember reading this as far back as 1st volume of Curry–Feys) the problem is that there are two captures going on, not one. So in ELet>>rename:to: we need to transform

let x = x+1 in x

into

let x′ = x+1 in x′

However, one onion-layer outside of this, in the λx. … there is another uniquification going on. So there must be three xs, not two; so, two renamings.

[janvrany]

Yeah, you're right. I was too quick. Something like:

ELet >> rename: a to: b
	| sym sym′ decl′ expr′ |
		
	sym := decl bind id.
	sym′:= sym spriteλuniquify.
	
	decl′ := decl class 
						bind: (decl bind rename: sym to: sym′) 
						expr: (decl expr rename: a to: b).	
	expr′ := (expr rename: sym to: sym′ ) rename: a to: b.
	
	^ELet
		decl: decl′ 
		expr: expr′		

This should handle following as well:

⟦val f1 : x:int => y:int => int[z | z === (x + y + 3) ] ⟧
let f1 = (x,y) => {
	let x = x + 1;
	let y = y + x;	
	y + 2
};

[shingarov]

I am asking myself if even that is enough. Shouldn't be there two uniquify's, one in EFun and the other in ELet?

[shingarov]

BTW, this seemingly-boring-bug is turning into an incredibly exciting area, due to https://arxiv.org/pdf/2001.10490.pdf

[janvrany]

IIRC, we agreed this PR will be replaced by #199 once I fix the "too aggresive renaming" issue.
So shall I close this one?

[janvrany]

Closing as resolved via 3ac081f and #283