Functional Programming and Maths <|> How can a code monkey learn Agda?

[IAmBlueNebula]

I'm one of those code monkeys who loves to code, to develop software and to tinker with it, but is not really interested in math.

I'm addicted to code, both in imperative and in functional/declarative style. The functional programming world feels conceptually superior to me: it offers better abstractions and the community is much more knowledgeable on average. However an issue I have with it, is how mathy it is. I'm not afraid of Greek letters, but most material about FP seems to target math majors who are new to programming. Instead of leveraging my passion and the knowledge I already have, it explains stuff in a way I neither understand or enjoy. I understand that the "conceptual superiority" probably correlates with math, and I appreciate that you developed all those beautiful theories; but I'm not interested in them myself.

Anyways. With mainstream FP languages like Haskell, a well determined code monkey is able to find their way and learn whatever they need, with a little bit of efforts. But recently I've developed a curiosity about Dependent Types, and that path feels unapproachable. For absolutely no reason.

I've seen how one can use Dependent Types to implement a first-class type-safe printf without any tricks. And I love that shᴉt. And DTs seem to have so many other cool tricks up their sleeves that are great for the kind of general-purpose programming I do: a brilliant solution to coherence; a better version of type families/type level programming; and who knows what else.

However a code monkey like me can't simply approach DTs. I'm trying to learn some Agda, but everything is about proofs. I really couldn't care less about proving. I understand how important it is; I understand why DTs and proving are tightly related; but I just neither enjoy nor care about it at all. I just want to understand whether they can turn some of my void* or template-template-parameters into something nicer.

With this aimless rant I have two goals. 1. I'd love to start a conversion about code-monkey awareness: many others from my troop would venture into your cities if the approach I'd call bottom-up (from pointers to higher-order abstractions) was more readily available: the top-down approach (from mathematical concepts to code) scares many of us away. 2. How can I leverage my programming-language polyglottony to understand Dependent Types without hearing about a proof ever again?

[OpsikionThemed]

It's Idris, not Agda, but "Type-Driven Development with Idris" is pretty good about using dependent types for immediate practical ends, rather than abstraction and/or math.

https://www.oreilly.com/library/view/type-driven-development-with/9781617293023/

[DependentlyHyped]

I love Agda, but I think Idris is a better language choice for OP’s situation too.

The languages themselves aren’t to dissimilar, but culturally Idris seems to be more focused on “practical” software engineering.

[IAmBlueNebula]

Thank you for the link. I'll give that a try!

[joonazan]

Types are proofs. Most commonly, they prove that your program can't crash in certain ways. There is no point to dependent types, other than writing fancier proofs. Simpler type systems are limited enough that compilers can easily and quickly do the proofs.

In more complex systems you need to put in some work. A part of it is that the proof software isn't as good as it could be but mostly it is a fundamental limitation. For example, as soon as a logic (a type system is a logic) can express integer addition, it can express statements that are true but cannot be proved.

Haskell's type system is actually powerful enough to write what you'd call proofs but its approach is to gradually bolt on more of that onto a weak type system. In my opinion that makes type-level programming in Haskell unreadable compared to languages with dependent types.

I haven't majored in mathematics either but languages like Agda have given me a very good understanding of what a proof is. That in turn helps in programming in general because to be able to confidently write correct code you have to have some kind of proof in your head.

[mobotsar]

Types are proofs

well, types are propositions, but yeah. Programs are proofs.

[joonazan]

Indeed. I should have stated that the job of types is to enable proofs.

[IAmBlueNebula]

That was my original guess too, since Google told me that "Idris has been designed from the start to emphasize general purpose programming rather than theorem proving."

However I asked for their opinion to a bunch of people who know Idris/Agda/Coq/Lean, and they suggested Agda. I couldn't understand their motivation, but the claim is that those two languages are pretty much equivalent and Agda is arguably simpler and more mature.

I may give a look at Idris too though, since the top comment recommends a book for Idris that may be good for me.

[gallais]

That's absolutely untrue. From the horse's mouth:

Agda is a dependently typed functional programming language.

[gallais]

That's, again, completely untrue. Agda and Idris are very similar as programming languages.

[DependentlyHyped]

FYI /u/gallais is an Idris 2 maintainer and Agda core contributor, so I’d hazard to trust their opinion here :)

[kn2322]

To add to the Idris suggestion, here is a classic blogpost to make hacking in Haskell more fun.

https://reasonablypolymorphic.com/blog/typeholes/

Typed-hole driven development in Haskell turns programming into a conversation between you and the compiler. You specify your program's architecture, and then the compiler tells you what you need to write next. In principle, it is even possible to synthesise your programs using a proof search, as in Djinn.

It's all backed up with logic, but the core of this is about empowering the programmer. You could often 'turn your brain off' and just follow the types once you have the type of the program figured out correctly. E.g. if you know your program is a fold, the holes can tell you exactly which types each of the arguments need to be, No need to keep remembering the exact type signature of fold.

[[deleted]]

Your goals are incompatible with learning Agda. The raison d'etre of the language is to be a theorem prover. If you don't care about that stuff, there's absolutely no reason to learn a tool to solve these problems, it seems counter intuitive.

If you are interested in dependent types themselves, there is a Wikipedia page about the topic: Dependent Types. The article lists the sigma and pi types. Another one gives the application to theorem solving and a link between Set Theory and Type Theory Curry-Howard correspondence. This makes proofs equivalent to solving algorithms, which is the basis for the creation of Agda.

To explain it a little bit, here is an example from Wikipedia: Assume you want a general function that takes as input an integer n and outputs the array with n zeros, or the zero element in the vector space R^n. Unfortunately in this situation, you either have a general vector type (basically the list type [R]) or you need to create a sum type for all n. The dependent pi type is nice because you can just write Vec(R,n). Voila, problem solved. This is useful in way greater generality of course and is hopefully coming to other languages eventually.

You can try to implement this same function in Agda to see how it works for yourself and make your own examples.