Functional Pearl: Witness Me -- Constructive Arguments Must Be Guided with Concrete Witness

Beloved Curry–Howard correspondence tells that types are intuitionistic propositions, and in constructive math, a proof of proposition can be seen as some kind of a construction, or witness, conveying the information of the proposition. We demonstrate how useful this point of view is as the guiding principle for developing dependently-typed programs.