Idris is basically an eager-evaluated Haskell, with other niceties on top (dependent types if you want them; fixed String type)

yes please