Tests at compile time?

[stevejb71]

You can do tests in Idris at compile time:
E.g. for the leap exercise:

total is_leap_year : Nat -> Bool
is_leap_year n = assert_total $ (mod n 4 == 0 && mod n 100 /= 0) || mod n 400 == 0

leap_year_2000 : (is_leap_year 2000 = True)
leap_year_2000 = Refl

@srenatus, @yurrriq: Any thoughts on if this is a better choice than the more traditional runtime testing?

[yurrriq]

I'd prefer to use idris-testing.

[srenatus]

I'm not sure but I think this way of "testing" (it's rather the compiler ensuring, with the help of types, that the program is correct) doesn't apply to all problems. For example, in the "hello world" exercise, it's not obvious to me how to do something similar. (Maybe by changing the types?)

[stevejb71]

I'll have a try with hello-world.
I like it because

• dependent types are a key feature of Idris which this highlights
• does not need any dependencies.

[yurrriq]

For the leap year and hello world exercises this works ok, but in general I'm opposed to it. If you wanted instead to prove theorems about properties of a given exercise, that would be ok.

[srenatus]

@yurrriq I agree. It would make sense to keep hello world as simple as can be -- for getting your feet wet with the exercism CLI, testing of Idris, ... -- and there's nothing keeping you from revisiting hello world (or leap year) to look into advanced features of Idris. This would then be another exercise, though. (I realise that this is not exactly what you proposed, but rather a slight variation of it. 😉 )

[yurrriq]

Closing this since we're going with the unit testing approach.