Comment by gnulinux | Hacker News Reader

Comment by gnulinux | Hacker News Reader

Parent Full thread

I code real life programs in Agda. Some part of my server and my tools are in Agda. One time I was in #haskell freenode IRC channels and people started acting out as if I'm some crazy person. Agda has seemless integration with Haskell. There is almost no friction writing 20% of your program in Haskell (unsafe) and 80% in Agda (safer).

I personally believe, agda is an excellent programming language. It's stdlib is good, concepts and construct are very well-thought out, it's very safe and works surprisingly well. I've been programming in agda for years and almost never had issue implementing anything even though it's not Turing complete. Using sized types you can prove most sane things to terminate anyway. And if you really need infinite loops (say, you're implementing an interpreter of a Turing complete language) then you have many options: (1) disable termination checking for a single function (2) use Haskell to implement a single function (3) use Rust, C, C++ etc to implement a function then with GHC ffi link it to agda.

Maybe I'm just being near sighted, but I'm really surprised more people don't use Agda or Idris in production. The number of times the type system saved my ass is uncountable. You can literally write unittests in your type system it fekkin runs your custom unittests while type checking. How is this not revolutionary? I don't understand.

Wow; I was impressed when I saw someone run an Agda program (rather than declaring success once it compiled).

My main gripe with dependently-typed languages is the amount of wheel-reinventing that's involved; e.g. I might have crafted a "ListOfIncreasing comparisonFunction" type, which is perfectly suited to the problem I need to solve, but then I find myself implementing a map function, a filter function, an append function, a length function, etc. Then I find myself needing a "length of appending commutes" lemma, and an "empty is left identity of append" lemma, and an "empty is right identity of append" lemma, and so on.

It's really nice when it works, as a nice self-contained little module; but any more can get exhausting. I haven't tried integrating Agda with Haskell, but that sounds like a nice tradeoff: do all of the "boilerplate" in Haskell (string plumbing, etc.) to get a "Maybe InputsForMyAgda" value, pass it into whatever tricky algorithm we've managed to implement thanks to Agda keeping us in check, then send the result back into Haskell for throwing into whatever external monstrosity we're interfacing with.

I would share my github projects but unfortunately I don't want this HN persona to be associated with my real name (my github name is my name_lastname unfortunately). Look at some of Ulf Norell's (agda's main author) projects though you'll have a taste, although I think his work is more on the abstract side.

I don't know why you had problem with compiling... All you have to do is run `agda --compile src/Main.agda` and it just works...

> My main gripe with dependently-typed languages is the amount of wheel-reinventing that's involved; e.g. I might have crafted a "ListOfIncreasing comparisonFunction" type, which is perfectly suited to the problem I need to solve, but then I find myself implementing a map function, a filter function, an append function, a length function, etc. Then I find myself needing a "length of appending commutes" lemma, and an "empty is left identity of append" lemma, and an "empty is right identity of append" lemma, and so on.

This is true to some extent, but this has nothing to do with Agda. If you're working in an extremely strict type system like agda's where all types need to be provably constructable, you cannot just start coding. You need to have a good idea what your program will look like. E.g. if you're writing a parser (as I often do because writing parsers in agda is such fun) you need to know some mathematical structure behind parsers.

Take a look at this page: https://agda.readthedocs.io/en/v2.6.1.1/language/sized-types...

Here they build Kleene star, which expresses infinite computation. However, you need to construct it in a (coinductive) way such that it doesn't infinitely loop. You cannot just code something like this. In that page they use a paper to base their functions. You need to know the math behind this to have an idea what will work. But you also absolutely don't need to be a mathematician either. And if you have no clue where to start, having multiple iterations of your program usually results in success. E.g. sometimes I start coding agda, then realize my types aren't good enough, restart, rinse and repeat. In my experience Haskell is much better for programs like this. Once you write your program in Haskell and have an idea where things are going, start formalizing some functions in agda, and then try to rewrite everything in agda. Writing programs in agda doesn't mean it's correct, of course, your business logic can still be wrong. The power of agda that comes from dependent typing, is that you can encode tests and proofs of your invariants into the type system. This means if you really want X to be always correct you can prove X or of it's not easy, you can write a whole bunch of unittests that'll be checked at typecheck time.

Regarding FFI, it's actually very easy, read here: https://agda.readthedocs.io/en/v2.6.1.1/language/foreign-fun...

You can add arbitrary haskell code in your agda programs. If you compile with `agda --no-main` agda doesn't call GHC so you can manually call GHC to link your program. This means you can do everything you can do with GHC to your compiled Haskell code in MAlonzo/

I believe their gripe with compiling was not about invoking or executing the compiler. I believe the issue was with writing code that would (successfully) compile.

> I don't know why you had problem with compiling... All you have to do is run `agda --compile src/Main.agda` and it just works...

My point was that most Agda code I've written, or seen others write, is used to prove theorems; the result is rarely run. Even when implementing "real" algorithmic programs, it's usually just to prove that they satisfy some property, rather than actually using them to do anything ;)

> This is true to some extent, but this has nothing to do with Agda.

It's not inherent to Agda, but it's true in the sense that I could do "stringly typed programming" in Agda (i.e. using big, imprecise types which require a bunch of redundant checking and the compiler won't help me with), but there wouldn't be much point (I might as well do that in, say, Python and benefit from the vast amount of libraries and tooling).

> you can write a whole bunch of unittests that'll be checked at typecheck time.

I do this whenever I'm writing Agda or Idris, and it's so satisfying. The 'test framework' is just the type system, e.g.

    test_parse_empty : Eq (parse "[]") Nil
    test_parse_empty = refl

When I'm testing in most languages I tend to do property checking, e.g. QuickCheck/Hypothesis/etc. I haven't been brave enough to do that during type checking yet ;)

I even do

    _ : (f x y) == expected; _ = refl

makes tests shorter.

I also put my tests in the same file that define them by adding a private module

   module X

   record X : ...

   private
     module test where
        _ : (f x y) == expected; _ = refl

This way it's not possible to export record X without its tests passing.

Did you tried to incorporate cubical agda into some real world development? For me it is cool to let internal machinery handle isomorphism between different types, but cubical agda library is still much smaller than std agda library ;/

Not yet, it's been one of the things I wanted to do for about a year since cubical-agda was released. I dabbled with it but I don't know enough type theory/topology to digest cubical type theory well. I tried a few times, but I didn't understand everything...

The benefits look really promising e.g. proving forall x -> f x == g x -> f == g. I really want to use this theorem in some of my agda projects, but I never needed it desperately enough that I had to drop everything and do this. My usual workaround is implement slowButEasyToUnderstand function. Do a whole bunch of proofs with slowButEasyToUnderstand. Implement fastButComplicated function. Prove forall x slowButEasyToUnderstand x == fastButComplicated x

I think one immediate application I can think of with cubical is, you can implement mergeSort : List X -> List X and then pass this around everywhere. You don't need a Sorter record or whatever since when you implement quickSort, you will be able to prove quickSort == mergeSort, so everything will typecheck. I don't know which will end up getting compiled though.

Reply on news.ycombinator.com