Skip to content

2016 Talk 4: Trevor McDonell #17

Open

Activity

changed the title 2016 Talk #4 - Trevor McDonell 2016 Talk #4: Trevor McDonell on Sep 9, 2016
changed the title 2016 Talk #4: Trevor McDonell 2016 Talk 4: Trevor McDonell on Sep 9, 2016
cgswords

cgswords commented on Sep 9, 2016

@cgswords
Author

TALK START 4:44

cgswords

cgswords commented on Sep 9, 2016

@cgswords
Author

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

osa1 commented on Sep 9, 2016

@osa1
Member

(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

ccshan commented on Sep 9, 2016

@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

ccshan commented on Sep 9, 2016

@ccshan

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

rrnewton

rrnewton commented on Sep 14, 2016

@rrnewton
Contributor

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions

      2016 Talk 4: Trevor McDonell · Issue #17 · wonks/ICFP_rehearsal_feedback