[Hs-Generics] A Lightweight Implementation of Generics and Dynamics (LIGD)

[James Cheney]

Hi,

Sorry! I was subscribed to the list, but I never received any emails
from the generics list server until yesterday, so I didn't realize this
discussion was happening.  (I think the problem was that my list account
was sent to "digest"; I only received the first digest yesterday also.
So it might be good for the list owner to check on this...)  On top of
that, somehow I then managed to delete both Bruno's message and the
digest.

Since I haven't done much more research on generic programming per se,
I'm probably not capable of adding much to a discussion of LIGD beyond
any comments Ralf and other experts have (e.g. in the "comparing
approaches" paper).  From what I've seen, Ralf's "Fun with phantom
types", "generics for the masses" and from what I've heard Stephanie's
RepLib (caveat: haven't read that paper carefully) are in a similar
spirit and subsume much or all of what's in the LIGD paper.  Also,  much
more now appears to be known about complementary things like GADTs,
open/extensible types and functions which could help fix some of the
limitations of the original LIGD approach.

Assuming that GADTs do eventually become a standard feature, I'd
definitely be in favor of using them instead of explicit to/from
conversions in an implementation of LIGD, for efficiency if nothing
else.  In addition, as the FCPT paper notes, there are some natural
seeming things that you can only do if equations are known to the type
system.  This was one motivation for our subsequent tech report on
"first class phantom types", which essentially proposed extending
Haskell 98 with equation guards on datatypes, i.e. GADTs.  But, once you
have GADTs a lot of things appear to get simpler, and simulating
first-class generics/dynamics via type representations seem to be just
one example.

I'm attaching a tarball containing everything that both I and ghci could
make sense of from my code directory for the HW 02 paper; it includes

Dynamic.lhs        -- Isomorphism-based equality types
DynamicLeibniz.lhs -- Leibniz-based equality types
Lambda.hs          -- de Bruijn terms via type equations
Nat.hs             -- Some peano arithmetic using type equations
FoldRep.hs         -- Generates "fold" function from a Rep
MapRep.hs          -- An example of a representation tailored to maps.
                   -- (Not sure this makes sense...)
RepFn.lhs          -- An example of an encoding of a function on types
                   -- (specifically, the one that maps each int to a
                       pair of Ints)

Ralf may have more/better commented code...

I may have more coherent thoughts later as well (and will try to
participate more actively now that I should be getting list emails
regularly).

--James

-- 
James Cheney <jcheney at inf.ed.ac.uk>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: LIGD.tar.gz
Type: application/x-compressed-tar
Size: 9324 bytes
Desc: not available
Url : http://www.haskell.org/pipermail/generics/attachments/20061005/0812630f/LIGD.tar.bin