The ability to define types and values by structural induction would be extremely useful in many use cases.