add parallel-letter-frequency (#61)

Author: oxe-i

config.json

@@ -393,6 +393,14 @@
         "prerequisites": [],
         "difficulty": 6
       },
+      {
+        "slug": "parallel-letter-frequency",
+        "name": "Parallel Letter Frequency",
+        "uuid": "67c85ebf-e5da-4f05-ae86-5a988c2ae499",
+        "practices": [],
+        "prerequisites": [],
+        "difficulty": 6
+      },
       {
         "slug": "change",
         "name": "Change",

exercises/practice/parallel-letter-frequency/.docs/instructions.append.md

@@ -0,0 +1,38 @@
+# Instructions append
+
+## Asynchronous tasks
+
+[Tasks][tasks] are the primary abstraction for writing asynchronous code in Lean.
+They are lightweight and may execute in parallel on another thread, or concurrently on the same thread.
+
+Tasks can be either pure or impure.
+Pure tasks are created with `Task.spawn`, which accepts a pure computation.
+Impure tasks are created from `IO` computations using, for example, `IO.asTask`, which lifts an `IO α` into a `Task α` within the `IO` monad.
+
+In this exercise, the function `calculateFrequencies` is monadic, returning a `IO (Std.TreeMap Char Nat)`.
+This allows the use of impure tasks via `IO.asTask`, and also makes it possible to spawn pure tasks for intermediate computations before returning the final value.
+
+## Preventing data races
+
+As a functional language, most values in Lean are persistent, i.e., immutable.
+Operations that appear to modify a value actually produce a new value with the requested changes.
+This means that memory can often be shared safely between tasks without introducing data races.
+
+Note, however, that not all data structures are equally well suited to persistent use.
+For example, updating a single element of an `Array` usually requires copying the entire array.
+The same is true for `Std.HashSet` and `Std.HashMap`.
+
+To make such data structures efficient, Lean employs reference counting.
+As long as a value has a unique reference, updates may be performed destructively, avoiding unnecessary copying.
+
+Other data structures, such as `List`, `Std.TreeSet` and `Std.TreeMap`, are designed to share structure internally.
+They reuse unchanged nodes when updates are performed, so that multiple values may share references to those nodes.
+As a result, modifying one part of the structure does not usually require copying the entire value.
+This makes them particularly well suited for sharing between tasks.
+
+## Measuring execution speed
+
+The execution time of each test is measured in nanoseconds using `IO.monoNanosNow` and shown alongside the results.
+You can experiment with different approaches and check their impact on runtime performance.
+
+[tasks]: https://lean-lang.org/doc/reference/latest/IO/Tasks-and-Threads/#Task

exercises/practice/parallel-letter-frequency/.docs/instructions.md

@@ -0,0 +1,7 @@
+# Instructions
+
+Count the frequency of letters in texts using parallel computation.
+
+Parallelism is about doing things in parallel that can also be done sequentially.
+A common example is counting the frequency of letters.
+Employ parallelism to calculate the total frequency of each letter in a list of texts.

exercises/practice/parallel-letter-frequency/.meta/Example.lean

@@ -0,0 +1,25 @@
+import Std
+
+namespace ParallelLetterFrequency
+
+def countText (text : String) : Std.TreeMap Char Nat :=
+  text.foldl (fun acc ch =>
+    if ch.isAlpha
+    then acc.alter ch.toLower (fun
+          | none => some 1
+          | some v => some (v + 1)
+        )
+    else acc
+  ) {}
+
+def calculateFrequencies (texts : List String) : IO (Std.TreeMap Char Nat) :=
+  let tasks := texts.map (fun text => Task.spawn (fun () => countText text))
+  return Task.get (Task.mapList (·.foldl (·.foldl (fun acc k v1 =>
+      acc.alter k (fun
+        | none => some v1
+        | some v2 => some (v1 + v2)
+      )
+    ) · )
+  {} ) tasks)
+
+end ParallelLetterFrequency

exercises/practice/parallel-letter-frequency/.meta/config.json

@@ -0,0 +1,17 @@
+{
+  "authors": [
+    "oxe-i"
+  ],
+  "files": {
+    "solution": [
+      "ParallelLetterFrequency.lean"
+    ],
+    "test": [
+      "ParallelLetterFrequencyTest.lean"
+    ],
+    "example": [
+      ".meta/Example.lean"
+    ]
+  },
+  "blurb": "Count the frequency of letters in texts using parallel computation."
+}

exercises/practice/parallel-letter-frequency/.meta/tests.toml

@@ -0,0 +1,50 @@
+# This is an auto-generated file.
+#
+# Regenerating this file via `configlet sync` will:
+# - Recreate every `description` key/value pair
+# - Recreate every `reimplements` key/value pair, where they exist in problem-specifications
+# - Remove any `include = true` key/value pair (an omitted `include` key implies inclusion)
+# - Preserve any other key/value pair
+#
+# As user-added comments (using the # character) will be removed when this file
+# is regenerated, comments can be added via a `comment` key.
+
+[c054d642-c1fa-4234-8007-9339f2337886]
+description = "no texts"
+
+[818031be-49dc-4675-b2f9-c4047f638a2a]
+description = "one text with one letter"
+
+[c0b81d1b-940d-4cea-9f49-8445c69c17ae]
+description = "one text with multiple letters"
+
+[708ff1e0-f14a-43fd-adb5-e76750dcf108]
+description = "two texts with one letter"
+
+[1b5c28bb-4619-4c9d-8db9-a4bb9c3bdca0]
+description = "two texts with multiple letters"
+
+[6366e2b8-b84c-4334-a047-03a00a656d63]
+description = "ignore letter casing"
+
+[92ebcbb0-9181-4421-a784-f6f5aa79f75b]
+description = "ignore whitespace"
+
+[bc5f4203-00ce-4acc-a5fa-f7b865376fd9]
+description = "ignore punctuation"
+
+[68032b8b-346b-4389-a380-e397618f6831]
+description = "ignore numbers"
+
+[aa9f97ac-3961-4af1-88e7-6efed1bfddfd]
+description = "Unicode letters"
+include = false
+
+[7b1da046-701b-41fc-813e-dcfb5ee51813]
+description = "combination of lower- and uppercase letters, punctuation and white space"
+
+[4727f020-df62-4dcf-99b2-a6e58319cb4f]
+description = "large texts"
+
+[adf8e57b-8e54-4483-b6b8-8b32c115884c]
+description = "many small texts"

exercises/practice/parallel-letter-frequency/ParallelLetterFrequency.lean

@@ -0,0 +1,8 @@
+import Std
+
+namespace ParallelLetterFrequency
+
+def calculateFrequencies (texts : List String) : IO (Std.TreeMap Char Nat) :=
+  sorry
+
+end ParallelLetterFrequency

exercises/practice/parallel-letter-frequency/ParallelLetterFrequencyTest.lean

@@ -0,0 +1,15 @@
+name = "parallel-letter-frequency"
+version = "0.1.0"
+defaultTargets = ["ParallelLetterFrequencyTest"]
+testDriver = "ParallelLetterFrequencyTest"
+
+[[lean_lib]]
+name = "LeanTest"
+srcDir = "vendor/LeanTest"
+
+[[lean_lib]]
+name = "ParallelLetterFrequency"
+
+[[lean_exe]]
+name = "ParallelLetterFrequencyTest"
+root = "ParallelLetterFrequencyTest"

exercises/practice/parallel-letter-frequency/lakefile.toml

@@ -0,0 +1 @@
+leanprover/lean4:v4.25.2