Transient notes for someone fluent in cats-effect/fs2 who wants to write efficient, idiomatic Lean.
This is based on Lean 4.29 sources and Std as installed in this workspace.
Lean's concurrency model is much closer to "native OS threads plus runtime tasks" than to cats-effect's fiber runtime.
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:
| 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). |
| /** 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 |
| 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] |
| 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}""" |
| 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 |
| # 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) |
| //> 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 |
| 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 |
