I personally am not really interested in rewriting AQL at all, but rewriting AQL in Haskell would be a fun project for someone. Mostly I'm trying to think in advance of the challenges that would be involved, and I think there are many - the essence of AQL lies in writing down finite presentations of categories (rather than categories) and doing automated theorem proving on these presentations, and I'm not sure fancy types can make this problem go away.