2016 Talk 1: David

[rrnewton]

Comments below.

[rrnewton]

I think "TT" was first mentioned without explanation.

[vollmerm]

When you started talking about tactics, you threw in terms like hole and focus, and phrases like "solve with typeclass resolution," without giving much context.

I was unclear on the difference/connection between Raw and TT. You used both in your Elaborating DSLs example and I don't remember an explanation of what they were.

I know you were running out of time, but I got lost at the end.

Showing the implementation of mush was a good idea. It's impressively simple.

Despite the technical issues, your textboxes-in-a-slideshow thing is pretty cool.

[samth]

• "Control Your Language" sounds like "Control Your Children"
• Fewer transitions for introducing idris (or examples)
• Elaboration challenges: show the parts of the program that are relevant
• Too many bullets
• Too much text -- more code and examples and type signatures
  *** Lead with an example!
• You don't need so many titles on your slides
• Show how the elaborator is used before showing the code that implements it.

[ccshan]

This suggestion is vague, but is there any way you can make your argument for the first two bullet points on your final slide more explicit? It seems that your argument consists of showing off what one can do by following your advice. Can you perhaps organize your sequence of demos into a compact yet informative classification or outline that you can show on your final slide to remind the audience of why they should draw the same conclusions as you do?

[pravnar]

The slide titled "Metaprogramming dependent types" had three high level points, and you had a lot to say about each point. You might want to either 1) say less during that slide, or 2) make slides that show what you're saying there.

I agree with @vollmerm : it's cool to see code boxes inside slides!

[jsiek]

• The introduction should give more examples of the kinds of language
  extensibility and meta programming that you're aiming to support.
• The slide sequence makes it sounds like Elab. Refl. is primarily a monad.
  While it is a monad, that's not very informative. Lots of things are monads.
  The important thing is that it provides access to the Elaborator.
  The presentation should focus on the Elab. operations and how they can be used
  together with other features of Idris, including other meta programming features.
  The subsequent examples ramp up too quickly, so it's difficult to spot what
  features are being used and combined.