andorp / archaidr

Classic Arcade games written in Idris compiled to JavaScript.

ArchaIdr

Classic Arcade games written in Idris compiled to JavaScript.

Summary

TL;DR: Come and join me learning Idris and Game programming!

Implemented games

• Pong game source
• More to come, when I have free time...

Game programming is fun and complex

My goal here is to to have fun and learn something new. I would like provide examples of complex Idris programs which try to find the balance between pragmatic programming and applied dependent types. I believe that dependent types are useful in software development and they are not that hard. In many cases I find restricting myself in other programming paradigms, in a good sense, as an engineer. One sees the problems and their theoretical solutions, but the theoretical solutions needs to be converted into the tools we have at hand. We are actually interested solving some real world problems. I think dependent types add to the programmers toolbox and makes the theoretical to practical transition easier in complex systems.

Games are fun. I started my programming journey implementing games of my own. But also games are complex. Games represent many problems in modern software architectures. Implementing complex games is hard and makes the programmer's mind bend, which is good for learning. I am not a game programmer. I became a software engineer and forgot about games for a long time. So it is time for me to relearn some of these things.

I hope this experience teaches me on how to use dependent types in a pragmatic way. I hope I will find patterns and I can provide feedback for the Idris community which I appreciate for their work and for their effort bringing practical dependent types to the (FP) world.

Note

There is no applied dependent types in this repository so far. Although soon to come, as I try to apply the things from the depedently typed programming book.