<commit_before>-----
title: Introduction
date: 16th Febuary 2011
prev: _
next: <a href="/pages/peano.html">Hello, Peano → </a>
-----

About this tutorial
===================

Welcome to *Learn You an Agda and Achieve Enlightenment!*. If you're reading this, 
you're probably curious as to what Agda is, why you want to learn it, and in general what 
the big deal is about dependently typed, purely functional programming.

Inspired by BONUS, the writer of [Learn You a Haskell](learnyouahaskell.com), I decided
that I should write an approachable Agda tutorial that would introduce dependently typed
programming to ordinary people rather than Ivory Tower Academics. Of course, seeing as
*I* am one of those Ivory Tower Academics, this might not be easy. I am, however, prepared
to give it a try. Learning Agda was a very rewarding but very difficult process for me. It
is my hope that, by writing this tutorial, it will become a little bit easier for everyone
else.

Step One: Learn Haskell
-----------------------

<img class='img left' src='/static/koala.png' />

This tutorial is not aimed at anyone completely new to programming. Agda is similar on
a basic level to typed functional languages such as Haskell and ML, and so knowing a 
language in the ML family will certainly make learning Agda a great deal easier. If you
don't know a statically typed functional language, I recommend that you learn Haskell,
as Agda has a close relationship with the Haskell ecosystem. If you're looking for a good
Haskell tutorial, look no further than this book's companion, [Learn You a Haskell](learnyouahaskell.com).
You should only have to read the first few chapters of this book in order to get a feel
for Agda.

If you don't know how purely functional programming works, learn a little of it before 
trying to tackle Agda.

Understanding of imperative and object oriented programming (C, Java, Ruby..) isn't
necessary. In fact, trying to apply skills learnt from these languages might even be
harmful when you're trying to learn Agda.

The moral of the story is: keep an open mind. A lot of Agda's power comes from features 
that are at first difficult to understand. It took a long time for everything in Agda 
to fall into place in my head. Agda is *hard*. After some time, though, Agda's inherent
awesomeness comes to the fore, and it all just clicks. If you encounter 
obstacles in your Agda learning, don't be discouraged! Keep working, and eventually 
you will be a master of Agda fu.

What is Agda, anyway?<commit_msg>Fixed links learnyouahaskell.com<commit_after>-----
title: Introduction
date: 16th Febuary 2011
prev: _
next: <a href="/pages/peano.html">Hello, Peano → </a>
-----

About this tutorial
===================

Welcome to *Learn You an Agda and Achieve Enlightenment!*. If you're reading this, 
you're probably curious as to what Agda is, why you want to learn it, and in general what 
the big deal is about dependently typed, purely functional programming.

Inspired by BONUS, the writer of [Learn You a Haskell](http://learnyouahaskell.com), I decided
that I should write an approachable Agda tutorial that would introduce dependently typed
programming to ordinary people rather than Ivory Tower Academics. Of course, seeing as
*I* am one of those Ivory Tower Academics, this might not be easy. I am, however, prepared
to give it a try. Learning Agda was a very rewarding but very difficult process for me. It
is my hope that, by writing this tutorial, it will become a little bit easier for everyone
else.

Step One: Learn Haskell
-----------------------

<img class='img left' src='/static/koala.png' />

This tutorial is not aimed at anyone completely new to programming. Agda is similar on
a basic level to typed functional languages such as Haskell and ML, and so knowing a 
language in the ML family will certainly make learning Agda a great deal easier. If you
don't know a statically typed functional language, I recommend that you learn Haskell,
as Agda has a close relationship with the Haskell ecosystem. If you're looking for a good
Haskell tutorial, look no further than this book's companion, [Learn You a Haskell](http://learnyouahaskell.com).
You should only have to read the first few chapters of this book in order to get a feel
for Agda.

If you don't know how purely functional programming works, learn a little of it before 
trying to tackle Agda.

Understanding of imperative and object oriented programming (C, Java, Ruby..) isn't
necessary. In fact, trying to apply skills learnt from these languages might even be
harmful when you're trying to learn Agda.

The moral of the story is: keep an open mind. A lot of Agda's power comes from features 
that are at first difficult to understand. It took a long time for everything in Agda 
to fall into place in my head. Agda is *hard*. After some time, though, Agda's inherent
awesomeness comes to the fore, and it all just clicks. If you encounter 
obstacles in your Agda learning, don't be discouraged! Keep working, and eventually 
you will be a master of Agda fu.

What is Agda, anyway?
{'fraction_non_alphanumeric': 0.0675329789328608, 'fraction_numerical': 0.002362669816893089, 'mean_word_length': 4.110663983903421, 'pattern_counts': {'":': 0, '<': 9, '<?xml version=': 0, '>': 9, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '1419920', 'n_tokens_mistral': 1387, 'n_tokens_neox': 1283, 'n_words': 811}