Emulating ML modules

Stream: Type theory

[Shreyas Srinivas]

To what extent do Lean structuresallow us emulate ML modules? In principle modules are implementable as dependent sum types. I know lean structures don't :

1. Act as a compilation unit
2. allow recursive fields (ofc you can use an inductive declaration instead)
3. Provide data hiding (like say a private keyword)

Is there more?

[Shreyas Srinivas]

This is a question that comes out of a discussion with Bhavik

[Eric Wieser]

Can you give a short example of an ML module using 2 or 3 that is hard to translate to Lean?

[Shreyas Srinivas]

I am not on a computer, but the example on the ocaml manual seems nice: https://ocaml.org/manual/5.2/recursivemodules.html

[Shreyas Srinivas]

(deleted)

[Shreyas Srinivas]

It allows you to encapsulate an algebraic data type with a function that acts on it.

[Shreyas Srinivas]

You can add data hiding by implementing extra functions in the struct that are not present in the signature. Those declarations are hidden

[Shreyas Srinivas]

I found a useful explanation of hiding: https://cs3110.github.io/textbook/chapters/modules/encapsulation.html

[Shreyas Srinivas]

It provides a lot of nice examples of how a module's hidden functions can be used by other module functions but not outside the module

[Andrés Goens]

FWIW, it looks like this is on the FRO's roadmap for this year, in language frontend. I think I remember reading/hearing something about private symbols being part of this, but I can't find it rigth now

[Andrés Goens]

(by private I understand that to be these hdden functions, or more generally, identifiers)

[Shreyas Srinivas]

the word "module" covers a wide spectrum of implementations and features from simple namespacing to the stuff I mentioned above. I don't think the FRO wants to implement ML style modules based on Sebastian's response to my question in one of the FRO community meetings in late 2023 or early 2024. My curiosity is purely about how much of it would fit into lean's type theory.

[Yuri]

Shreyas Srinivas said:

Is there more?

What about signatures? Where a signature is a type definition that specifies the interface of a module. It defines the types and values that a module must provide, without exposing implementation details. It acts as a contract separating interface from implementation 'in the large'.

[Shreyas Srinivas]

That's true. But if we ignore encapsulation and abstraction, a structure's instantiations are implementations, while the structure itself is a signature. Ofc this still does not give us file level modules and is not strictly a contract that hides implementation details

[Andrés Goens]

I guess I don't quite understand why this is about Lean's type theory, it doesn't really say anything about e.g. the visibility of identifiers accross files and stuff like that, does it? that's kind of orthogonal infrastructure isn't it?

[Shreyas Srinivas]

More than one source has told me that ML module types and their associated polymorphism and data hiding is incompatible with dependent types. I am trying to understand why and to what extent one can recover some nice features of ML modules

[Shreyas Srinivas]

What I understand (and have worked with formally) is a semantics of modules in system F as existential types.

[Horațiu Cheval]

Isn't Coq's module system similar? https://coq.inria.fr/doc/V8.18.0/refman/language/core/modules.html
And Coq does have dependent types.

[David Thrane Christiansen]

Shreyas Srinivas said:

while the structure itself is a signature

I think this is not quite accurate - ML signatures match ML structures _structurally_, which is to say that a given module can be compatible with signatures that didn't even exist when it was implemented. Using iterated sigma types to emulate a module system misses out on this, though it can be faked with fancy enough elaboration a la coercive subtyping.

[Shreyas Srinivas]

Okay so there is some structural subtyping rules that have to be emulated somehow

[Shreyas Srinivas]

So far my impression is that different features of ML modules are supported wholly or partially by different Lean constructs, but there is no unifying construct that adds all the above.

[David Thrane Christiansen]

Some of the features are supported to various degrees in various ways, yeah

[David Thrane Christiansen]

One thing you'd have a hard time getting is generative functors, which won't matter so much in a pure language