Goal
Let people explore programming in Agda without theoretical background.
Ideology
Assumptions
- Most IT people are not interested in theory in the first place.
- One can go a long way without any theoretical knowledge in Agda.
- Theoretical remarks interrupt the programming experience.
- Students react quite differently to theoretical remarks.
(confused ↔ want to know a lot more)
- People who have already played with Agda are more open to theoretical background.
Goal details
- Subgoals
- - give the syntax and semantics of Agda by examples
- - teach Agda programming skills
- Requirements
- - only secondary school mathematics is required
- - Haskell, type theory, and category theory knowledge is not required
- Audience
- - for newcomers
- - followable even without a tutor
How to teach programming skills
Programmers should know equivalent solutions to be able to make design decisions.
Hence we teach program transformations steps.
Programmers should know which solution is better to be able to make design decisions.
Hence we add remarks to each program transformation step.
We teach how to do incremental program construction (planned).
Additional features
- Teach data types first, functions later
GitHub repository
There is a git repository located at GitHub:
https://github.com/mcmtroffaes/AgdaTutorial
You are welcome to submit pull requests (but please make small changes first)!
Social contract
- Remain freely available and ready to fork
- Give citation of sources if applicable
- Try to merge with similar tutorials if any
Users
This is the 6th semester we teach Agda at Eötvös Loránd University (ELTE) with the help of this tutorial.
- 13 weeks × 90 mins.
- Lecturer: Gábor Páli
- Past lecturers: Péter Diviánszky, Ambrus Kaposi
- We also learn a lot by teaching Agda :-)
Further materials
import About.AIM_XVI