[TYPES] seeking papers with good examples of the use of GADTs

[Philip Wadler]

Good suggestion.  Henglein's ICFP 08 paper is one of my favorite  
papers of the last few years.  It is beautifully written, and turns  
folk wisdom (a sort is n log n) on its head.  GADTs are well used in  
the paper, but are not essential.  An exercise to set the students is  
to do the same thing without GADTs, using type classes instead,  
providing a good example of the tradeoff between the techniques.   
Indeed, I suspect Fritz's work may become a killer app for type  
classes---sorting in linear time is important enough to get type  
classes or an equivalent into the next generation of PLs.  (That's  
already happening, as the new idea of 'concepts' in C++ is related to  
type classes.) Yours,  -- P

On 10 Apr 2009, at 19:28, Derek Dreyer wrote:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list 
>  ]
>
> I would highly recommend Fritz Henglein's ICFP'08 paper, "Generic
> Discrimination: Sorting and Partitioning Unshared Data in Linear
> Time":
>
> http://portal.acm.org/ft_gateway.cfm?id=1411220&type=pdf&coll=GUIDE&dl=GUIDE&CFID=30629082&CFTOKEN=48962619
>
> It provides a very elegant use of GADTs for expressing distributive
> sorting algorithms in a compact, composable way.  Also, the motivation
> (sorting) is as basic as it gets, and the paper has a good mixture of
> theory and Haskell code to chew on.  There are probably some elements
> of the paper that your students will have trouble with, but they are
> not essential ones.
>
> Derek
>
> On Fri, Apr 10, 2009 at 11:05 PM, Norman Ramsey  
> <nr at eecs.harvard.edu> wrote:
>> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list 
>>  ]
>>
>>
>> I have a class of beginning functional programmers; we're approaching
>> end of term, and I'd like them to learn about GADTs.  One of my goals
>> in the class is to give students practice learning by reading papers,
>> so I am asking for recommendations of papers that have good examples
>> of GADTs in action.   Papers I've used in the past have included
>>
>>  Pottier and Gauthier 2005: Polymorphic Typed Defunctionalization and
>>  Concretization, in Higher-Order and Symbolic Computation
>>
>>  Pottier and Régis-Gianas 2006: Towards Efficient, Typed LR Parsers,
>>  in Electr. Notes Theor. Comput. Sci
>>
>> and
>>
>>  Peyton Jones et al. 2006: Simple unification-based type inference
>>  for GADTs, in the 11th ACM SIGPLAN International Conference on
>>  Functional Programming.
>>
>> Unfortunately the first two rely on concepts in which my students  
>> have
>> little background (LR parsing and defunctionalization respectively),
>> and the the third, while it opens with a nice example, is primarily
>> about the (now obsolete) type-inference algorithm, rather than about
>> how to use GADTs.
>>
>> I am hoping some of you may have suggestions about other papers that
>> would be good tutorials in the use of GADTs.
>>
>>
>> Norman
>>
>>
>>
>

  \ Philip Wadler, Professor of Theoretical Computer Science
  /\ School of Informatics, University of Edinburgh
/  \ http://homepages.inf.ed.ac.uk/wadler/




-- 
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.