Compile error for 2048 game example

[rpjh...@gmail.com]

I am running the pre-built Idirs 64-bit binary for my Windows 8 notebook. I was able to get the hello world example running.

I tried to compile the 2048 example by Kester Tong (https://github.com/KesterTong/idris2048/blob/master/README.md), and received this error:

Effects.idr:48:35:When elaborating type of Main.rndFin':
When elaborating argument ce to type constructor Effects.Eff:
        Can't unify
                Vect (S n) a
        with
                m -> List EFFECT

        Specifically:
                Can't unify
                        Vect (S n)
                with
                        \{uv0} => m -> uv

I am new to functional programming, and Idris. Any tips would be appreciated. Are there any caveats about using the Windows pre-built binary? Thank you.

Robert

[Robert]

I tried reading the Effects.idr file for the error reference line and column number, but all of the files in the folder are of a *.ibc extension, not *.idr.

[Ramon Snir]

I'm not working with Idris regularly and didn't see the error while skimming rndFin''s code, but here's the source of Effects.idr, in case it helps you:

https://github.com/idris-lang/Idris-dev/blob/master/libs/effects/Effects.idr

--
You received this message because you are subscribed to the Google Groups "Idris Programming Language" group.
To unsubscribe from this group and stop receiving emails from it, send an email to idris-lang+...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[Edwin Brady]

Hi,
The Effects library has changed a few times, and it looks like it requires an older version. To update the code for the latest version, anywhere you see “Eff m a”, try updating it to “Eff a” (i.e. remove the first argument). This should probably work.

Edwin.

[Robert]

The man himself! Thanks for the quick reply, however, I think I need to step aside and learn a bit more about Idris before trying to run somebody else's code. I understand the gist of the older library calling methods in the code, but I can't connect the dots on this one. I am sure I'll have more questions as I work through my own examples.

Rob

[Kester Tong]

Hi Rob,

As Edwin said, I haven't updated my code to use the latest version of the Effects library.  I'll try and update it sometime this week.

Kester

[Robert]

Thanks! I just started with Idris, and your code seemed to be just short enough and an engaging subject for me - games - that I dove in. I really need to hone my functional chops first. I am fascinated with Idris because I am also self-teaching higher mathematics, and I see its logical base as a good fit. I appreciate your efforts.

Rob

[Robert]

One last thing: any issues with using the pre-built binaries for Windows 64 bit vs. a Linux or Mac OS X build? Libraries, etc... Thanks!

Rob

[Kester Tong]

Hi Rob,

The idris2048 repo should work with the latest version of Idris now.  I'm doubt there are any Windows specific issues in my code, except that the behavior when reading from the keyboard (when actually playing the game) might differ.  e.g. on my mac you have to press enter after each command.  This isn't really anything to do with Idris, it's just that the standard methods for getting keyboard input aren't designed for playing games where you enter commands one key at a time.

Kester

[Larry Marburger]

Thanks, Kester! I've been referencing this code a lot as I've been learning Idris.

[Kester Tong]

Thanks Larry, I'm glad it was helpful.

On Tue, Oct 14, 2014 at 7:09 AM, Larry Marburger <lmarb...@gmail.com> wrote:

Thanks, Kester! I've been referencing this code a lot as I've been learning Idris.

--
You received this message because you are subscribed to a topic in the Google Groups "Idris Programming Language" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/idris-lang/qjaoVsU54rA/unsubscribe.
To unsubscribe from this group and all its topics, send an email to idris-lang+...@googlegroups.com.

[Robert]

Thank you! That works. Sorry for the late reply. Now, on with Idris...