6 ms·

A game in a pure language (part 1): introduction and problems with Idris

144 points by panic 7y ago

moomin 7y ago
Grief, this is impressive. For the record, I really can’t recommend learning (typed, pure) functional programming on Idris. It’s a whole extra step beyond learning to do Haskell well.
- kccqzy 7y ago
  I wouldn't think so. As a beginner you can probably just treat Idris like a superset of Haskell and learn the parts that are common to both. For example you can use the `data T =` syntax and not worry about the more advanced `data T where` syntax for GADTs. You can turn off totality checking. You can use simple data types like lists rather than length-indexed vectors. I quite like the book Type-Driven Development with Idris by Edwin Brady. It doesn't assume you already know Haskell. But it does teach you a nice mindset of thinking about types first and use that to drive the implementation.
- rq1 7y ago
  On the contrary, I’d recommend to start with Idris instead. The design of the language is globally better and way more coherent. It fixes a lot of Haskell “mistakes”. Check out “Type-Driven Development with Idris” by Edwin Brady himself. The book is truly amazing.
  - rictic 7y ago
    Idris is great, its design is super impressive, and it expanded my mind tremendously in terms of what is possible in programming. We can and should ask much more of our type systems! It is also way less mature than Haskell, and someone trying to learn it will run into many issues as a result. I mean, read the linked blog post! Needing to regularly restart one's editor, long compile times for even short programs, and difficulties with installation are all issues I also ran into. (Also, strong agree about the book. It's really well written, and all around excellent)
    - dwohnitmok 7y ago
      I would second this. If you've never done pure functional programming before I would hesitate to recommend Idris as your first foray simply because of ergonomic issues with the tooling. Regardless of whether you think Idris the language is suitable for a beginner, it's not a fun experience to deal with the landscape of abandoned libraries, editor integration issues, compiler bugs, etc. if you are already struggling to understand some of the basic principles behind the language. The only exception is if you use it purely as a companion to the Type-Driven Development book. As long as you don't stray too far from the book you generally won't run into any of these other issues and it's more plausible to think of it as a first foray into pure functional programming.
    - tluyben2 7y ago
      Idris 2 is supposed to be better in that regard. I could not see in the article if 1 or 2 was used but I think it was 1; 2 is a lot faster and fixed a lot of issues from 1.
      - moomin 7y ago
        But there won’t be a book.
        lodi 7y ago
        I believe the plan is to release an Idris2 edition of the book. The Idris2 repository currently has all of the book code as part of its test suite and is making progress towards compiling all of it (currently 12 of the 15 chapters).
  - macintux 7y ago
    Thanks for the recommendation, bought it today.
rq1 7y ago
> 1. Compile times Give Idris 2 a try if you’re not afraid of the teething problems.
- bjoli 7y ago
  Isnt Idris 2, like new racket, compiled to chez? I remember Edwin Bring very impressed by the chez backend for Idris 1.
  - rq1 7y ago
    Yes. IIRC according to Edwin, he didn’t want to spend too much time on implementing an efficient RTS and decided to focus on his core competency instead to (correctly) bring in qtt. The result is surprisingly good and fast. Way faster than v1 actually on both compile and run time. Ps. Brady btw.
- deleted 7y ago
  [deleted]
galaxyLogic 7y ago
Could someone quickly summarize how a stateful game is best implemented in a purely functional language, like here? Is there a main tail-recursive function which takes any inputs that have appeared since the last iteration and adds them to the arguments for the next recursive call? The global state would evolve as the arguments of that tail-recursive function over time? Any state-evolution would need to be made by creating new data-structures out of existing ones, not by modifying the existing data-structures, to be "pure". So in essence the whole state of game-world would need to be copied for each iteration? What's the trick that makes it efficient enough to be usable?
- jjnoakes 7y ago
  The whole state of the game doesn't need to be copied per se - if you use efficient functional data structures then only the parts of the state you modify are copied, the rest of the unchanged data structure is referenced directly.
  - galaxyLogic 7y ago
    Is that what happens by default, or do you need to take care to make it be so? I understand you can create a new car-cdr -list out of existing list and a new element, without having to modify anything. So would implementing the game-state functionally then mostly consist of creating new lists non-destructively? Also still wondering about the 'main loop". Is it a tail-recursive function?
    - lalaithion 7y ago
      The common data structures in pure languages are slightly different than what you would find in a stateful language, so you do need to take care to make it so only via what data structures you choose to use. Additionally, the author does say they use Control.ST, which depending how you look at it is either a pure wrapper over stateful operations or stateful looking syntax implemented with technically pure semantics. https://www.microsoft.com/en-us/research/wp-content/uploads/1994/06/lazy-functional-state-threads.pdf https://www.microsoft.com/en-us/research/wp-content/uploads/... The main loop is probably a tail recursive function.
dwohnitmok 7y ago
> Sadly I didn’t manage to make as much use of this type-level programming as I had hoped I would at the beginning: Idris allows you to gradually refine your types, and I’ve often succumbed to just moving on to the next feature as my interest for the game itself grew. This sounds quite promising. Large amounts of mandatory type level programming makes constructing useful programs hard. That it is opt-in is a good thing, and agrees with my own experiences with Idris, which are on a much smaller scale than the OP's.
dmitriid 7y ago
What always amazes about such write-ups is the question "but... but... how?" So: - A year (started in 2019) - With a new language - A purely functional language that's not the easiest to learn and use and ended up with: - an actual playable game prototype - a level editor - a scripting engine - etc. etc. But.... how?! I would still be trying to read files from disk or some such.
- whateveracct 7y ago
  Languages like Idris and Haskell have a big learning curve along with fixed costs around missing ecosystem. But once you pay those off, they allow for single developers or small teams to manage large amounts of complexity and get lots of things "for free" thanks to their composition- and data-oriented nature. A level editor and scripting engine are actually the exact sorts of things I'd expect Idris or Haskell or the like to make noticeably easier than other languages!
  - eyegor 7y ago
    Eh, I'm not sure the level editor/scripting comes from the language so much as the nature of game dev. I've written a hobby 2d engine + game before, level design is a hell of a lot easier if you build an editor to do it in. Same with scripting for enemy behaviors. I wrote one in c++ and another in Java, both ended up with level editors and a limited scripting language designed for my own benefit. Once you have them, it speeds up actual game development immensely.
    - whateveracct 7y ago
      Yeah I agree. But what I was saying is that implementing the level editor / scripting engine is a class of application where pure FP tends to shine.
      - anentropic 7y ago
        This is an interesting point. As a humble pythonist I would like to hear more about why that is... thanks!
heydenberk 7y ago
I'm fascinated by Idris, dependent types and the promise of massively expanding compile-time guarantees. The compile times mentioned in the article raise a question that I've wondered about, and would love to hear from an expert: are compile times essentially unbounded in languages like Idris? Is it possible (likely?) in practice that wrong or misguided uses of the type system could cause quadratic or exponential scaling of compile times?
- pcstl 7y ago
  Yes and no. Yes, you can make compile times _extremely long_. They're not unbounded, as code you use in types needs to pass the _totality checker_, which proves it terminates. (The totality checker requires code to follow certain formats the checker knows how to solve for, otherwise it would solve the halting problem and therefore it could not exist)
- dwohnitmok 7y ago
  Not an expert, but I've played with these languages. The short answer is yes this is possible, but it is also possible already in non-dependently typed languages to do so. Moreover in practice it's not very common to actually evaluate your functions on large literal inputs at compile time. Indeed it's not very common to evaluate the function on a single value as such at all. Instead it is better to think of your functions as abstract rewrite rules, that allow you to substitute one side with the other. Unlike at runtime, recursive functions do not always need to recurse until their base case. Therefore it's not actually very common to e.g. have a recursive function recurse many times at compile time. However, when it does happen, yeah your compile times can shoot up, but it's usually fairly obvious what's causing it. Even then, in absolute terms the quantity of calculations involved generally isn't astronomical, it's rather the case that the compiler is far more inefficient at executing your code at compile time than your runtime system is at executing the compiled code. That being said, dependently typed languages on the whole do tend to have abysmal compile times, but this seems like an implementation issue rather than a fundamental limitation. Efforts like https://github.com/AndrasKovacs/smalltt/blob/master/README.md https://github.com/AndrasKovacs/smalltt/blob/master/README.m... make me hopeful this is something that can be solved.
- 7y ago
lmm 7y ago
case health <= 0 of False => pure () True => Output $ Death target This ought to just be: when (health <= 0) Output $ Death target It takes years to learn all the general-purpose helper functions in these languages (I'm still discovering new ones after 10 years of Scala), but they can help make code so much clearer. And since they're just plain functions rather than keywords or anything, a reader who doesn't know can just jump through to the definition, which is a one-liner: https://github.com/idris-lang/Idris-dev/blob/master/libs/prelude/Prelude/Applicative.idr#L51 https://github.com/idris-lang/Idris-dev/blob/master/libs/pre...
lasagnaphil 7y ago
Developer productivity outside, I'm curious if garbage collection (which almost every functional programming language all have) would become an issue. Especially if you're making a 2D platformer, you really don't want to have any sort of frame stuttering. And yeah, compile times are really a big problem if you're making games, because you need to constantly tweak your game logic and playtest). To be fair C++ also has this issue, but fortunately there are ways to alleviate this problem (minimize template usage, do not use libraries which use template metaprogramming like the notorious Eigen, divide your files into source/header files frequently, etc.)
- dkersten 7y ago
  Unless you’re making a large or complex game, I doubt it will matter. Remember that Minecraft was written in a garbage collected language (although its possible they carefully do object pooling, I’m not sure they did in the early days). On your second point, some people dynamically recompile C++ too! I guess that code maybe is designed for fast compiling. Many other people use an embedded language like Lua for fast iterations.

144 points by panic 7y ago

Grief, this is impressive. For the record, I really can’t recommend learning (typed, pure) functional programming on Idris. It’s a whole extra step beyond learning to do Haskell well.

kccqzy 7y ago
I wouldn't think so. As a beginner you can probably just treat Idris like a superset of Haskell and learn the parts that are common to both. For example you can use the `data T =` syntax and not worry about the more advanced `data T where` syntax for GADTs. You can turn off totality checking. You can use simple data types like lists rather than length-indexed vectors. I quite like the book Type-Driven Development with Idris by Edwin Brady. It doesn't assume you already know Haskell. But it does teach you a nice mindset of thinking about types first and use that to drive the implementation.
rq1 7y ago
On the contrary, I’d recommend to start with Idris instead. The design of the language is globally better and way more coherent. It fixes a lot of Haskell “mistakes”. Check out “Type-Driven Development with Idris” by Edwin Brady himself. The book is truly amazing.
- rictic 7y ago
  Idris is great, its design is super impressive, and it expanded my mind tremendously in terms of what is possible in programming. We can and should ask much more of our type systems! It is also way less mature than Haskell, and someone trying to learn it will run into many issues as a result. I mean, read the linked blog post! Needing to regularly restart one's editor, long compile times for even short programs, and difficulties with installation are all issues I also ran into. (Also, strong agree about the book. It's really well written, and all around excellent)
  - dwohnitmok 7y ago
    I would second this. If you've never done pure functional programming before I would hesitate to recommend Idris as your first foray simply because of ergonomic issues with the tooling. Regardless of whether you think Idris the language is suitable for a beginner, it's not a fun experience to deal with the landscape of abandoned libraries, editor integration issues, compiler bugs, etc. if you are already struggling to understand some of the basic principles behind the language. The only exception is if you use it purely as a companion to the Type-Driven Development book. As long as you don't stray too far from the book you generally won't run into any of these other issues and it's more plausible to think of it as a first foray into pure functional programming.
  - tluyben2 7y ago
    Idris 2 is supposed to be better in that regard. I could not see in the article if 1 or 2 was used but I think it was 1; 2 is a lot faster and fixed a lot of issues from 1.
    - moomin 7y ago
      But there won’t be a book.
      - lodi 7y ago
        I believe the plan is to release an Idris2 edition of the book. The Idris2 repository currently has all of the book code as part of its test suite and is making progress towards compiling all of it (currently 12 of the 15 chapters).
- macintux 7y ago
  Thanks for the recommendation, bought it today.

rq1 7y ago

> 1. Compile times Give Idris 2 a try if you’re not afraid of the teething problems.

bjoli 7y ago
Isnt Idris 2, like new racket, compiled to chez? I remember Edwin Bring very impressed by the chez backend for Idris 1.
- rq1 7y ago
  Yes. IIRC according to Edwin, he didn’t want to spend too much time on implementing an efficient RTS and decided to focus on his core competency instead to (correctly) bring in qtt. The result is surprisingly good and fast. Way faster than v1 actually on both compile and run time. Ps. Brady btw.
deleted 7y ago
[deleted]

galaxyLogic 7y ago

Could someone quickly summarize how a stateful game is best implemented in a purely functional language, like here? Is there a main tail-recursive function which takes any inputs that have appeared since the last iteration and adds them to the arguments for the next recursive call? The global state would evolve as the arguments of that tail-recursive function over time? Any state-evolution would need to be made by creating new data-structures out of existing ones, not by modifying the existing data-structures, to be "pure". So in essence the whole state of game-world would need to be copied for each iteration? What's the trick that makes it efficient enough to be usable?

jjnoakes 7y ago
The whole state of the game doesn't need to be copied per se - if you use efficient functional data structures then only the parts of the state you modify are copied, the rest of the unchanged data structure is referenced directly.
- galaxyLogic 7y ago
  Is that what happens by default, or do you need to take care to make it be so? I understand you can create a new car-cdr -list out of existing list and a new element, without having to modify anything. So would implementing the game-state functionally then mostly consist of creating new lists non-destructively? Also still wondering about the 'main loop". Is it a tail-recursive function?
  - lalaithion 7y ago
    The common data structures in pure languages are slightly different than what you would find in a stateful language, so you do need to take care to make it so only via what data structures you choose to use. Additionally, the author does say they use Control.ST, which depending how you look at it is either a pure wrapper over stateful operations or stateful looking syntax implemented with technically pure semantics. https://www.microsoft.com/en-us/research/wp-content/uploads/1994/06/lazy-functional-state-threads.pdf https://www.microsoft.com/en-us/research/wp-content/uploads/... The main loop is probably a tail recursive function.

dwohnitmok 7y ago

> Sadly I didn’t manage to make as much use of this type-level programming as I had hoped I would at the beginning: Idris allows you to gradually refine your types, and I’ve often succumbed to just moving on to the next feature as my interest for the game itself grew. This sounds quite promising. Large amounts of mandatory type level programming makes constructing useful programs hard. That it is opt-in is a good thing, and agrees with my own experiences with Idris, which are on a much smaller scale than the OP's.

dmitriid 7y ago

What always amazes about such write-ups is the question "but... but... how?" So: - A year (started in 2019) - With a new language - A purely functional language that's not the easiest to learn and use and ended up with: - an actual playable game prototype - a level editor - a scripting engine - etc. etc. But.... how?! I would still be trying to read files from disk or some such.

whateveracct 7y ago
Languages like Idris and Haskell have a big learning curve along with fixed costs around missing ecosystem. But once you pay those off, they allow for single developers or small teams to manage large amounts of complexity and get lots of things "for free" thanks to their composition- and data-oriented nature. A level editor and scripting engine are actually the exact sorts of things I'd expect Idris or Haskell or the like to make noticeably easier than other languages!
- eyegor 7y ago
  Eh, I'm not sure the level editor/scripting comes from the language so much as the nature of game dev. I've written a hobby 2d engine + game before, level design is a hell of a lot easier if you build an editor to do it in. Same with scripting for enemy behaviors. I wrote one in c++ and another in Java, both ended up with level editors and a limited scripting language designed for my own benefit. Once you have them, it speeds up actual game development immensely.
  - whateveracct 7y ago
    Yeah I agree. But what I was saying is that implementing the level editor / scripting engine is a class of application where pure FP tends to shine.
    - anentropic 7y ago
      This is an interesting point. As a humble pythonist I would like to hear more about why that is... thanks!

heydenberk 7y ago

I'm fascinated by Idris, dependent types and the promise of massively expanding compile-time guarantees. The compile times mentioned in the article raise a question that I've wondered about, and would love to hear from an expert: are compile times essentially unbounded in languages like Idris? Is it possible (likely?) in practice that wrong or misguided uses of the type system could cause quadratic or exponential scaling of compile times?

pcstl 7y ago
Yes and no. Yes, you can make compile times _extremely long_. They're not unbounded, as code you use in types needs to pass the _totality checker_, which proves it terminates. (The totality checker requires code to follow certain formats the checker knows how to solve for, otherwise it would solve the halting problem and therefore it could not exist)
dwohnitmok 7y ago
Not an expert, but I've played with these languages. The short answer is yes this is possible, but it is also possible already in non-dependently typed languages to do so. Moreover in practice it's not very common to actually evaluate your functions on large literal inputs at compile time. Indeed it's not very common to evaluate the function on a single value as such at all. Instead it is better to think of your functions as abstract rewrite rules, that allow you to substitute one side with the other. Unlike at runtime, recursive functions do not always need to recurse until their base case. Therefore it's not actually very common to e.g. have a recursive function recurse many times at compile time. However, when it does happen, yeah your compile times can shoot up, but it's usually fairly obvious what's causing it. Even then, in absolute terms the quantity of calculations involved generally isn't astronomical, it's rather the case that the compiler is far more inefficient at executing your code at compile time than your runtime system is at executing the compiled code. That being said, dependently typed languages on the whole do tend to have abysmal compile times, but this seems like an implementation issue rather than a fundamental limitation. Efforts like https://github.com/AndrasKovacs/smalltt/blob/master/README.md https://github.com/AndrasKovacs/smalltt/blob/master/README.m... make me hopeful this is something that can be solved.
7y ago

lmm 7y ago

case health <= 0 of False => pure () True => Output $ Death target This ought to just be: when (health <= 0) Output $ Death target It takes years to learn all the general-purpose helper functions in these languages (I'm still discovering new ones after 10 years of Scala), but they can help make code so much clearer. And since they're just plain functions rather than keywords or anything, a reader who doesn't know can just jump through to the definition, which is a one-liner: https://github.com/idris-lang/Idris-dev/blob/master/libs/prelude/Prelude/Applicative.idr#L51 https://github.com/idris-lang/Idris-dev/blob/master/libs/pre...

lasagnaphil 7y ago

Developer productivity outside, I'm curious if garbage collection (which almost every functional programming language all have) would become an issue. Especially if you're making a 2D platformer, you really don't want to have any sort of frame stuttering. And yeah, compile times are really a big problem if you're making games, because you need to constantly tweak your game logic and playtest). To be fair C++ also has this issue, but fortunately there are ways to alleviate this problem (minimize template usage, do not use libraries which use template metaprogramming like the notorious Eigen, divide your files into source/header files frequently, etc.)

dkersten 7y ago
Unless you’re making a large or complex game, I doubt it will matter. Remember that Minecraft was written in a garbage collected language (although its possible they carefully do object pooling, I’m not sure they did in the early days). On your second point, some people dynamically recompile C++ too! I guess that code maybe is designed for fast compiling. Many other people use an embedded language like Lua for fast iterations.