Add Tic Tac Toe

[neocastro]

No description provided.

[johnchandlerburnham]

I have some questions about the Matrix type you're proposing here. Basically it seems to me that for Matrix.fm we have the following options:

1. the standard dependently typed consctruction from Vector

T Matrix <A: Type> ~ (rows: Nat, cols: Nat)
| matrix<rows:Nat,cols:Nat>(vecs: Vector(Vector(A,cols),rows)) ~ (rows,cols);

Idris: https://github.com/idris-lang/Idris-dev/blob/master/libs/contrib/Data/Matrix.idr

2. A function from coordinates which is similar to what you're doing (although we should add type-safety/indices for dimension). In agda:

Vec : (A : Set a) (n : ℕ) → Set a
Vec A n = Fin n → A

Mat : (A : Set a) (m n : ℕ) → Set a
Mat A m n = Vec (Vec A n) m

More details: https://personal.cis.strath.ac.uk/james.wood.100/blog/html/VecMat.html

3. An interesting recursive construction described here: https://cs.stackexchange.com/questions/56489/recursive-definition-of-matrix

I have implemented this in Formality in this gist: https://gist.github.com/johnchandlerburnham/e35dec10bd8a5b7e512aa62e985d934e

Each of these approaches has different problems. Vectors makes proofs messy if you want to get things along columns instead of rows (and it giving Vector.fm some attention). Functions is great if we can get functional extentionality working with transport. And the recursive definition doesn't have canonicity, which means that we either need smart constructors (I tried a little to write it, but it seemed hard and not of obvious benefit over vectors) or we need quotients, which is the same problem as for #2.

So my feeling is that we should write a Matrix.fm based on the Idris method for now, and possibly revisit later when we know more about fancy extensional equality features.

@MaiaVictor, thoughts?

[VictorTaelin]

I think it is not time to think about Matrix instead, specially just for the sake of Tic Tac Toe. Just write a list of lists on the Tic Tac Toe namespace, it is fine. We can think about implementing a proper Matrix.fm later.

[VictorTaelin]

So, should this be merged? Will this be changed? Waiting

[MaisaMilena]

So, should this be merged? Will this be changed? Waiting

If TicTacToe.fm can be added to the master all terms must have their names updated to start with TicTacToe (and we are currently making the PR to dev-taelin-arena not master). Another option is to this PR be made to my personal repository to update the original code and it could keep the names of the current terms.
We would keep it away from Moonad and then add it as a post in moonad.org. What do you think?