A Database

• Databases are the backbone of most applications
• We'll build a minimal key-value store from first principles
• Pure core that can be tested without touching disk (like archive)
• Builds on types from types, IO from io, and pipelines from pipes

Log Entries

-- A log entry: key paired with an optional value (none = deleted/tombstone)
abbrev LogEntry := String × Option String
abbrev Log := List LogEntry

• A log entry is a (key, value) pair where the value is optional
  • some "val": the key has this value
  • none: the key has been deleted (a tombstone)
• Log is just a list of entries, newest at the end
• abbrev creates transparent type aliases
  • LogEntry and String × Option String are interchangeable
• Like Git's commit history: each operation appends a new record
  • Nothing is ever truly deleted until you compact

Setting Values

-- Append a new value record to the log
def dbSet (log : Log) (key val : String) : Log :=
  log ++ [(key, some val)]

• dbSet appends a new (key, some val) entry to the log
• Does not modify or remove old entries — just adds at the end
• The log only grows; old values are shadowed, not overwritten
• Like Python's log.append((key, val)) but returning a new list instead of mutating

Deleting Values

-- Append a tombstone to mark a key as deleted
def dbDel (log : Log) (key : String) : Log :=
  log ++ [(key, none)]

• dbDel appends a tombstone: (key, none)
• The key still appears in the log, but its value is now none
• When queried, the tombstone indicates "this key was deleted"
• Like setting a deleted_at timestamp in a soft-delete pattern

Getting Values

-- Scan newest-first: return the first value found for the key
def dbGet (log : Log) (key : String) : Option String :=
  Option.join ((List.reverse log).findSome? (β := Option String) fun (k, v) =>
    if k == key then some v else none)

• dbGet scans the log newest-first (reversed) and returns the first match
• List.reverse log puts newest entries first
• findSome? returns the first some result from the scan function
  • The function returns some v when the key matches, none otherwise
• β := Option String is an explicit type annotation: Lean cannot infer the inner type of findSome? here without a hint
• Option.join flattens Option (Option String) to Option String
  • some (some "val") → some "val" (key found with value)
  • some none → none (tombstone found)
  • none → none (key not in log)
• Like Python's next((v for k, v in reversed(log) if k == key), None) but handling tombstones

Compaction

-- Compact the log: keep only the most recent entry for each key
def dbCompact (log : Log) : Log :=
  let (_, kept) := (List.reverse log).foldl (init := ([], [])) fun (seen, acc) (k, v) =>
    if seen.contains k then (seen, acc)
    else (k :: seen, (k, v) :: acc)
  kept

• dbCompact removes redundant entries, keeping only the newest per key
• Algorithm: scan reversed log, keep first occurrence of each key
  • seen tracks keys already encountered
  • kept accumulates deduplicated entries
• Scanning newest-first and prepending each new entry to kept restores original key order
  • The first new key encountered (newest "b") is prepended first, then newest "a" is prepended on top of it
  • Result: "a" before "b" — same order as the original log
  • Same trick as reversing a list with foldl and prepend
• Like Python's dict(reversed(log)) but preserving insertion order of last write
• Performance: dbCompact traverses the log twice — once to reverse it, once to fold over it
  • Both passes are O(n); the total cost is O(n) overall
  • For large logs this is fine; for hot paths you could compact incrementally instead

Checking Key Existence

-- Check if a key exists in the log (has a non-tombstone entry)
def dbExists (log : Log) (key : String) : Bool :=
  dbGet log key |>.isSome

• dbExists checks if a key has a non-tombstone value
• dbGet log key |>.isSome is true when the value is some _
• Returns false for both missing keys and tombstoned keys

Serialization

-- Serialize one entry as "key\tvalue\n" or "key\t\n" for tombstone
def serializeEntry (k : String) (v : Option String) : String :=
  s!"{k}\t{v.getD ""}\n"

-- Deserialize a "key\tvalue" line back into a LogEntry
def deserializeEntry (line : String) : Option LogEntry :=
  match line.splitOn "\t" with
  | [k, v] => some (k, if v.isEmpty then none else some v)
  | _       => none

• serializeEntry formats an entry as "key\tvalue\n"
  • For tombstones, value is empty: "key\t\n"
  • v.getD "" extracts the value string, defaulting to "" for none
• deserializeEntry parses a line back into a LogEntry
  • line.splitOn "\t" splits by the tab character
  • Returns none for malformed lines (wrong number of fields)
• Like CSV but with tabs as delimiters and no quoting

File-Backed Operations

-- Append one entry to a file
def appendEntry (path key : String) (val : Option String) : IO Unit := do
  let h ← IO.FS.Handle.mk path IO.FS.Mode.append
  h.putStr (serializeEntry key val)
  h.flush

-- Read entire log from a file
def readLog (path : String) : IO Log := do
  let text ← IO.FS.readFile path
  pure (text.splitOn "\n" |>.filterMap deserializeEntry)

• appendEntry opens a file in append mode and writes a serialized entry
  • IO.FS.Handle.mk path IO.FS.Mode.append opens a file for appending
  • h.putStr writes the string, h.flush ensures it's on disk
• readLog reads the entire file and parses each line
  • IO.FS.readFile path returns the file contents as a string
  • splitOn "\n" breaks into lines
  • filterMap deserializeEntry parses each line, discarding malformed ones
• The file format is append-only: each new entry goes at the end
  • You never rewrite the file in place
  • Compaction to a new file is the only time you write a complete log

Tests

-- Tests ---------------------------------------------------------------

-- Set and get
#guard dbGet (dbSet [] "x" "1") "x" == some "1"

-- Latest write wins
#guard dbGet (dbSet (dbSet [] "x" "1") "x" "2") "x" == some "2"

-- Tombstone
#guard dbGet (dbDel (dbSet [] "x" "1") "x") "x" == none

-- Compact reduces redundant entries
def messyLog : Log := [("a", some "1"), ("b", some "1"), ("a", some "2"), ("b", none)]
#guard dbCompact messyLog == [("a", some "2"), ("b", none)]

-- Exists check
#guard dbExists (dbSet [] "x" "1") "x"
#guard !dbExists (dbDel (dbSet [] "x" "1") "x") "x"
#guard !dbExists [] "x"

• #guard tests verify the pure operations
• Set and get: writing a value and reading it back
• Latest write wins: writing the same key twice returns the newer value
• Tombstone: deleting a key returns none
• Compaction: four entries reduce to two after deduplication
  • "a" has two writes — only the latest ("2") is kept
  • "b" has a write then a tombstone — only the tombstone is kept
• Existence: checks that dbExists returns correct boolean values

Running the Program

-- Entry point: demonstrate the database in memory and on disk
-- Run with: lean --run db/code.lean
def main : IO Unit := do
  -- In-memory
  let log := dbSet (dbSet (dbSet [] "name" "Lean") "lang" "functional") "name" "Lean 4"
  IO.println s!"In-memory log: {log}"
  IO.println s!"  dbGet log \"name\" = {dbGet log "name"}"
  IO.println s!"  dbGet log \"lang\" = {dbGet log "lang"}"
  IO.println s!"  Compacted:     {dbCompact log}"

  -- File-backed: write to a log file, then read it back
  let path := "db/demo.log"
  IO.println s!"\nWriting to {path}..."
  appendEntry path "hello" (some "world")
  appendEntry path "count" (some "1")
  appendEntry path "count" (some "2")   -- latest write wins
  appendEntry path "tmp"   none          -- tombstone
  let diskLog ← readLog path
  IO.println s!"  Read from disk: {diskLog}"
  IO.println s!"  dbGet \"hello\" = {dbGet diskLog "hello"}"
  IO.println s!"  dbGet \"count\" = {dbGet diskLog "count"}"
  IO.println s!"  dbGet \"tmp\"   = {dbGet diskLog "tmp"}"
  IO.println "Done."

• main demonstrates both in-memory and file-backed operations
• In-memory: creates a log, queries it, compacts it
• File-backed: writes entries to a file, reads them back, queries
  • IO.FS.removeFile is not available in the prelude, so we skip cleanup
• Compile and type-check with:
  • lake env lean db/code.lean
• Run interactively with:
  • lean --run db/code.lean
• The file-backed section creates a db/demo.log file
  • You can inspect it with cat db/demo.log

-- This scans front-to-back; should scan newest-first for latest-write-wins
abbrev LogEntry := String × Option String
abbrev Log := List LogEntry

def dbGet (log : Log) (key : String) : Option String :=
  Option.join (log.findSome? (β := Option String) fun (k, v) =>
    if k == key then some v else none)

#guard dbGet [("x", some "1"), ("x", some "2")] "x" == some "2"
#guard dbGet [("x", none), ("x", some "1")] "x" == none

-- This keeps the oldest value instead of the newest. Fix it.
abbrev LogEntry := String × Option String
abbrev Log := List LogEntry

def dbCompact (log : Log) : Log :=
  let (_, kept) := log.foldl (init := ([], [])) fun (seen, acc) (k, v) =>
    if seen.contains k then (seen, acc)
    else (k :: seen, (k, v) :: acc)
  kept

#guard dbCompact [("a", some "1"), ("b", some "1"), ("a", some "2"), ("b", none)]
        == [("a", some "2"), ("b", none)]

-- Tombstones serialize as "DELETED", but should serialize as empty string
def serializeEntry (k : String) (v : Option String) : String :=
  s!"{k}\t{v.getD "DELETED"}\n"

def deserializeEntry (line : String) : Option (String × Option String) :=
  match line.splitOn "\t" with
  | [k, v] => some (k, if v.isEmpty then none else some v)
  | _       => none

#guard deserializeEntry (serializeEntry "x" none) == some ("x", none)
#guard deserializeEntry (serializeEntry "x" (some "y")) == some ("x", some "y")

-- deserializeEntry always wraps the value in some; should detect tombstones
def deserializeEntry (line : String) : Option (String × Option String) :=
  match line.splitOn "\t" with
  | [k, v] => some (k, some v)
  | _       => none

#guard deserializeEntry "key\tvalue" == some ("key", some "value")
#guard deserializeEntry "key\t"      == some ("key", none)
#guard deserializeEntry "bad"        == none

-- Missing do block: two IO actions need sequencing
def appendEntry (path key : String) (val : Option String) : IO Unit :=
  let h ← IO.FS.Handle.mk path IO.FS.Mode.append
  h.putStr s!"{key}\t{val.getD ""}\n"
  h.flush

#eval appendEntry "db/test.log" "hello" (some "world")

-- Tombstones (none values) are not detected; Option.join is missing
abbrev LogEntry := String × Option String
abbrev Log := List LogEntry

def dbGet (log : Log) (key : String) : Option String :=
  (List.reverse log).findSome? (β := Option String) fun (k, v) =>
    if k == key then some v else none

#guard dbGet [("x", none), ("x", some "1")] "x" == none

-- Write a function that counts how many times a key appears in the log
abbrev LogEntry := String × Option String
abbrev Log := List LogEntry

def countEntries (log : Log) (key : String) : Nat :=
  0

#guard countEntries [("x", some "1"), ("x", some "2"), ("y", some "1")] "x" == 2
#guard countEntries [("x", none), ("x", some "1")] "x" == 2
#guard countEntries [] "x" == 0

-- Write a function that returns all unique keys in the log (deduplicated)
abbrev LogEntry := String × Option String
abbrev Log := List LogEntry

def keys (log : Log) : List String :=
  []

#guard keys [("a", some "1"), ("b", some "2"), ("a", some "3")] == ["a", "b"]
#guard keys [] == []

-- Write a function that merges two logs (second log's entries are newer)
abbrev LogEntry := String × Option String
abbrev Log := List LogEntry

def dbMerge (log1 log2 : Log) : Log :=
  []

#guard dbMerge [("x", some "1")] [("x", some "2")] == [("x", some "1"), ("x", some "2")]
#guard dbMerge [] [("a", some "1")] == [("a", some "1")]

-- Write a function that applies a batch of (key, value) updates to a log
abbrev LogEntry := String × Option String
abbrev Log := List LogEntry

def dbSet (log : Log) (key val : String) : Log :=
  log ++ [(key, some val)]

def batchSet (log : Log) (updates : List (String × String)) : Log :=
  log

#guard batchSet [] [("x", "1"), ("y", "2")] == [("x", some "1"), ("y", some "2")]
#guard batchSet [("x", some "0")] [("x", "1")] == [("x", some "0"), ("x", some "1")]

-- Write a function that returns the full history of values for a key
abbrev LogEntry := String × Option String
abbrev Log := List LogEntry

def dbHistory (log : Log) (key : String) : List (Option String) :=
  []

#guard dbHistory [("x", some "1"), ("x", none), ("x", some "2")] "x"
        == [some "1", none, some "2"]
#guard dbHistory [("y", some "1")] "x" == []

-- Write a function that formats the entire log as a readable string
abbrev LogEntry := String × Option String
abbrev Log := List LogEntry

def dbDump (log : Log) : String :=
  ""

#guard dbDump [("x", some "1"), ("y", none)]
        == "x: 1\ny: (deleted)"
#guard dbDump [] == ""