Linearize before de/refunctionalize

[davidweichiang]

In https://github.com/diprism/compiler/commit/54a29000a6ae7a9ca537a282ffd248ed753139da @HerbertMcSnout added an example illustrating a problem which he traced to the fact that D/R is correct only with linear types, so affine-to-linear needs to be done first.

[davidweichiang]

I think @ccshan or I might be able to tackle some of the other issues this summer, but this one seems like it has to be @HerbertMcSnout. If you've got any time to spare for it, it would be much appreciated!

[colin-mcd]

If I have free time, I'll try to take a crack at this. I think the only really significant change will be generating discard functions for recursive datatypes, like this one for String:

data String = Nil | Cons Char String

define discardString : String -> Unit =
  \ s. case s of
    | Nil -> unit
    | Cons c s' -> discardString s'

Note to self: we can auto-discard any constructor args that are -> or & types, and only need to do work to discard recursive datatype args and * types with recursive datatypes in them.

[davidweichiang]

Thanks. I can try to write this into the paper as well.

[davidweichiang]

Actually, what's written into the paper but commented out is:

linearize[Δ ⊢ fold e] = <fold linearize[e], discard[Δ]> linearize[unfold e] = unfold (linearize[e].1) discard[x : μα.τ] = x.2

I'll be unsurprised if something is wrong with that, but what's wrong with that?

[colin-mcd]

If thee in fold e has some non-1 weight, then that approach would ignore it when discarding.

I think that we need to actually expose the values stored in the μ-type, as the issue in the first place was with code like:

data List = Nil | Cons Bool List;
let x = (Cons (sample amb : Bool) Nil) in False;

Which causes problems when we defunctionalize List, as then x just becomes some foldList constructor that doesn't double the weight. So when discarding x, we have to eliminate it entirely to get all the weights of the nested expressions, I think.

[davidweichiang]

Unlike lambdas and multiplicative products, fold e evaluates e so how about

linearize[Δ ⊢ fold e] = let x = linearize[e] in <fold x, discard[Δ]>

where x is fresh?

[colin-mcd]

I think that it may need to be

linearize[Δ ⊢ fold e] = let x = linearize[e] in <fold x, discard[x]>

Just to make sure that the FVs of both parts are exactly the same. But otherwise I think this should work.

[davidweichiang]

Ah, right.

On Wed, May 11, 2022 at 11:55 Colin McDonald @.***> wrote:

I think that it may need to be

linearize[Δ ⊢ fold e] = let x = linearize[e] in <fold x, discard[x, Δ]>

But otherwise I think this would work.

— Reply to this email directly, view it on GitHub https://github.com/diprism/compiler/issues/54#issuecomment-1123958706, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAKVY2MZ5ZG2NC5RTXZLXL3VJPJ5LANCNFSM5VFG7ZGQ . You are receiving this because you were assigned.Message ID: @.***>

[colin-mcd]

I'm going to start working on this on branch lin-before-dr

[ccshan]

Hi hi, here I am, late again. It seems that <fold x, discard[x]> (where x contains the recursive type) would not be amenable to defunctionalization?

[davidweichiang]

You're right, and in addition, it seems that the problem example is still not producing the right result. So this is still WIP.