Add Agda

[MarisaKirisame]

https://en.wikipedia.org/wiki/Agda_(programming_language) https://github.com/agda/agda Version: 2.5.4.2

agda is a dependently typed language that is like idris. however, it has support for universe polymorphism and homotopy type theory.

---

• [x] Install agda (Agda-2.5.4.2.20190217, use 2.6.0 when released)
• [x] agda-stdlib (https://github.com/agda/agda-stdlib/commit/2c27122a9b5d0acb8e97d9c094a4115b56fa9278)
• [x] cubical (https://github.com/agda/cubical/commit/14e92653ca3d324b793d193e9c292deca9480f8e)
• [x] Testing (agda module.agda)
• [x] Logo for icon
  • Official logo doesn't seem to exist yet (https://github.com/agda/agda/issues/2823)
  • Found these:
  • https://github.com/UlfNorell/agda-logo
  • https://github.com/jmchapman/agda-logos
• [x] CodeMirror mode. Use Haskell for now.

[ice1000]

No!!! 2.6.0 Please!!

[ice1000]

And Cubical Agda/stdlib please!

[DonaldKellett]

Took me a while but I seem to have stumbled upon what looks like a testing framework for Agda. Not sure if it is (easily) customizable though (or even a testing framework in the usual sense) 😛

[ice1000]

Agda is very safe by default so a type alias in the test case may probably be enough (because a by-default total language is entirely not suitable for writing something that cannot easily be tested with type ristrictions).

[ice1000]

But I feel like writing tests is also important.

[MarisaKirisame]

@DonaldKellett I'd say we dont really need one. Agda can evaluate code while typechecking, so you can write test that wont typecheck if the result is wrong.

[MarisaKirisame]

(random testing is still a good idea, but that library is incredibly outdated, has no star, and probably do not has random testing. we should leave it out until we found one.)

[DonaldKellett]

@MarisaKirisame Random testing may not be required if Agda's type system is expressive enough and doesn't provide any escape hatches like Haskell/Idris/PureScript does, but AFAIK Codewars still needs some kind of testing framework (like specdris) where basic assertions such as 3 + 5 `shouldBe` 8 can be written and its results printed to STDOUT, e.g. <PASSED::>Test Passed - Value == 8\n.

[DonaldKellett]

On the other hand @kazk , would it be possible to special-case certain languages in the runner such that those languages need only compile to be considered as "passed"? That could open up whole new classes of languages previously impossible to include on Codewars such as Coq where AFAIK there's no concept of printing stuff to STDOUT or interacting with the outside world.

[MarisaKirisame]

@DonaldKellett it can be written like this test : 3 + 5 ≡ 8 test = refl

test_fail : 3 + 5 ≡ 9 test_fail = refl -- this will not type check

[MarisaKirisame]

@DonaldKellett I think the point is we dont need to special case. The test will just always pass after it typecheck. if there is error then the failing case will be reported.

[kazk]

@DonaldKellett that should be possible. Just always have one implicit test case ("program compiles") that's marked as passed if the exit code is zero.

So the output will be either:

• <PASSED::>: Successfully compiled
• <FAILED::>: Failed to compile. Show error messages that's (hopefully) helpful enough to identify the cause

@MarisaKirisame yeah, that's the idea. Just slightly different from other languages for not having a test framework producing the required outputs.

[MarisaKirisame]

Just to state the obvious, we should not print the error message for failed actual test. Cause if we do so ppl can read what went wrong and fix them one by one (by special casing on the input).

[DonaldKellett]

Cause if we do so ppl can read what went wrong and fix them one by one (by special casing on the input).

But I thought this was what the type system was meant to prevent? E.g. you can't prove A + B = B + A in Coq and related languages by special casing on certain values of A and B.

[kazk]

Just to state the obvious, we should not print the error message for failed actual test.

So we just say it failed and don't show anything else? Wouldn't that be too frustrating? Maybe we're talking about something different.

[ice1000]

Special mention: @gallais

[ice1000]

Just to state the obvious, we should not print the error message for failed actual test. Cause if we do so ppl can read what went wrong and fix them one by one (by special casing on the input).

No! No! No! No! No! You should write the most general type signature to kick the hardcode men :devil_man:.

[MarisaKirisame]

@DonaldKellett there are two way to test agda on codewar. 0: force user to prove he's correct, so you do not need any input/output test 1: test that output match input for a few example. In the latter case, if all the test is visible, one can just cheese by returning a function that only work on the test case

[ice1000]

that's considered bad test because it's easily hackable anyway

[kazk]

I'm starting to play with Agda 2.5.4.2 and agda-stdlib.

Can anyone provide some (minimum) examples that I can use to experiment with?

• test (not really, but the part where kata author writes and requires)
• incomplete solution
• complete solution

If I'm understanding correctly, we don't need to do agda --compile right? agda --compile seems to generate Haskell code after type checking and compile that into an executable. We only care about the result of the type check.

[ice1000]

Initial solution (load this in Emacs, you see hints about all incomplete parts!)

{-# OPTIONS --safe #-}
module Example where
open import Agda.Builtin.Equality

_⇆_ : {A : Set} {a b c : A} → a ≡ b → b ≡ c → a ≡ c
a ⇆ b = ?

Complete solution:

{-# OPTIONS --safe #-}
module Example where
open import Agda.Builtin.Equality

_⇆_ : {A : Set} {a b c : A} → a ≡ b → b ≡ c → a ≡ c
refl ⇆ refl = refl

Test:

{-# OPTIONS --safe #-}
module Test where
open import Example

check : {A : Set} {a b c : A} → a ≡ b → b ≡ c → a ≡ c
check = _⇆_

[ice1000]

If I'm understanding correctly, we don't need to do agda --compile right?

Yup. agda File.agda is already what we want. There're several kinds of library-importing strategies like using CLI arguments or using .agda/ (see https://agda.readthedocs.io/en/latest/tools/package-system.html)

[ice1000]

However, I strongly recommend Agda 2.6.0 (which will be released soon), or simply track the master Agda (and use the experimental branch of the stdlib) because there's a killer feature called cubical model support and the status of 2.6.0 is very close to a release. If you're happy with updating to 2.6.0 after the release, ignore the comment.

[kazk]

Initial solution outputs the following with exit code 1

Checking ExampleTest (/workspace/agda/ExampleTest.agda).
 Checking Agda.Builtin.Equality (/opt/agda/share/x86_64-linux-ghc-8.4.3/Agda-2.5.4.2/lib/prim/Agda/Builtin/Equality.agda).
 Checking Example (/workspace/agda/Example.agda).
/workspace/agda/ExampleTest.agda:5,13-20
Module cannot be imported since it has open interaction points
(consider adding {-# OPTIONS --allow-unsolved-metas #-} to this
module)
when scope checking the declaration
  open import Example

Complete solution outputs the following with exit code 0

Checking ExampleTest (/workspace/agda/ExampleTest.agda).
 Checking Agda.Builtin.Equality (/opt/agda/share/x86_64-linux-ghc-8.4.3/Agda-2.5.4.2/lib/prim/Agda/Builtin/Equality.agda).
 Checking Example (/workspace/agda/Example.agda).

@ice1000 do you have something that can be imported, but fails? I'm trying to figure out what should be shown to the user on failure.

---

However, I strongly recommend Agda 2.6.0 (which will be released soon)

Yeah, I'm just trying things out and 2.5.x was just easier to get started.

[ice1000]

Either remove the --safe line in the test module and use this

{-# OPTIONS --allow-unsolved-metas #-}
module Example where
open import Agda.Builtin.Equality

_⇆_ : {A : Set} {a b c : A} → a ≡ b → b ≡ c → a ≡ c
a ⇆ b = ?

Or use another which does not need you to change the test module:

{-# OPTIONS --safe #-}
module Example where
open import Agda.Builtin.Equality

_⇆_ : {A : Set} {a : A} → a ≡ a → a ≡ a → a ≡ a
refl ⇆ refl = refl

[ice1000]

Agda's semantics of --safe: any unsafe operations, like importing some non---safe modules, postulate, {-# TERMINATING #-} pragma, anything (known) that may either crash the compiler or potentially damage anything at runtime will be forbidden. This makes it a lot easier to be used as an "it type-checks, it works" PL (at least comparing to Idris).

[ice1000]

Special mention: @DonaldKellett

I feel like I have a lot of things to be put to CW when Agda (2.6.0) is launched :).

While Idris really limits my imagination. I mainly study Type Theories so what Idris focus on is not my piece of cake. Making Idris Kata is fun but really annoys me sometimes.

[kazk]

We need to disallow --allow-unsolved-metas. By setting that option, it now has exit code 0 without any warnings.

Checking ExampleTest (/workspace/agda/ExampleTest.agda).
 Checking Agda.Builtin.Equality (/opt/agda/share/x86_64-linux-ghc-8.4.3/Agda-2.5.4.2/lib/prim/Agda/Builtin/Equality.agda).
 Checking Example (/workspace/agda/Example.agda).

This will be considered passed and unlike Idris, we can't check the output for a warning.

Doing agda --safe ExampleTest.agda failed saying --allow-unsolved-metas can't be used with --safe option so maybe we should always use agda --safe. Is there any downsides for always using agda --safe?

---

The one with different type outputs the following with exit code 1.

Checking ExampleTest (/workspace/agda/ExampleTest.agda).
 Checking Agda.Builtin.Equality (/opt/agda/share/x86_64-linux-ghc-8.4.3/Agda-2.5.4.2/lib/prim/Agda/Builtin/Equality.agda).
 Checking Example (/workspace/agda/Example.agda).
/workspace/agda/ExampleTest.agda:8,9-12
.b != .a of type .A
when checking that the expression _⇆_ has type
.a ≡ .b → .b ≡ .c → .a ≡ .c

[Bubbler-4]

Agda's semantics of --safe: any unsafe operations, like importing some non---safe modules... will be forbidden.

This sounds like, if I use --safe on test code, it automatically forces the solution code to use --safe too. If so, I guess we don't need to apply --safe runner-wise; we just explicitly put an options pragma when needed.

[kazk]

@Bubbler-4 It passed even with {-# OPTIONS --safe #-} in test file. I'm guessing --allow-unsolved-metas makes the module considered "safe", so importing it is "safe".

Example.agda

{-# OPTIONS --allow-unsolved-metas #-} -- makes "this" module safe?
module Example where
open import Agda.Builtin.Equality

_⇆_ : {A : Set} {a b c : A} → a ≡ b → b ≡ c → a ≡ c
a ⇆ b = ?

ExampleTest.agda

{-# OPTIONS --safe #-}
module ExampleTest where

open import Agda.Builtin.Equality
open import Example -- importing "safe" module

check : {A : Set} {a b c : A} → a ≡ b → b ≡ c → a ≡ c
check = _⇆_

agda ExampleTest.agda is ok

[gallais]

It passed even with {-# OPTIONS --safe #-} in test file. I'm guessing --allow-unsolved-metas makes the module considered "safe", so importing it is "safe".

There was a long standing bug meaning that option consistency was not checked (agda/agda#2487). It has been fixed in the upcoming 2.6.0.

[kazk]

@ice1000 @gallais Is the error always formatted like the following?

/path/to/module.agda:line,from_col-to_col
error message line 1
error message line 2
...
/path/to/module.agda:line,from_col-to_col
error message line 1

If so, I think we can output something like the following on failure:

or hide the location

I'd like to avoid having a huge wall of text like

or

---

On success, we'll show something like

[kazk]

I think I've got it mostly working, but we can't use standard-library yet. v0.17 doesn't work with --safe and I get the following for master

standard-library's experimental branch seems to work.

[ice1000]

For icon:

agda/agda#2823 https://wiki.portal.chalmers.se/agda/pmwiki.php?n=AIMXXIII.LogoCompetition

[gallais]

Is the error always formatted like the following?

We are using a pretty printer so everything should indeed follow the same format.

However, we need to be a bit careful: Agda also outputs warnings which do not necessarily mean the code is broken. So you may want to pass -Wignore so that you don't get any of these.

[kazk]

All G one looks cool!

Might be difficult to see in icon size, but it looks different from other language icons we have so it can work. Can we use this?

I couldn't vectorize the other one so I couldn't compare.

---

Agda also outputs warnings which do not necessarily mean the code is broken. So you may want to pass -Wignore so that you don't get any of these.

Hmm, currently the output is handled differently depending on the exit code. So when the exit code is zero and the warning is outputted, it should be displayed like

collapsed by default so it shouldn't be a problem in this case.

But warnings and errors are mixed when the exit code is non-zero and warnings are grouped under "Issues" so that can be misleading :thinking: I'll adjust this later if it gets in the way and depending on what users think.

[kazk]

Agda is now available on Codewars! Thanks for all the help! The actual language version is 2.5.4.2.20190217 which I'll update to 2.6.0 once released.

This should be considered an alpha release and I need help testing it. For example, I didn't test the output much because I don't know Agda and it was difficult for me to come up with variations to produce different errors. I installed/type checked standard-library (experimental) and cubical (master), but only confirmed that it can be imported.

Any feedback is appreciated as always :)

For the editor, we're using CodeMirror's Haskell mode and it's not great :(

If any of you want to try making Agda mode for CodeMirror, that'll be great.

[kazk]

We have some Agda challenges now :tada:

https://www.codewars.com/kata/search/agda

Also checkout the new "Thorem Proving" tag.