Open cgswords opened 7 years ago
TALK START 4:44
Nice talk.
Some nits:
List
and Vec
was :cry:End time: 4:58.
(I missed some parts of the talk, the sound was a bit quiet ...)
deriving (Read)
) ? Maybe list
those in a slide for clarity, and then show examples.length :: ADTList -> TypeNat
???data.typeable
but I fail to see how it's related in any way...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.
Wait, did you not include any Ghostbuster reference (graphics?)
There are some terms/concepts that I would be in here (or be more prominent) to help with intuition:
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?
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
CC @tmcdonell