Anton Dergunov | 8 Jan 20:22 2013
Picon

Seeking feedback for a tutorial paper draft about GADTs

Hi Haskellers,

I have written a draft of an introductory-level tutorial paper about GADTs in Haskell (for submittion to
proceedings of the recent LASER summer school) and I would like to seek initial feedback about its
content: what information is probably missing? are there any subtle mistakes?

The main idea of this article was to serve as a starting point for learning GADTs (I was missing this kind of
information myself some time ago), so I have collected several examples demonstrating common use cases.

Here is a link to the paper:
https://docs.google.com/open?id=0B9ZIIsDR0B7Hb1VBTFZOZEUzXzA

--
Best Regards,
Anton Dergunov
Attachment (gadt.pdf): application/pdf, 386 KiB
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Alexander Batischev | 9 Jan 16:13 2013
Picon

Re: Seeking feedback for a tutorial paper draft about GADTs

On Tue, Jan 08, 2013 at 11:22:39PM +0400, Anton Dergunov wrote:
> I have written a draft of an introductory-level tutorial paper about
> GADTs in Haskell (for submittion to proceedings of the recent LASER
> summer school) and I would like to seek initial feedback about its
> content: what information is probably missing? are there any subtle
> mistakes?

Not exactly the feedback you asked for, but I hope it still can be of
some use.

As a person with no prior knowledge about GADTs, I found your paper a
good introduction. Following proof of correctness of red-black tree
insertions turned out to be a little bit of a challenge as type
annotations quickly become tangled (made me wondering how one should
prove correctness of the proof).

I particularly liked how you handle things that are not central to
tutorial, like phantom and existential types: you give single-sentence
explanation that provides good enough intuition to follow you further.

Talking of quick explanations, I would love to see kinds and singleton
types explained in the same manner. You tried to explain singleton types
at page 13, but I find explanation provided by GHC documentation[1] to
be much more clear. As for kinds, it just puzzles me why you use the
term but don't explain it.

  1. http://hackage.haskell.org/trac/ghc/wiki/TypeNats/Basics

The same goes for type families - while I was able to quickly look up
definition of singleton types, I failed to comprehend basics of type
(Continue reading)

Anton Dergunov | 12 Jan 09:57 2013
Picon

Re: Seeking feedback for a tutorial paper draft about GADTs

I would like to thank Owen Stephens, Alexander Batischev, Denis Kasak and Mann mit Hut for the valuable comments! I am going to update the tutorial to fix the indicated issues. Also, I am going to improve description of kinds and singletons. Also, I will improve description of red-black tree example: I think I need to include the whole listing after every big step.

Are there any other topics you would like to be described in the context of a practical-oriented introductory-level tutorial on GADTs?

PS: Please let me know if I misspelled your names (to make sure that I do not put wrong names in acknowledgements section). You can do it by email to anton dot dergunov dog mail dot ru.

--
Best Regards,
Anton Dergunov

Среда, 9 января 2013, 17:13 +02:00 от Alexander Batischev <eual.jp <at> gmail.com>:
On Tue, Jan 08, 2013 at 11:22:39PM +0400, Anton Dergunov wrote:
> I have written a draft of an introductory-level tutorial paper about
> GADTs in Haskell (for submittion to proceedings of the recent LASER
> summer school) and I would like to seek initial feedback about its
> content: what information is probably missing? are there any subtle
> mistakes?

Not exactly the feedback you asked for, but I hope it still can be of
some use.

As a person with no prior knowledge about GADTs, I found your paper a
good introduction. Following proof of correctness of red-black tree
insertions turned out to be a little bit of a challenge as type
annotations quickly become tangled (made me wondering how one should
prove correctness of the proof).

I particularly liked how you handle things that are not central to
tutorial, like phantom and existential types: you give single-sentence
explanation that provides good enough intuition to follow you further.

Talking of quick explanations, I would love to see kinds and singleton
types explained in the same manner. You tried to explain singleton types
at page 13, but I find explanation provided by GHC documentation[1] to
be much more clear. As for kinds, it just puzzles me why you use the
term but don't explain it.

  1. http://hackage.haskell.org/trac/ghc/wiki/TypeNats/Basics

The same goes for type families - while I was able to quickly look up
definition of singleton types, I failed to comprehend basics of type
families by reading Haskell Wiki. I ended up pretending that type
families are just type-level functions.

I would love to see Yampa optimizations section expanded with more
interesting examples. Are there any?

Last but not least, a few minor typos and errors I spotted:

* at page 8, "Than we need to declare type instances..." should be "Then
  we need...";

* probably due to excessive editing, parameters to repeatElem at page 13
  are in the different order than before;

* at page 14, you state:

  > As in all binary search trees, for a particular node N c l x r
  > values greater than x are stored in left sub-tree (in l) and values
  > less than x are stored in right sub-tree (in r).

  But later on, your code contradict that statement by recursing to left
  sub-tree when x we look for is less than value in the node, and to
  right sub-tree when x is greater than value in the node.

Thank you once again for a nice introduction to GADTs!

--
Regards,
Alexander Batischev

PGP key 356961A20C8BFD03
Fingerprint: CE6C 4307 9348 58E3 FD94 A00F 3569 61A2 0C8B FD03



_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Gmane