[HN Gopher] A game in a pure language (part 1): introduction and...
___________________________________________________________________
A game in a pure language (part 1): introduction and problems with
Idris
Author : panic
Score : 77 points
Date : 2020-01-19 00:15 UTC (22 hours ago)
(HTM) web link (flowing.systems)
(TXT) w3m dump (flowing.systems)
| rq1 wrote:
| > 1. Compile times
|
| Give Idris 2 a try if you're not afraid of the teething problems.
| moomin wrote:
| 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.
| rq1 wrote:
| 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 wrote:
| 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)
| kccqzy wrote:
| 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.
| galaxyLogic wrote:
| 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 wrote:
| 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 wrote:
| 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 wrote:
| 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/...
|
| The main loop is probably a tail recursive function.
| whateveracct wrote:
| It's a bunch of trees. You end up only copying the spine (from
| modified leaf to root). containers & unordered-containers are
| the popular packages.
|
| It's also pretty common to still use mutability (the vector
| package in Haskell is hugely popular) but it tends to be
| principled and/or abstracted out because its use is explicitly
| tagged in type signatures. And those APIs can get even better
| once LinearTypes land.
|
| In gamedev, both can be useful. Vector is useful for
| performance and GC relief (when Storable/Unboxed). Immutable
| structures are still useful when backtracking is needed since
| they make it trivial and performant in that setting. A useful
| property for debugging, "training mode", replays, netcode etc.
|
| Recursion is used but not necessarily self tail recursion
| thanks to general TCE.
| sansnomme wrote:
| Can you elaborate on why tail recursion is not necessary? The
| stack is not exactly cheap.
| curryhoward wrote:
| I believe they are just saying that tail calls can be used
| in a mutually recursive way without consuming unbounded
| memory. They said "self tail recursion" is not necessary
| but you interpreted it as "tail recursion is not
| necessary".
___________________________________________________________________
(page generated 2020-01-19 23:00 UTC)