"Practical" Haskell programming very quickly devolves into carefully constructed stacks of monad transformers. "Practical" Idris programming lives in a modality

"Practical" Haskell programming very quickly devolves into carefully constructed stacks of monad transformers. "Practical" Idris programming lives in a modality of extensible effects. These are objectively easier to get started with. (Moreover, I did also include SML in my list of languages better for beginners than Haskell and Scala incidentally. If the purity is the problem, then SML is a great place to start. Begin with proving by induction that an SML program is pure or impure—this will motivate having it internalized in the type theory.) Moreover, you don't even need to use the "proving" parts of Idris. You can use the fragment of Idris which is a fixed Haskell, and move on up to the more interesting bits when they become useful to you. For instance, you can write partial programs (and coprograms) in Idris without doing any proofs; then at the end, you can have someone help you shore it up with proofs that it is sound.