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
Not exactly the feedback you asked for, but I hope it still can be of
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 to
be much more clear. As for kinds, it just puzzles me why you use the
term but don't explain it.
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
* 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!
PGP key 356961A20C8BFD03
Fingerprint: CE6C 4307 9348 58E3 FD94 A00F 3569 61A2 0C8B FD03