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/BasicsThe 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