1. 60

  2. 5

    Amazing article and a wonderful idea, thanks for writing it and for sharing!

    As to gradual typing in context of going after new features vs. polishing types on existing ones: I believe you shouldn’t feel bad about this, and for at least two reasons!

    • First and foremost, this is your hobby project, so the most important aspect of it is to have fun; this is important both for you and the project, as you have the highest chance of finishing it if you optimize for your fun :) so whenever you feel it’s becoming a chore, it’s ok to take a seemingly time-wasting stupid side-path, if it relaxes you it can actually reinvigorate your excitement! That said, it’s a balancing act, cutting corners and sitting through is also sometimes a thing when aiming to release ;P I try to look at it as kinda playing with my inner “tiger” and trying to see when can I shorten the leash and push it to bite on some annoying stuff, vs. loosen it and let it play and have fun…
    • Secondly, I’ve come to see weak(er) typing as a valuable tool for quick prototyping. As in focusing on the optimistic path; correctness and corner cases be damned. This way it’s easier to quickly test if the idea makes sense. I’ve had times when finishing the prototype showed me that an idea I had doesn’t work as well as I thought. I then ditched it, so any time spent on handling errors would go to waste. Ideally after the idea proves worthwile in the prototype, that would be a good time to try and enable typing, so that a compiler shows me where the bucket is leaking water and I can start trying to plug them one by one. I’d be very interested in a language & compiler that allows something like this, starting from fully dynamic typing, then letting me switch static typing on, then letting me add proofs/dependent types/linear types/whatnot in some areas I consider worth the effort.

    As to the sandbox aspect of your dream game, I’m curious if you tried to play Noita. I didn’t check it myself yet, but it seems to me from reviews that it may have at least some aspects of what you describe as your dream features.

    1. 3

      Hey thanks for the thoughtful response:) I 100% agree with your “should be fun” criteria. That’s vital. Also agreed with your analysis of time wasted vs time well spent… personally I don’t have problems with that though, at least not some that are immediately obvious, as in I liked doing most of the stuff even when in the end it won’t make it into the final game implementation. Aside from the UI! Really wish I could’ve skipped that.

      Secondly, I’ve come to see weak(er) typing as a valuable tool for quick prototyping. […]

      Personally I think that talking about types as just a verification tool is a bit reductive. I didn’t really talk about that but types definitely help you think about and structure your code. If I have the option (and as a student I generally do) I don’t use dynamic typing.

      As to the sandbox aspect of your dream game, I’m curious if you tried to play Noita

      It’s not really meant to be a sandbox. Its overarching structure is more like WoW. There are definitive zones, questlines, stories, etc. I don’t like sandbox games:D

      As for Noita, I’ll check it out–first time hearing about it!

    2. 4

      I really enjoyed the article! However, it looks like 2 images in the errors section (errors2.png and errors3.png) are 404’ing

      1. 2

        Thanks for the catch, fixed!

      2. 3

        I wonder if Idris 2 (https://github.com/edwinb/Idris2) will help with any of the problems with Idris that you encountered. The Readme makes a few claims which might be relevant:

        • Better inference…
        • Better type checker implementation which minimises the need for compile time evaluation.
        • New Chez Scheme based back end which both compiles and runs faster…
        • Everything works faster :).
        1. 4

          Edwin said that some of the problems will in fact be addressed: https://twitter.com/edwinbrady/status/1216825355417399301

          1. 12

            In particular, I wouldn’t be surprised if a large part of the compilation performance problems were due to ST, which was a fun thing to try but now I think is far too complicated for what it achieves - linear types probably do the job better for the situations where it’s most useful - and the notation is pretty ugly too. Also the fact that it uses implicit conversions internally (which don’t, and won’t, exist in Idris 2) makes it very hard to get good error messages.

            It’s great to see people trying these things anyway! I’ll be interested to find out how Idris 2 deals with it, but I have a bit of work to do before it’ll be possible to try.