wonks / ICFP_rehearsal_feedback

Temporary repository to collect feedback.
1 stars 2 forks source link

Talk 1: Trevor McDonell #1

Open rrnewton opened 8 years ago

rrnewton commented 8 years ago

There is a lot of code already and it went up to 12 minutes! Probably need to compress the part you presented or reduce detail. B

rrnewton commented 8 years ago

I also didn't have a firm handle about what was new about the encoding -- or what specifically was necessary to scale up to a real language/compiler.

samth commented 8 years ago
rrnewton commented 8 years ago

Ken asked: what advice do you have for someone working on EDSLs in Haskell?

rrnewton commented 8 years ago

Isn't the claim that you "won't introduce errors" too strong? You can add a + 3 to every number and it still type checks. Rather, the LLVM will always be type correct.

If the argument is that the informal benefits extend beyond this, I can buy that. But it's not a watertight guarantee of functional correctness.

vollmerm commented 8 years ago

The slides looked great, and you provided great motivation at the beginning.

The claims about correctness were a bit vague, and mixed in with a software engineering argument. Maybe including concrete examples of what kinds of errors would and would not be prevented would help.

eholk commented 8 years ago

The slides looked really good. I liked the emphasis on pictures rather than text.

At one point you talked about GADT techniques you might be familiar with, but the slide said "familiar GADT techniques." I'd drop familiar from the slides, since the audience (well, me, anyway) may not be familiar with all these techniques.

tmcdonell commented 8 years ago

@rrnewton RE yes, it starts getting code heavy very quickly. This is the territory that is new and I haven't gotten nailed down yet. I want to think of a more concise (or diagrammatic) way to present that, but it is quite detail-heavy.

@rrnewton @eholk good point. I'll put a quick background slide to show the canonical example of GADTs as a well-typed interpreter, so that I can talk about what is missing and then move on to how we add those pieces.

@samth @rrnewton @vollmerm yeah, by "not go wrong" I should have said that we aren't turning well-typed source programs into ill-typed LLVM programs. I'll be more specific in the slides & narrative about that and the other guarantees I am claiming.

@rrnewton RE (+3) to every number: I guess this is to say that I assume you aren't a malicious compiler writer (; But that's a good point and related to the previous about being clear on the claims.

Thanks all for the feedback!

rrnewton commented 8 years ago

I lost the dropbox link for slides -- could you post that here or send again?

tmcdonell commented 8 years ago

https://www.dropbox.com/s/83td5m24i4djno8/haskell-2015.key?dl=0