Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Talk 1: Trevor McDonell #1

Open
rrnewton opened this issue Aug 20, 2015 · 10 comments
Open

Talk 1: Trevor McDonell #1

rrnewton opened this issue Aug 20, 2015 · 10 comments

Comments

@rrnewton
Copy link
Contributor

No description provided.

@rrnewton
Copy link
Contributor Author

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
Copy link
Contributor Author

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
Copy link

samth commented Aug 21, 2015

  • The intro sequence (before the box with the gears) has too many slides.
  • have some pictures for research languages
  • "never go wrong" is not a clear criteria for compiler correctness
    • asked this as a question

@rrnewton
Copy link
Contributor Author

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

@rrnewton
Copy link
Contributor Author

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
Copy link

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
Copy link

eholk commented Aug 21, 2015

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
Copy link

@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
Copy link
Contributor Author

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

@tmcdonell
Copy link

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

5 participants