1. 7

I was reminded of Djinn by John’s recent article, http://degoes.net/articles/insufficiently-polymorphic

If you’re curious to give Djinn a go, it is maintained enough that cabal install works.

Similarly, in older versions of Idris (I haven’t tried the new elaborator reflection stuff), you could use proof tactics to generate functions (since they’re just proofs of types).