Implementing type theory in higher order constraint logic programming