2016 Talk 4: Trevor McDonell

[cgswords]

CC @tmcdonell

[cgswords]

TALK START 4:44

[cgswords]

Nice talk.

Some nits:

• The indentation of your datatypes List and Vec was 😢
• checked vs. synthesized slide 1: on how ~> for how (?)
• Time for 'moar example' at 4:55
• Actual percentage on numbers (5500 / 8000) would be nice; talking about why the failures occurred would be, too.
• No github link on the end there?
• The lack of a ghostbuster joke is... disturbing 👻

End time: 4:58.

[osa1]

(I missed some parts of the talk, the sound was a bit quiet ...)

• So the main problem is that GADts are hard to work with because of 1) error
  messages 2) we lose some compiler features (deriving (Read)) ? Maybe list
  those in a slide for clarity, and then show examples.
• Maybe I've missed that part, but what was the problem with GADT to ADT
  conversion?
• Again I may have missed, but how does hint help help with GADT<->ADT
  transformations?
• Checked vs. synthesized did you give examples for both?
• I'm completely lost about how to synthesize or check. If I have a
  length-indexed vector how do you derive the length :: ADTList -> TypeNat ???
• Say I have a verified RB-tree or something like that, will Ghostbuster be
  able to generate transformers from GADT representation and ADT
  representation? More generally, I'm wondering what properties my GADTs need
  to have to be able to use Ghostbuster.
• you mention data.typeable but I fail to see how it's related in any way...

[ccshan]

Even though your motivation for this work may be Accelerate and teaching, I expect most of the audience (including myself) to be motivated by wanting to use the tool. So please say the words "convert" and "GADT" within the first 10 seconds and the first 3 minutes of your talk. Perhaps begin with the same slide as you end with?

In the last slide with type signatures before the "moar example" slide, are there some existential quantifiers missing?

The code (such as "data List a...") should not have extra horizontal whitespace that doesn't line up. I guess it's just because Ryan's computer does not enjoy font determinism.

I worry if the light-green syntax highlighting will be visible. Maybe make it a bit darker?

Is it possible to make one or two backup slides about ambiguity checking, etc., for if someone asks "what GADTs can your tool handle?"?

Now you have heard about attribute grammars and their synthesized vs inherited attributes.

[ccshan]

Wait, did you not include any Ghostbuster reference (graphics?)

[rrnewton]

There are some terms/concepts that I would be in here (or be more prominent) to help with intuition:

• "fast prototyping"
• "proof obligations"

Also, we didn't really get any idea of how the code for up/down conversions works at all. What does a manual or generated one look like? What basic operations does it use for someone who is not intimately familiar with Data.Typeable already?

Copied from evernote on phone; excuse typos:

Nice animation on the feature insertion.
Why is going down to ADTS error prone? It should be the new feature box itself right?

I kind of like bringing up the graph early. But it says "ghostbuster" on it.... That hasn't been introduced yet.

Questions:

Praveen - example where the structure changes? No. This is about same recursive structure.

Ryan Scott asked about about what the graphs mean. Is it using synthesized or checked or both?

Ken: can you relate synthesized/checked to synthesized/inherited in attribute grammars?

Aaron Hsu -- how would this tie back to classroom setup?

Me: I ask how the manual conversions are actually written (didn't show)

Omer: what properties must a Gadt have for this to work. Does red black work?
Do you have any general rules about what I need to satisfy? (Ambiguity check in paper)

Aaron Hsu came away with the impression that you don't need the type indexed Gadts at all....

Should probably mention and appeal to gradual typing intuitions