3 ms·

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 unfortuna

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.html 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-function-interface.html 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/

AnimalMuppet 6y ago
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.
chriswarbo 6y ago
> 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 ;)
- gnulinux 6y ago
  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.

AnimalMuppet 6y ago

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.

chriswarbo 6y ago

> 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 ;)

gnulinux 6y ago
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.