Affine terms and fail

[colin-mcd]

How should we make the affine term \ b. (\ c. if b then true else c) fail linear? If we follow the rules from the document and realize too that each individual case needs to use the same set of vars as each other case, then it becomes if amb then inl (\ b. case (if amb then inl (\ c. if b then (if c then true else true) else c) else (if b then inr unit else inr unit)) of inl f -> f fail | inr u -> fail) else inr unit

Note that if b then true else c becomes if b then (if c then true else true) else c, which because c will be fail, would cause this term to fail even when b is true (which is unintuitive). Is this wrong, or is it intended?

One possible solution (if it is indeed not desired), I think, would be to do the same trick we do with functions on all local variables. That way, c would get type Bool + Unit (from if amb then inl fail else inr unit), and the then case would fail on the inl fail branch and proceed as normal on the inr unit branch. EDIT: my proposed solution won't work for terms like \ b. if b then b else true because in the else case it will assume b is inr unit (failing if it is inl), but because we use b elsewhere (we are case splitting on it), it must already be inl.

[ccshan]

(which is unintuitive). Is this wrong, or is it intended?

Well… it feels intuitive to me? In a call-by-value language (such as ML or Scheme but not Haskell), using fail (throwing an exception) as an argument makes the entire application fail, even if the applied function does not use its argument. So (\ c:Bool. true) fail should also fail. (Because the type of c is Bool and there is no arrow in this type Bool, even the linear language allows this expression (\ c:Bool. true) fail. And it's intuitive to me for this expression to fail, whether in the affine language or in the linear language.)

The way I'm thinking the affine-to-linear translation should work is

• If e has unit type then discard e in translates to let unit=e in
• If e has pair type then discard e in translates to let (x,y)=e in discard x in discard y in
• If e has sum type then discard e in… translates to case e of inl x -> discard x in… | inr y -> discard y in… (actually it might be better to avoid duplicating … by using an intermediate result of unit type)
• If e has function type then discard e in… translates to case e of inl f -> fail | inr u -> let unit=u in…
• Accordingly, e0 e1 translates to case e0 of inl f -> f e1 | inr u -> fail as you know, and more interestingly, \ x1. e2 translates to if amb then inl (\ x1. e2) else discard all my free variables, or at least all my free variables whose types contain arrows, in inr unit

One possible solution (if it is indeed not desired), I think, would be to do the same trick we do with functions on all local variables.

As someone used to call-by-value, I'd ask those who desire this trick to change their c:Bool to a thunk c:Unit->Bool.

[colin-mcd]

Alright, makes sense then! I'll close this issue, since this is indeed the desired behavior.