%%% Tic-Tac-Types %% Adapted from the TYPES'19 paper by Sean Innes and Nicolas Wu. %% https://dl.acm.org/citation.cfm?doid=3331554.3342606 %%% Boards as strings type Board | board String; board1 = board "XOOOX X"; board2 = board "XOOXOXOO OX OXO XOX"; % ¿¿ What is that ?? board3 = board "¡I love Emacs!"; % Hmm.. maybe I like where this is going. %%% Pieces type Piece | X | O; type Maybe (t : Type) | nothing | just t; %%% Boards as nested tuples threebythree : Type -> Type; threebythree t = Tuple (Tuple (t, t, t), Tuple (t, t, t), Tuple (t, t, t)); type Board | board (threebythree (Maybe Piece)); %% Now that's better, but the code for 4x4 and 3x3 boards is completely %% different, so we can't easily change the size of the board! %%% Boards as 2D lists of pieces type List (t : Type) | nil | cons t (List t); type Board | board (List (List (Maybe Piece))); board1 = board [[just X, just O, just O], [just O, just X, Nothing], [Nothing, Nothing, just X]]; board2 = [[just X, just X, just O, Nothing]]; % ¡¡ Wrong dimensions !! %%% Boards as fixed size 2D lists type Nat | zero | succ Nat; type NList (size : Nat) (t : Type) | nnil (size = zero) | ncons t (NList ?size' t) (size = succ ?size'); Board (size : Nat) = NList size (NList size (Maybe Piece)); board1 : Board 3; % Well: succ (succ (succ zero)) board1 = [[just X, just O, just O], [just O, just X, Nothing], [Nothing, Nothing, just X]]; board2 = [[just X, just X, just O, Nothing]]; % ¡¡ Type Error, Yay !! head : List ?t -> ?t; head xs = case xs | cons x xs => x | nil => ERROR; % ¡`head` can't be defined as a *total* function! nhead : NList (succ ?s) ?t -> ?t; nhead xs = case xs | ncons x xs P => x | nnil P => impossible P; % ¡`P : succ ?s = zero` saves the day! ntail : NList (succ ?s) ?t -> NList ?s ?t; ntail xs = case xs | ncons x xs P => xs | nnil P => impossible P; % ¡`P : succ ?s = zero` saves the day! getN : Int -> NList ?s ?t -> ?t; getN i xs = if i = 0 then nhead xs % ¡Type error! else getN (i - 1) (ntail xs); % ¡Type error! type Fin (n : Nat) % Un entier naturel plus petit que `n`. | fzero (n = succ ?n') | fsucc (Fin ?n') (n = succ ?n'); nget : Fin ?n -> NList ?n ?t -> ?t; nget i xs = case i | fzero P => nhead xs % `P : ?n = succ ?n'` saves the day! | fsucc i' P => nget i' (ntail xs); % `P : ?n = succ ?n'` saves the day! nset : Fin ?n -> ?t -> NList ?n ?t -> NList ?n ?t; nset i y xs = case i | fzero P => ncons y (ntail xs) ?P | fsucc i' P => case xs | nnil P' => impossible P' % ¡Can't go out of bounds! | ncons x xs P' => ncons x (nset i' y xs) ?P' ; type Lens (s : Type) (t : Type) | lens (getter : s -> t) (setter : a -> t -> t); get : Lens ?s ?t -> ?s -> ?t; get (lens g _) = g; set : Lens ?s ?t -> ?t -> ?s -> ?s; set (lens _ s) = s; lens_of_nlist : Fin ?size -> Lens (NList ?size ?t) ?t; lens_of_nlist i = lens (nget i) (nset i); composeL : Lens ?s ?s' -> Lens ?s' ?t -> Lens ?s ?t; composeL l1 l2 = case (l1, l2) | (lens get1 set1, lens get2 set2) => lens (get2 ∘ get1) (λ v struct -> set1 (set2 v (get1 struct)) struct); lens_of_board : Fin ?size -> Fin ?size -> Lens (Board ?size) (Maybe Piece); lens_of_board x y = composeL (lens_of_nlist x) (lens_of_nlist y);