p-pavel

You are helping an experienced software engineer and former applied mathematics student orient himself in Lean 4.

Your goal is NOT to teach Lean as “just another functional programming language” and NOT to immediately turn the discussion into theorem proving or category theory.

Your goal is to help him build the correct mental model first.

Assume:

• strong engineering background
• mathematically literate

p-pavel

module

import Lean.Elab.Deriving.Basic
public meta import Lean.Elab.Command

open Lean Elab Command Meta

public section

/-- Generic final/tagless term shape (`repr` / `Sym` in Oleg's notes).

p-pavel

/** we can start with pure structure, not even thinking about specific types here's the structure of
  * a person
  */
trait PersonBase:
  val name, birthdate: Any
  val children: Any // What about this? we know more than just Any!

/** How about abstracting the idea of "something type-indexed"? */
object AbstractKindedTypes:
  opaque type K1[A]                                   = Any

p-pavel

trait Compiler:
  type Env = Map[String, BigDecimal]
  @throws[ParserError]
  def compile(formula: String): Env => BigDecimal


import scala.quoted.*
type Env  = Map[String, BigDecimal]
type E[A] = Expr[Env] ?=> Expr[A]

p-pavel

import io.circe.*
import literal.*
import cats.implicits.*
import NamedTuple.NamedTuple
import language.experimental.namedTuples

@main
def greet =
  type Person = (name: String, age: Int)
  val greeting = json"""{"name": "Joe", "age": 42}"""

p-pavel

trait Semigroup[T]:
  type C = T
  extension (a: C) def |+|(b: C): C

trait Monoid[T] extends Semigroup[T]:
  def empty: T

def mkMonoid[T: Semigroup as s](e: T) = 
  new:
    def empty = e

p-pavel

# This is the log of pauses from shitty N5105 Celeron running Karaf OSGi container
# most of the load comes from a component running inside the container that 
# does data acquisition, some simple processing, grouping and straming into
# TSDB (victoria metrics). The app is written in very high level style using 
# fs2/cats.effect without any optimisation attemts altogether
# it does ~ 3000 syscalls per second to obtain data. 
# No memory options at all, no attempts of tuning, vanilla G1 collector
# you can see <2ms pauses once in 40 seconds or so. OpenJDK 22 (GraalVM JIT would 
# help in this case a lot, btw, it's very good in allocation elimination)

p-pavel

//> using scala 3.5.1
//> using options -Wunused:all -deprecation -Xkind-projector -rewrite -source future-migration
//> using dep org.typelevel::algebra:2.12.0
//> using test.dep org.typelevel::discipline-munit:2.0.0
//> using test.dep org.typelevel::algebra-laws:2.12.0

import algebra.laws.LatticeLaws
import algebra.lattice.MeetSemilattice

given MeetSemilattice[String] with

p-pavel

trait PseudoSbt:
  type Setting[+_]
  type Key[+_]
  type Project

  /** context to extract value of type A from Setting[A]*/
  type ValueExtractor 

  /** Location in source file to be used to track definitions*/
  type Location 

p-pavel

//>using lib "org.typelevel::cats-effect:3.5.1"
import cats.effect.*
import cats.implicits.*

object HowToRunJobsInParallel extends IOApp.Simple:
  def jobConstructor(r: Ref[IO, Long])(jobId: Any) = r
    .modify(n => (n + 1, n))
    .flatMap(v => IO.println(s"Job $jobId processed task $v"))
  def run                               =
    for