Conversation

Yeah really need a citation for why exponential code duplication might be a problem in practice.

Yeah I really should compare to that other translation that doesn’t preserve types and is therefore not really related.

Indexed type for WebAssembly isn’t novel. I guess. I don’t even have a joke about that one.

Will you please compare to CertiCoq? Oh sure, you see, they use ANF because I cornered Zoe and Andrew at POPL and tried to convince them that ANF was better than CPS, based on the early result of this paper you're reviewing.

Now they use ANF because I managed to convince Zoe (not Andrew though) to look into it. They've been published cause y'all love a massive Coq proof but not the fundamental research that enables it.

Brendan Zabarauskas

@brendanzab

Sep 5, 2021

Just wanna say, thanks for all the effort on the ANF front, wrt. compiling dependent types. You and

@koronkebitch

have me pretty curious about it and I'm thankful for your efforts, in spite of the setbacks. Really hoping to see this paper eventually!

12:40 AM · Sep 5, 2021Twitter Web App

Sep 5, 2021

:) You can read Paulette's thesis. We might go ahead and post an arxiv version. This submission isn't dead in the water yet.. all B's isn't the worst set of reviews I've come back from.

Replying to

and

Will do! I'm wanting to make an ANF compiler for my dependently typed experiments, so I'll go to Paulette's first – I was originally looking at your thesis. I'm pretty slow at understanding this stuff and I find implementing it from a nice description is the best way I learn. 😅

Replying to

and

Anyway, despite my slowness sometimes I look at this stuff and think ‘man, this stuff is cool, I'm glad somebody worked on this’. So yeah, thanks again for doing cool stuff!

Replying to

and

You should look at Paulette's; she's scaled it up to handle if, and recursion via eliminators. Even have a sketch of how to handle match and fix, but preserving the guard condition is on you.