The idea of the Launchpad series is to provide affordable training in interesting languages and technologies for Scottish developers.
The events are inexpensive because they are run by unpaid volunteers who want to share their knowledge and increase the uptake of the technologies they care about.
NCR pick up the tab for the volunteers' expenses and open up our offices to host the events. As only limited spaces are available we charge a nominal ticket price to try and ensure that tickets are only claimed by those genuinely intending to attend.
Idris (named after the dragon from Ivor the engine) is one of the first dependently typed languages that is suitable for general purpose programming.
Dependent types allow types to be predicated on values so, for example, trying to read a value from an empty list could become a compile time error instead of a runtime one.
We've surprised ourselves so far in the launchpad series by managing to attract such well known names to run the courses, but this is the first time we've gone right to the source and nabbed the creator of language.
Never heard of Idris? Never heard of dependent types?
Edwin will bring you up to speed with the cutting edge of type theory and how these concepts are implemented in Idris.
You might not expect to be coding in Idris in the near future but the concepts you will be introduced to are likely to appear in more main stream languages over the coming years.
They are already being implemented without direct language support.
This course is going to cover some pretty advanced stuff, but fortunately Edwin is an engaging speaker.
Familiarity with a statically typed functional language such as Haskell would be helpful, but not required. As a minimum you will however need to be proficient in at least one programming language.
Tickets will be available here soon.