Add Idris

[DonaldKellett]

Please complete the following information about the language:

• Name: Idris
• Website: http://idris-lang.org
• Language Version: 1.3.1

The following are optional, but will help us add the language:

• Test Frameworks: (native), specidris
• How to install: see Download
• How to compile/run: idris solution.idr -o solution && ./solution (where solution.idr is the Idris program to be compiled)
• Any comments: Much better suited than Haskell at theorem proving due to proper totality checking (both coverage and termination check). Consider this Haskell "cheat" to "A * B = B * A? Prove it!" - it leverages the absence of coverage and totality checking in Haskell to construct a fake "proof" which would never type-check in Idris to begin with. Also, unlike PureScript which has received virtually no attention, I know of at least one fellow Codewarrior who would like to see it available on Codewars (special mentions below).

---

👍 reaction might help. Special mentions: @ice1000 , @MarisaKirisame 😉

[ice1000]

Is it possible to enforce users to %total?

[kazk]

We might be able to add test support by forking specdris and changing the output.

@ice1000 Can you explain what that is and what's needed to accomplish that?

[ice1000]

@kazk To ensure users don't write unsafe code (like panic in unreachable cases) and infinite-loop code.

Idris has the ability to use the type system to eliminate all impossible cases and people are supposed to make use of this mechanic.

IDK if it's easy to accomplish since I'm rarely Idrising. I was basically throwing some ideas so people can discuss.

[kazk]

@ice1000

By default, Idris allows all well-typed definitions, whether total or not. However, it is desirable for functions to be total as far as possible, as this provides a guarantee that they provide a result for all possible inputs, in finite time. It is possible to make total functions a requirement, either:

• By using the --total compiler flag.
• By adding a %default total directive to a source file. All definitions after this will be required to be total, unless explicitly flagged as partial.

All functions after a %default total declaration are required to be total. Correspondingly, after a %default partial declaration, the requirement is relaxed.

http://docs.idris-lang.org/en/latest/tutorial/theorems.html#directives-and-compiler-flags-for-totality

I guess we can put %default total whenever needed and disallow flagging it as partial? I'm guessing it's not always enforced because that'll be too strict.

[kazk]

The code runner part of Idris support is almost ready.

I've got the test support with specdris by forking and changing the output. The code was easy to follow even it was my first time reading Idris. The example from their repo works.

Minimum example:

module Solution

%access export
%default total

add : Nat -> Nat -> Nat
add a b = a + b

module SolutionSpec

import Specdris.Spec
import Solution

%access export
%default total

specSuite : IO ()
specSuite = spec $ do
  describe "add" $ do
    it "adds two natural numbers" $ do
      (1 `add` 1) `shouldBe` 2

The test needs to export specSuite : IO () like in their example. The name of the module can be anything and the optional preloaded code will be just extra module.

[Bubbler-4]

Just added a thumbs up. I got disappointed at Haskell once when I saw a pile of type system hacking for a seemingly simple task - modular arithmetic; I still have no idea how it works. Idris looks promising in this particular aspect to me.

[kazk]

Idris is now available on Codewars.
See example kumite or wiki page for how to write tests.

[DonaldKellett]

Great, we finally have a language dedicated to theorem proving on CW! 🎉

One thing though - random tests currently appear to be infeasible in Idris, at least when using specdris. While I doubt random tests will find their use in theorem-proving Kata where totality is enforced (which should make it pretty difficult to get hardcoded "proof"s to type-check), a lot of generic Haskell/PureScript kata on topics other than theorem proving should also be suitable for translation into Idris. In those cases, being able to write random tests could be helpful.

Incidentally, pheymann/specdris#1 mentions a QuickCheck implementation in Idris which has not been integrated into specdris as of 06/03/2019. Would such an integration be possible?

[kazk]

Would such an integration be possible?

I'd recommend working with specdris authors and make something that can be used by the Idris community and not just on Codewars. We're using specdris with minimal change so we should be able to use it too.

I'd start by asking them for their plans and what can be helped. It has "help wanted" label so I'm sure they're looking for some help :)

I have no experience with Idris so I can't help with this. Maybe some of our users can, but I think the discussion should happen on pheymann/specdris#1.

[ice1000]

I've did the first non-multiply Kata translation: https://www.codewars.com/kumite/5c7fbeaf9775762c55934656?sel=5c7fbeaf9775762c55934656

[Voileexperiments]

@kazk There's a critical issue in regards to type holes:

1. They don't actually show the type of the holes at all:

2. They're only warnings, which means a kata can be passed with dangling holes that are not evaluated. However holes are as powerful as undefined in Haskell (in fact it's even more powerful because it covers equality types like 2 + 2 = 4 too, unlike believe_me) so for example, in this kata, submitting initial solution passes the kata.

In fact even this works, it's completely absurd:

module Absurd

%access export
%default total

wtf : 2 + 2 = 5
wtf = ?oh_my_god_how_do_I_prove_this

[ice1000]

/cc #717

[Voileexperiments]

There's another issue(?):

Every data type and type level function must be public exported in order for the test module to see them (and the same goes to the test module to main), so %access public export should be the default for almost all cases. This throws people (read: me when solving a Idris kata) off because e.g Try It Online does not need it (code are in the same module as Main.main).

I think at least this should be documented somewhere?

[ice1000]

Doilecument