Type Tac Toe: Idris Version ($1673837) · Snippets

Type Tac Toe: Idris Version

Based on the post by Chris Penner, I decided to make an implementation of the approach using Idris. The purpose of this language is exactly Type-Driven Development, so the code has much less noise and it's much simpler than Haskell's one.

I am, however, nothing more than a beginner in Idris. If you, dear reader, are more versed in this language and something catches your eye (whether a bug or a possible improvement), don't hesitate to tell me!

Edited Oct 11, 2017

tictactoe.idr 1.27 KB

JW @jwin · Oct 11, 2017

Actually there should be an 0 or X in the example game.. I think. The typesystem should validate the (explicit) alternating players, here it seems to alternate 'automatically', not going through compiler validation (?)

Also testing this, I was able to place for example an X into a field already set by an O, this should not be possble. So the Haskell version validates moves quite differently I think.

Actually there should be an 0 or X in the example game.. I think. The typesystem should validate the (explicit) alternating players, here it seems to alternate 'automatically', not going through compiler validation (?) Also testing this, I was able to place for example an X into a field already set by an O, this should not be possble. So the Haskell version validates moves quite differently I think.

Please register or to comment