Learning project by a group of people interested in learning the Idris language
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Failed to load latest commit information.




This is a learning project by a group of people interested in learning the Idris language, a functional programming language with dependent types.

The goal would be to have the bowling kata written in the Idris language by the time we go to BuildStuff 2015, probably November 2015.

If it works out, we can all feel like Jean-Claude: this is how we might feel if we succeed!


  • Andrew Jones - @andrewscj - UTC+0 (DST)
  • Frank Bedlam - I don't tweet - UTC+0 (DST)
  • Ryan Roberts - @ryansroberts - UTC+0 (DST)
  • Jason Imison - @nosami - UTC+0 (DST)
  • Lee Crossley - @lee_crossley - UTC+0 (DST)
  • Tom Janssens - @ToJans - UTC+1 (DST)
  • Koen Metsu - @koenmetsu - UTC+1 (DST)
  • Jef Claes - @JefClaes - UTC + 1 (DST)
  • Jonn Mostovoy - @manpages - UTC+1
  • Antonios Klimis - @antoniosklimis - UTC+2 (DST)
  • Greg Young - @gregyoung - UTC+2
  • Bartul Bonacic - @bartul - UTC+4
  • Paul Szulc - @rabbitonweb - UTC+1
  • Andreas Schlapsi - @aschlapsi - UTC+1 (DST)

Social media etc

For now I don't see the added value of having a twitter account etc. I'd assume the hashtag #Idris101 should be sufficient. Opinions are welcome!

Link to relevant tweets here

Some further learning

In case you'd want to get a feel of what we're trying to grasp, we've set up a preliminary page with some video tutorials on the wiki.

(I've also created a blog post introducing this project here, including some of Andrew's code.)