Challenge Problems

This is a collection of small exercises to help you come to grips with dependent types in Idris.

• A list type that enforces ordering.
  • Suggested reading: Conor McBride defines a whole class of sorted structures in "How to keep your neighbours in order". In a nutshell, he advises using indices as top-down constraints on data, rather than bottom-up inferred "description". He then indexes his structures by the interval, in which the contained values must lie.