Converting typed term representations: from HOAS to de Bruijn.
http://www.cse.unsw.edu.au/~chak/haskell/term-conv/
Given a GADT representation of a typed higher-order term language using higher-order abstract syntax (HOAS), it is more difficult to convert to an alternative GADT representation using de Bruijn indices for bound variables than I at first expected. Here is a solution using explicit type representations (with Data.Typeable).
