This one involves literal folding! Given a 2D grid (yet again) with a set of marked coordinates, I want to fold it along a given row or column. Since the grid is “transparent”, the marks on each side of the “crease” will “show through”, giving a new set of marked coordinates (on a smaller grid). The first part of this puzzle is to find the number of marks on the grid after a single fold–the first one given in the puzzle input.

I’ll once again use a grid type, this time with boolean entries indicating whether a given coordinate is marked.

```
for S ⊆ (ℕ × ℕ),
Grid Bool ≅ S → Bool
hbounds : Grid α → (ℕ × ℕ)
```

Coordinates are column-major and (0, 0) is the top left entry. Grids
can be of all sizes. *hbounds g* gives the maximum column and row
indices for *g*.

Now I have to think about what it means to fold a Grid onto itself.
For simplicity, I’ll write separate transformations for row and column
folds. To avoid confusion, I’m going to call these *crease*
operations.

```
crease_row : ℕ → Grid Bool → Grid Bool
crease_col : ℕ → Grid Bool → Grid Bool
```

*crease_row r g* can be thought of as being composed of three steps:
first, split the grid *g* into two grids on row *r*, second, “flip
over” one of the segments, and third, overlay them. Here’s the
specification (`;`

is right-to-left composition):

```
-- Specification
crease_row : ℕ → Grid Bool → Grid Bool
crease_row k = split_row k ; orient_v ; overlay
split_row : ℕ → Grid α → (Grid α × Grid α)
orient_v : (Grid α × Grid α) → (Grid α × Grid α)
overlay : (Grid Bool × Grid Bool) → Grid Bool
```

These functions will mostly be described abstractly, in terms of how they map indices to elements. This is enough to calculate with.

The sum of the number of rows of the two grids returned by *split_row*
will always be smaller than the row-size of the original.

Define

```
nrows : Grid α → ℕ
nrows g = let (_, r) = hbounds g in r + 1
```

Then

```
(g′, g″) := split_row g
nrows g′ + nrows g″ < nrows g
```

where *nrows* : Grid α → ℕ gives the number of rows of a grid. I’ll
go further and postulate:

```
nrows g = nrows g′ + nrows g″ + 1
```

That is, *split_row* always divides a grid equally along its central
row. This is a big simplification; maybe it only works for the example
puzzle. [EDIT: Yes, it holds in general. Each crease instruction
bisects a grid.]

The horizontal dimension is preserved by *split_row*:

```
ncols g′ = ncols g″ = ncols g
```

where

```
ncols g = let (c, _) = hbounds g in c + 1
```

Here’s the crucial property of *split_row k g*, which I’m thinking of
here as a map T ⊆ ((ℕ × ℕ) × (ℕ × ℕ)) → Bool × Bool:

(split_row k g) ! ((i, j), (p, r))

```
⎧ ⊥, if j ≡ k ∨ r ≡ k -- cut out the kth row
= ⎨
⎩ (g ! (i, j), g ! (p, r + k + 1)), otherwise
```

This is complicated a bit by the “cutting out” of the *k*th row.
`!`

denotes the index operation Grid α → (ℕ × ℕ) → α.

A similar property describes *split_col*:

(split_col k g) ! ((i, j), (p, r))

```
⎧ ⊥, if i ≡ k ∨ p ≡ k -- cut out the kth column
= ⎨
⎩ (g ! (i, j), g ! (p + k + 1, r)), otherwise
```

I don’t really want to define (!) on products of Grids; this is just a compact way to describe how these functions transform their arguments.

*overlay* is really the core of the function. What are its properties?
Again, I assume for simplicity that I can only overlay grids of the
same size. The crucial idea of “transparency” is captured by the
following property of *overlay*:

```
(overlay (g₁, g₂)) ! (i, j) = g₁ ! (i, j) ∨ g₂ ! (i, j)
```

In other words, a place in the grid *overlay* (*g*₁, *g*₂)) is marked
iff it is marked in *g*₁ or *g*₂. This is pretty much all the meaning
I need to work with *overlay*.

The puzzle promises not to put marks on the row/column of folding,
which eliminates some weird corner cases. It also explains how to
overlay the two grid sections in each case: when folding vertically
(on rows), I’m to fold the *bottom* section *up*, and, when folding
horizontally (on columns), I’m to fold the *left* section *over*.

This is not actually a matter for *overlay*, but for the *orient*
functions.

```
orient_v (gt, gb) = (gt, vflip gb)
orient_h (gl, gr) = (hflip gl, gr)
```

where *vflip* and *hflip* perform vertical and horizontal flips
of a grid, respectively:

```
(vflip g) ! (i, j) = let rmax = π₂ (hbounds g) in
g ! (i, rmax - j)
(hflip g) ! (i, j) = let cmax = π₁ (hbounds g) in
g ! (cmax - i, j)
```

where *row_max g* and *col_max g* give the greatest row/column
indices of *g*, respectively.

I have a specification for the *crease* functions, but it involves
creating intermediate values (the two halves of the split input
grid) only to compute the value I’m actually interested in. It
should be possible to calculate more efficient implementations.

```
crease_row = split_row ; orient_v ; overlay
```

Thinking of grids as functions, what is the relationship between
the functions *g* and *crease_row k g*? Clearly the domain of
the latter is a smaller subset of ℕ × ℕ. Call it S; for
(i, j) ∈ S, I can calculate:

```
(crease_row k g) (i, j)
= { crease_row spec. }
(overlay (orient_v (split_row k g))) (i, j)
= { overlay property }
let (g₁, g₂) = orient_v (split_row k g) in
g₁ ! (i, j) ∨ g₂ ! (i, j)
= { orient_v def. }
let (g₁, g₂) = split_row k g in
g₁ ! (i, j) ∨ (vflip g₂) ! (i, j)
= { vflip spec. }
let (g₁, g₂) = split_row k g
rmax = π₂ (hbounds g₂) in
g₁ ! (i, j) ∨ g₂ ! (i, rmax - j)
```

This eliminates all of the intermediate stuff except for
*split_row*, so I’m almost at the point where I can compute
*crease_row k g* in terms of *g* alone. With slight informality,
I now use the defining property of *split_row*:

```
= { split_row property }
let (g₁, g₂) = split_row k g
rmax = π₂ (hbounds g₂) in
g₁ ! (i, j) ∨ g₂ ! (i, (rmax - j) + k + 1)
```

To eliminate *split_row*, I have to calculate *rmax* without
reference to *g*₂. This is easy, by the transforming the postulate
stated above for *split_row*:

```
nrows g₂ = nrows g - nrows g₁ - 1
≡ { nrows g₁ = k }
nrows g₂ = nrows g - k - 1
```

Then:

```
π₂ (hbounds g₂) = (nrows g₂) - 1
= (nrows g - k - 1) -1
= nrows g - k - 2
= (π₂ (hbounds g)) - k - 1
```

No more *split_row*:

```
(crease_row k g) (i, j) =
let rmax = (π₂ (hbounds g)) - k - 1 in
g ! (i, j) ∨ g ! (i, (rmax - j) + k + 1)
```

Arithmetic further simplifies this:

```
(crease_row k g) (i, j) = g ! (i, j) ∨ g ! (i, (π₂ (hbounds g)) - j)
```

In data terms, this is sufficient to compute the result of
*crease_row k g* without building any intermediate results.
Assume there’s a *grid* constructor (modelled on *array* from
the Data.Array Haskell library) that takes a pair of bounds
and a list of ((ℕ × ℕ) × Bool) pairs to a new grid. Then:

```
crease_row k g =
let (c, r) = hbounds g
rmax = r - k - 1 in
grid ((0, 0), (c, rmax))
[ ((i, j), g ! (i, j) ∨ g ! (i, r - j)) |
i ← [0..c], j ← [0..rmax] ]
```

This completes the calculation of a more space-efficient
*crease_row*. An analogous calculation (left as an exercise for
the reader) can be used to compute *crease_col*, which is similar:

```
crease_col k g =
let (_, r) = hbounds g
cmax = k - 1 in
grid ((0, 0), (cmax, r))
[ ((i, j), g ! (cmax - i, j) ∨ g ! (i + k + 1, j)) |
i ← [0..cmax], ← <- [0..r] ]
```

Assume the grid section of the puzzle input has already been parsed and converted into a Grid Bool, and let the folding instructions be described by a list:

```
data Inst = X ℕ | Y ℕ
[Y 7, X 5, …]
```

This is easy enough to construct from the puzzle input. Then it’s just a matter of folding the folds. To get the solution for part 1, I only need to count the number of marks visible after the first crease. Here’s a more general function which can be used for part 2, as well:

```
creases : Grid Bool → [Inst] → Grid Bool
creases = fold (λ g c →
case c of
X k → crease_col k g
Y k → crease_row k g)
solution = marked (creases init (take 1 insts))
marked : Grid Bool → ℕ
marked = count id
```

Here, *init* is the starting grid and *insts* is the list of
fold instructions, both constructed from the puzzle input.

I have to complete the folding, now, and read the digits off the final grid. Pretty much everything is in place to do this, except for functions to print a grid in a readable form. (No, I’m not going to write an OCR function!) This isn’t very interesting, but here it is, for completeness:

```
print_row :: Grid -> Int -> IO ()
print_row g r = sequence_
(map putStr
(map (\c → if g ! (c, r) then "#" else ".")
[0 .. (fst (hbounds g))])
⧺ [putChar '\n'])
print_grid :: Grid -> IO ()
print_grid g = sequence_ (map (print_row g)
[0 .. (snd (hbounds g))])
```

These functions use the (pseudo-)monadic structure of Haskell’s
`IO`

type. If this is unfamiliar, take a look at the built-in function
`sequence_`

and maybe Chapter 12 of Graham Hutton’s *Programming in Haskell*.