You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
(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...
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.
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
Activity
cgswords commentedon Sep 9, 2016
TALK START 4:44
cgswords commentedon Sep 9, 2016
Nice talk.
Some nits:
List
andVec
was 😢End time: 4:58.
osa1 commentedon Sep 9, 2016
(I missed some parts of the talk, the sound was a bit quiet ...)
messages 2) we lose some compiler features (
deriving (Read)
) ? Maybe listthose in a slide for clarity, and then show examples.
conversion?
transformations?
length-indexed vector how do you derive the
length :: ADTList -> TypeNat
???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.
data.typeable
but I fail to see how it's related in any way...ccshan commentedon Sep 9, 2016
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 commentedon Sep 9, 2016
Wait, did you not include any Ghostbuster reference (graphics?)
rrnewton commentedon Sep 14, 2016
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?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