summary description of the module system for lean

Stream: lean4

[Nicolas Rolland]

Will the new module system be true first class modules, as in 1ML style, with one language for modules and core expressions ?

If not, what is the technical flavor of those modules ?

More than a few languages have half-baked module systems, it would be a shame if Lean went that way.

[Henrik Böving]

The new module system is not at all about providing something you would see in an ML language. It's about providing a way to more clearly define which symbols defined within a Lean file are visible to importers of said file in order to enable things like faster (re)compilation and more clearly defined APIs.

[Kyle Miller]

My understanding is that some of the main use cases of ML-style modules, ad hoc polymorphism and abstraction, are handled by Lean's typeclass system. It's a different design space too, since there's not so much of a focus on decidable inference, and higher-kinded typeclasses are accepted too.

Lean 3 used to have parameters for uniformly parameterizing a set of declarations, which you might call a "half-baked ML module system", but that feature was not included in Lean 4, in favor of typeclasess.

Maybe something that's missing in Lean that's sort of handled by ML modules is first-class inductive type descriptions? Sometimes it would be nice to be able to have nested inductive types that are parameterized by another type. Something like this:

inductive_schema TreeOf (container : IndType (Type → Type)) (α : Type) : Type where
  | leaf : α → TreeOf container α
  | node : container (TreeOf container α) → TreeOf container α

structure Pair (α : Type) where
  (fst snd : α)

def BinaryTree (α : Type) := TreeOf Pair α
def Tree (α : Type) := TreeOf List α

The TreeOf type isn't a valid inductive type on its own. The kernel needs container to be a concrete inductive type to be able to check that the whole type is well-formed.

[Nicolas Rolland]

"module" is probably an overloaded term, and as Henrik was highlighting, lean modules might not refer to some other classical notion of modules which I thought they were.

By "half-baked module system" I mean a module system that is not backed by a clear theory and erasable to some calculus. 1ML modules, as far as I know, are just very useful syntactic constructs which stand for some encoding in system-F-omega (cf f-ing ) giving a clear interpretation of what they stand for.

As a design, modules in this language refers to not just some ad-hoc facility bolted on top, incompatible with the rest of the language but forms a coherent whole. Having one language for both has a few important benefits.

Type classes, in the language of modules, builds those modules for you through instance search, instead of you having to build and provide them by hand. It has its own limitation as it requires a global picture of the whole system, and is only available at compile time.

Of course each has benefit and negative side, but they both provide a dictionary of ad-hoc operation to some polymorphic code. Admittedly, mixing both is a challenge, but Lean folks are so amazing so far ;)