2016 Talk 1: David - Githubissues

wonks / ICFP_rehearsal_feedback

Temporary repository to collect feedback.

1 stars 2 forks source link

2016 Talk 1: David #13

Open rrnewton opened 7 years ago

rrnewton commented 7 years ago

Comments below.

rrnewton commented 7 years ago

I think "TT" was first mentioned without explanation.

vollmerm commented 7 years ago

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 commented 7 years ago

"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 commented 7 years ago

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 commented 7 years ago

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 commented 7 years ago

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.