I added a translation of this Kata over to Idris, adapting the structure of the code as close as possible (except moving (:<:) from a typeclass (interface in Idris) to a data type that covers all 3 instances similar to the Elem datatype in the Idris standard library.
Idris is a functional language like Haskell, but with a Dependent type system instead. It also, unlike Haskell, uses Strict instead of lazy evaluation.
I've tried porting this as close as possible to Idris, only electing to switch from a typeclass for (:<:) to a proof-like data type instead. Annoyingly/Sadly, the In constructor of Expr generates a warning about it not strictly positive (even though, the way we use it here, that shouldn't pose a problem) that I couldn't find a way to disable, and led to needing me to plaster partial annotations on a lot of the other functions.
Any help improving it appreciated, especially since I mostly write with Idris 2 nowadays!
I added a translation of this Kata over to Idris, adapting the structure of the code as close as possible (except moving (:<:) from a typeclass (interface in Idris) to a data type that covers all 3 instances similar to the Elem datatype in the Idris standard library.
Idris is a functional language like Haskell, but with a Dependent type system instead. It also, unlike Haskell, uses Strict instead of lazy evaluation.
https://www.codewars.com/kumite/63f93ea7cbfbb30047dcece3?sel=63f93ea7cbfbb30047dcece3
I'd appreciate any help or suggestions!
I've tried porting this as close as possible to Idris, only electing to switch from a typeclass for (:<:) to a proof-like data type instead. Annoyingly/Sadly, the In constructor of Expr generates a warning about it not strictly positive (even though, the way we use it here, that shouldn't pose a problem) that I couldn't find a way to disable, and led to needing me to plaster partial annotations on a lot of the other functions.
Any help improving it appreciated, especially since I mostly write with Idris 2 nowadays!