[ feature ] datatype descriptions

* We move away from the ad-hoc definition of Nat to a more general
  description-based system. This impacts pretty much everything
  hence quite a big diff.
  Left to do: implementing `fold` for a description algebra and
  typechecking.