Discuss appropriate problems for Idris about idris HOT 3 CLOSED

There are several current exercises that would be appropriate for idris, mainly the functional ones.

Some examples:

• https://github.com/exercism/x-common/tree/master/exercises/rna-transcription
• https://github.com/exercism/x-common/tree/master/exercises/space-age
• https://github.com/exercism/x-common/tree/master/exercises/leap

from idris.

Those exercises suite about every language, you won't need any of idris' special features to solve them.

And even with a lot of bending, I can't think of a way to solve those using dependent types, except for rna-transcription, but its just using Vect n a instead of List a.

Sure this can be used to introduce Vects for the first time.

I'd really like to see some exercises that actually do something with the benefits of dependent types.

hamming in its current for is a good start. By using Vect n a -> Vect n a -> Nat, we specify in the functions type that both inputs are of same length. Also this makes us able to omit clauses for hitting the end of the list for a single list early and idris still knows that its fine. I like this! If now we could also find a way to tell, that the returned Nat will be less than or equal to n… But perhaps that would complicate things too much, but it would show the capabilities of dependent types.

But to be honest, I think we need exercises that deal with proofs and rewrites and stuff. In any language with dependent or refined types, this is my biggest problem. Convincing the compiler that the obvious holds…

from idris.

Maybe we could borrow some stuff from Logical Foundations. There ought to be something useful in https://github.com/idris-hackers/software-foundations

from idris.