Sorry, I have a “FP vs OOP debates miss the point” draft blog post in my head
for years at this point, so I feel like I need to pour some fire and brimstone
of my own. The “point” being modules of course!
So, yeah, modules are not discussed nearly enough. This is the most important
thing when building large systems, and yet almost everyone treats them as just
something extra, just as a place to store the actually interesting stuff in.
But I think there are two competing views of what the module is. On is a
type-theoretician view, that a module is one of the many inhabitants of a type
system zoo. The other is a view of practitioner, compiler writer, that the
module is a chunk of code, which can be separately compiled, and then a bunch of
independent modules can be linked together to form a coherent program.
I want to make a strong claim that it’s the second view that is actually
important for practical software, and that, historically, we only have been
touching this view as a side effect of fancy programming-paradigm-of-the-day
modules.
To give a specific example, I attribute the success of OOP to the fact that
classes make poor modules. Like, of course
Package java.util;
class ArrayList<T> {
...
}
is not really a great module for all the specified reasons, but it is a great
improvement over just having a bunch of my_lib_array_list_push() functions in
the global namespace.
Similarly, I think ML modules are an improvement over classes, as they allow,
eg, having several types in a single module, but, like classes, they also bring
too much unrelated stuff. To be clear, those extra abstraction capabilities,
like inheritance for the classes and functors for the modules, are important to
have for “programming in the small” somewhere in the language, but it would be
a mistake to re-use them for programming in the large.
My somewhat provocative list of languages to learn modularity from would be C,
Rust and Swift :-) I don’t think that any of them nails the module system
exactly, but, of the three, Rust is the one with the biggest and the most
consequential ideas.
Here’s what I think what matters in the module system for programming in the
large.
First, modules should be concrete. Abstraction, substitution principle, and
reusability are very useful in a pinch, but most code out there is doing some
specific concrete thing. https://crates.io/crates/ has 109786 concrete modules,
and they absolutely do compose beautifully in practice. Diagram in
https://www.tedinski.com/2018/02/27/the-expression-problem.html is very useful.
The bulk of the software (especially “in the large”) is in the closed-closed
quadrant.
Second, module systems should be two-level. There should be a distinction
between a library and a module. The difference between the two is that modules
allow circular dependencies and libraries don’t. Or rather, you would have
circular dependencies somewhere, if you allow recursion at all, so you need to
place some boundary on it. The right granularity here is a collection of files
developed and compiled together as a single unit. Rust nails this requirement,
with crates and modules being the two levels (although the mapping between
modules and files could have been better).
Third, there should no global namespace of symbols. If A uses B, then “B”
belongs to the dependency edge between the two. Again, rust handles this
beautifully. OCaml fails: modules are compiled in order, and earlier modules are
visible to the latter ones.
Fourth, modules should have well-defined public interface (while still being
concrete!). Visibility should be tied to modules, rather than classes. Here,
Rust’s record it mixed. It used to have .mli-like .crate files, but they
were removed. The all important pub(crate) visibility was added after 1.0,
so it doesn’t play as central role as it should. rustdoc somehow compensates
for that by automatically compiling modules’ interface. C, with .h and ML with
.mli are the languages to learn from here
Fifth, modules should allow separate compilation. Here C is the language to
learn from, C’s compilation model is actually great for that language. But
today’s king is Swift, as it showed the world how to reconcile monomorphisation
and separate compilation.
OCaml fails: modules are compiled in order, and earlier modules are visible to the latter ones.
I’m not sure that’s quite correct. Of the top of my head in Ocaml you need the interface of dependencies to be compiled before you can compile a module — not the dependencies themselves. So as long as you compile the interfaces first (and those do need to be compiled in a specific order), the modules themselves can be compiled in any order.
OCaml does well on separate compilation point. OCaml fails at global namespace: what’s logically visible in you program is determined by the physical compilation order. It should be the opposite! Logical dependencies between modules should dictate compilation order. ocamldep is a horrible thing: no sane module system should rely on heuristic parsing to figure out dependencies between modules! This somehow feels even worse than C, as that doesn’t depend on order of compilation, and dependencies are explicitly specified via header inclusion.
My, yes, good point. I remember having some trouble because of that.
Logical dependencies between modules should dictate compilation order.
Yes, definitely. My dream there is that I just point the compiler to the entry point, and it pulls the dependencies for me, no further thinking required. And if my dependency graph is broken, or if a dependency is unreachable, the compiler would just tell me.
Though perhaps that’s not quite possible in a world where you also have to talk to C. I’m not sure.
https://crates.io/crates/ has 109786 concrete modules, and they absolutely do compose beautifully in practice.
I’d say they compose very well compared to C or C++ libraries; the process and experience of using a library is indeed seamless with Cargo. On the other hand, trying to write something in #[no_std] and bringing in new libraries is a minefield; async ecosystem is fragmented into tokio/async_std/smol niches (at least as of now). Having “interface crates” like http or log is definitely an improvement, but I wish for more fine-grained interface modularity. I wish that libraries would be no_std by default, explicitly taking a capability-like implementation of a dependency (e.g. https://crates.io/crates/filesystem or an allocator) instead. A crate A and a crate B might describe one thing in slightly different ways and often there’s no flexible easy way to bridge them unless you make both depend on it. Many of those 109786 crates are just glue crates between other crates.
Maybe these are symptoms of inherent technical complexity. Or maybe some kind of structural compatibility of types and traits or some other flexible glue can help (while keeping abstractness in check, ideally).
C, with .h and ML with .mli are the languages to learn from here
I’m on the fence on this one. Having a strict separate interface description sounds like a good thing in theory. On the other hand, the programmer is forced to duplicate definitions, to update them in sync, to switch to the interface file to see if a top-level entity is public. The current solution gives the programmer some flexibility: they can either use it as it is or implement a separate public interface file manually via pub mod and reexporting items with pub use.
I do agree with the other points. I wish Rust leaked less low-level details (like a fixed memory layout) in crate interaces and was more like Swift in making boundaries more abstract and flexible.
This is a good writeup. It leans a little too much on the Milner doctrine that “well-typed programs cannot go wrong”, but it’s a nice contrast to Java interface tutorials.
Also, let me remind you that a sufficiently powerful type system lets you stuff arbitrary correctness requirements in the type, so we can read “M has type A” as saying “M is correct.”
This is sleight of hand. If working in OCaml or SML, then the type system only lets you specify first-order membership predicates. Here is an old series of examples using Haskell, but they can be translated into strict ML without issues; each example demonstrates a hole in the typical ML type system.
For, in a sufficiently powerful type system, every useful fact that can be stated about a function or module can be stated as part of its type.
This is a goalpost that begs to be moved as we consider which facts are useful. Gödel’s Incompleteness applies to type systems which have type-level Peano arithmetic, after all.
…this funky S extends Stack<S> business…
This is the curiously recurring template pattern! I bet that your observation works both ways – when we find CRTP in C++ or Java codebases, we can analyze it in terms of recursively-bounded quantification.
We have a module N which uses some module M, but only through its type (interface) A. M can be replaced by any other module with the same type, and N will continue to work. That’s modularity.
That is naturality! Consider M as a functor on types; M takes a collection of parameter types and returns a parameterized type. N is a collection of functors, one for each possible M, such that we can naturally deform any particular N(M(p1)) into N(M(p2)) for any particular p1 or p2 used to parameterize M; the deformation is just syntactic replacement of the p1 type with p2! This is the rationale behind the word “functor” in OCaml.
If working in OCaml or SML, then the type system only lets you specify first-order membership predicates.
Ah, but I’m not talking about SML or OCaml there. I was talking about OCaml hypothetically extended with dependent types. And really, I had a dependently-typed language like Coq or Agda in mind. It’s not that “well-typed programs cannot go wrong”; it’s that, in Coq or Agda, the “type” can contain a full correctness theorem!
Gödel’s Incompleteness applies to type systems which have type-level Peano arithmetic,
Pretty funny. Touché that I hadn’t been thinking of Gödelian concerns when writing this. I’ll be interested in an example where this comes up for real.
A friend once quipped “If it’s nontrivial to prove your program terminates, your program probably doesn’t run,” and that about sums up my attitude to the relevance of undecidability.
I bet that your observation works both ways – when we find CRTP in C++ or Java codebases, we can analyze it in terms of recursively-bounded quantification.
I definitely recommend reading Cook’s (RIP) original F-bounded polymorphism paper. I think it’s on the simpler side for type theory paper, but I haven’t seen any other write-ups explaining it.
A friend once quipped “If it’s nontrivial to prove your program terminates, your program probably doesn’t run,” and that about sums up my attitude to the relevance of undecidability.
That’s a fine perspective, honestly. I might be grouchy about this because lately I’ve been working in a total functional context; my programs always terminate, but sometimes it takes longer than I’m willing to wait! Similarly, I hear sometimes from folks working in dependently-typed languages that the compiler could prove something, but it would take too long for their taste. (I personally didn’t have that issue when using Coq or Idris.)
This is a great write-up, but I often find these module-focused posts frustrating because they do two things when comparing OCaml to Haskell:
They discuss how Type Classes are global in scope and how challenging it is to solve this problem, but they never discuss newtype, which does solve the problem with a little boilerplate.
They never discuss the amount of explicit boilerplate involved at the call site when using the module-functor-based approach. Just try printing an arbitrary type in OCaml without a ppx.
I understand the theoretical advantages of modules, but in my opinion type classes are almost as good 90% of the time with no boilerplate, and the other 10% of the time newtype can be used with an equivalent amount of boilerplate as every functor invocation.
What am I missing here? As an OCaml newbie, I feel like there’s a counterpoint to this argument, but I’m not seeing it.
Yeah, this post probably does sound like it was written by an ML afficionado. It was actually written by a hardcore Haskeller of over 10 years who was even on the PC of the Haskell Symposium last year, although I was explaining a blog post by an SML maximalist.
But actually, the lack of ML-style modules has been at the top of my Haskell wishlist for about as long as I’ve been using it, next to the ability to have finer-grained control of typeclass instantiation at use-sites. I was pretty disappointed by Backpack for that reason; they missed their chance to fix this problem, and Backpack is still little used a decade later.
A big difference between typeclasses and modules is that typeclass instances are chosen per function and need to be specified. Module implementations can be chosen at the top level.
I have two implementations of the memoization library, and expect at some point to add a third based on concurrent hash tables. I switch between them by commenting out an import statement at the top. There is nothing in the type system that forces these two modules to have the same interface. If I wanted better support for switching between them, I would add a build flag and #ifdef’s.
How would I do this with typeclasses? The normal way is to add a typeclass constraint to every single function that needs it. I would go further and add said parameter to many that don’t, because it’s an implementation detail whether a given operation is memoized, and interfaces should be stable. Now my choices are to either wrap each ECTA in an ECTAUsingSingleThreadedMemoization or ECTAUsingConcurrentMemoization newtype, to add a new proxy parameter to every function, or to go full on AllowAmbiguousTypes and force every caller to give a type parameter specifying the memoization library used. Also, did I mention that memoization libraries are based on global state (either “not very Haskelly” or “extremely Haskelly,” depending on your perspective), and that if you supply different instances at different call-sites, the code will function fine, but have a silent performance bug. This puts a burden on the caller to maintain consistency in which the easiest solution is for the caller to….use a module system! The final option is to make the ECTA data structure itself have a phantom type parameter used to select the memoization implemenatiton. E.g.: instead of passing around an ECTA, you always pass around an ECTA Concurrent or an ECTA SingleThreaded.
In any of these, you are exposing implementation details to callers, or even to transitive callers. They are based on universally-quantified types, when I need existentially-quantified types, synonymous with information-hiding.
How to get existentials? I can go object-oriented. In Haskell, that can look like stuffing a typeclass instance inside a GADT. But that doesn’t work for binary functions; I wouldn’t be able to guarantee that, when intersecting two ECTAs, they use the same memoization library (and they would thus use different global state when they need to use the same).
But, yeah, I totally agree with you about the poor ergonomics of actually writing all your code as a module-valued function (functor) over all its dependencies. I think this could be fixed rather easily using a new kind of import or open statement, but the MLers haven’t yet.
I am adding this answer to a Q&A on the blog post.
Oh hey, I didn’t realize that jkoppel (you) had written this post! I’ve listened to you on several podcasts and I’m very impressed with your work. Thanks for this excellent response, I’ll take some time to digest it and the linked materials you provided. Perhaps this is the push I need to try writing real programs with OCaml.
I, too, think that it is perfectly reasonable to draw conclusions about the best practices in computer science from a 10 line module written in a language that is unused outside of academia.
I actually regret the snark of my previous ^ comment.
I do NOT want to discourage young people in academia from writing things and pushing ideas. And snark like mine is a great way to discourage people from “putting themselves out there”. Shame on me for being that asshole. In my defense, I like to write controversial things online for no apparent reason.
What I was trying to say (hidden in the snark) was that it’s dangerous to accept conclusions from experiments in the small. Yet those same experiments can be excellent catalysts for building experiments in the large, and sometimes the key to discovering scalable solutions is found in the elegance of the small (metaphorical) crystal that shows how to solve some challenge of composition in the large.
So while I hesitate to accept grandiose ideas based on small examples, particularly those from carefully controlled environments like academia, I also want to celebrate that process of learning and experimenting and sharing ideas, which academia excels at.
I hope this exposition at least slightly redeems my previous comment.
There are no experiments in this post. There are several small examples used for teaching a well-known concept. Everyone, industry and academia, uses small examples. Complaining about them can be used to attack any explanation whatsoever.
There are definitely many ideas in programming and computer science that can be approached from a purely mathematical perspective, where the math models the problem closely
I’d argue that module systems are not one of them. Any counter-argument to that? It seems obvious
For example
compilation time matters
Distributed upgrade without global knowledge matters.
A module system that’s useful for 1000 line programs is not necessarily useful for 1M line programs
1M and 10M line programs are where the real test of a module system is (e.g. browsers, compilers, kernels, and I would even bet the Glasgow Haskell Compiler itself is getting up there, although I haven’t looked)
That’s an interesting article. You did well showing how many languages try to patch on the effects of a good, module system. Those patch-ups do extra damage. I was looking at functional programming via preprocessor in C just last month. I think the scariest thing about such hacks are how there are systems composing that don’t really understand what each other are doing. There’s no consistency protection across those separate formalisms or applications. If anything, it’s like we’d need real, module theory with formal specs for each thing we used to fake the modules. We don’t have that either. So, it might always be a mess to deal with.
I especially loved how you illustrated that that many interfaces might have satisfied an implementation. I’ve been thinking of software rewriting again (eg language-to-language translation). Others are using machine learning to improve software. Tools aiming for one-to-one correspondence between an original and improved version might write different, unintended pieces of software. While they’d treat it as a bug, it might be inherent to how they try to guess interfaces (or other abstract info) from the implementations people feed them. Issues like you mentioned might mean there are upper limits to what we can do.
One thing missing, but almost there in “Not Just for…” section, is you can publish a clean, prototype module as documentation along with code in a different language. This is basically the old concept of prototyping with a high-level language before implementing in a low-level language. Instead, we’re applying it as a specification technique for interfaces which might be easier to learn than full, formal specification. It would help if the readers in the messy language knew the cleaner language. If they didn’t, it could be an excuse to expose them to unfamiliar ideas that broaden their mind.
On your Trinity reference, I think verses 19-20 here apply. God said He designed all of creation to testify to His presence. Thinking of articles here, one way is that what should be a random mess of a universe follows specific laws that follow mathematical/logical rules like you shared. Many of the same maths show up in seemingly-unrelated things like how an artist leaves repeating signatures on their work. While they should changed often, the machinery consistently works with no deviations from its specs. God said in v35-36 here that the fixed laws, which secure our existence physically, were a reminder that He’d keep a greater promise to hold us secure forever. If we repent of our lives’ many sins and put our faith in Jesus Christ (God) instead.
I put up a short explanation with proof of that up here. I hope you receive His free gift, old friend. If you do, you get to meet the Creator of those abstractions, know Him personally, and explore the depths of His designs over eternity.
The “computational trinity” is an older name for what we now call the computational trilogy, a grand connection between logic/syntax/type theory, semantics/category theory, and computation. Harper is quoted on that page, too:
Computational trinitarianism entails that any concept arising in one aspect should have meaning from the perspective of the other two. If you arrive at an insight that has importance for logic, languages, and categories, then you may feel sure that you have elucidated an essential concept of computation–you have made an enduring scientific discovery.
So, when we consider syntactic modules as presented in the blog post, we should also consider the category-theoretic meaning of modules.
The “Holy Trinity” is an older name for God as one being of three persons. People have a history of taking his name in vain or re-applying it in different ways. His names, like His creation, are meant to give Him glory. I just point it back to Him when I see it.
That said, I thank you for sharing the link. It’s very interesting. On top of mathematical education, there’s even another theological concept in it which is potentially useful:
“The central dogma of computational trinitarianism holds that Logic, Languages, and Categories are but three manifestations of one divine notion of computation. There is no preferred route to enlightenment: each aspect provides insights that comprise the experience of computation in our lives.”
This is great wording for a concept that’s hard to explain. One indeed similar to the Trinity. We have God existing as His own essence with all His properties (or nature). Then, each person has their own attributes, sets an example for us, takes seemingly-independent action, and are highly interdependent. After describing specifics, one might say something similar to the above quote: “each aspect provides insights that represent the experience of God moving in our lives.”
This might be another example where God creates things on earth to be shadows of things in heaven to help us understand them and marvel at Him.
Thanks for sharing a second off-topic comment! I appreciate it. In return, here is a quick proof that Jehovah and other omnipotent beings don’t exist. First, consider potentially-infinite matrices of Booleans. If any row of such a matrix is all true, then there cannot be any column which is all false, and vice versa, and vice versa; proofs left to the reader.
Create an open tournament. By tradition, it will be a rock-throwing tournament. Entrants can register rocks which will be thrown, and also champions which will throw rocks. A judgemental person decides whether each champion/rock pair is a successful throw, and tallies the result in a matrix of Booleans. Then, by the above lemma, there cannot be an entrant who simultaneously registers an unthrowable rock and also a champion who can throw any rock whatsoever. Dually, there also cannot be an entrant who simultaneously registers an always-throwable rock and also a champion who is unable to throw rocks. Proof: what does the judge tally after each attempt? This is just a rigorous version of the paradox of the stone, with fluff removed.
In general, the logical relations between our observable reality are sufficient to exclude the possibility of omnipotence. Similar basic statements can be used to exclude trivialism, solipsism, and dialethism/paraconsistency from our reasoning, too.
The article is the topic. Many authors like to drag our faith into unrelated writing. So, my response was to multiple angles. Plus, just out compassion for my old buddy who submitted it. I’d like to see the man be saved by the very God he referenced. :) Back to the tangent.
Re proof. Although interesting, your proof ditches the scientific method for conjecture based on imagined worlds. Science says we must observe our universe’s attributes, how things work in it, build hypotheses based on those observations, test them with controlled experiments, and have skeptical parties independently replicate that. The evidentiary method used in historical situations at least requires corroborated evidence from honest observers. Divine revelation with prophecy and miracles works similarly to the evidentiary method. So, let’s also start with observation of the real world.
We see a universe whose parameters are very fine-tuned. Even non-believers argue this point. They tend to dodge the implication. I wrote that we never see such well-maintained order emerge from chaos. If working from observations, we’re forced to default on God made the universe.
We struggle to make physics work precisely in tiny areas (example). Our AI’s, whether NN or GA, require lots of intelligent design to even operate, much less work correctly. People struggle to develop, optimize, and verify logics with consistency. We marvel at mathematicians and engineers who pull off these feats. How much more should we marvel at God who drives all of that to work with no failures?! We say those people’s output was clearly design as they fought an uphill battle against chaos. Then, we treat the universe like we could make it by shaking up a shoebox long enough. Logically inconsistent. Why do we do this?
“Boast no more so very proudly, Do not let arrogance come out of your mouth; For the Lord is a God of knowledge, And with Him actions are weighed.” (1 Sam. 2:3)
“The LORD Almighty has a day in store for all the proud and lofty, for all that is exalted (and they will be humbled).” (Isa. 2:12)
I was the most guilty of this. Although a good tool, science has failed countless times with so many rewrites of our books. Empirical observation should lead scientists to be the most humble of all people with carefully-worded statements they know might be disproven the next day. Instead, they tell believers what’s definitely true, what’s definitely not possible, and often believe theories with neither observation nor skeptical replication (aka faith). Many mock people who believe in God with far greater evidence than exists for some theories they have much confidence in.
God’s Word said people like me were arrogant people who wanted to be god, had no interest in submitting to a real one, and ignored all the evidence He existed. When God judged how we lived our lives, we’d still be trying to argue with Him about why our moral theories and lifestyles made more sense. The proof was all around us but we already saw god in the mirror. We’d speak so certainly about our beliefs due to our wicked, arrogant hearts. I had to repent.
It gets better still! If you humble yourself and seek God, then He gives you a shortcut around all of those proof requirements. God’s Word says the Father draws us in, “my sheep hear my voice,” and faith comes by hearing the Word. After digging into His Word, God will supernaturally do something that makes it click at some point. Then, a testable prediction is that we’re transformed from inside out by His power. We may also experience answered prayers and miracles. That one message, without modification, has gotten those same results in around 2,000 people groups for thousands of years. It’s power is proven.
Pray to God that He reveals Himself and saves you and start in John. You’ll meet Him. Then, what happens to His followers in His Word will happen to you as well.
Thanks for a third off-topic comment. Let’s see if you’re really a person of science.
Rock-throwing tournaments are completely scientific. Nothing I described is impossible to build in a laboratory, and because Jehovah doesn’t exist, of course they can’t show up and participate in a contradictory fashion. You’re going to have to reply with logic and maths if you don’t like the rock-throwing tournament!
Quantum mechanics is incompatible with omniscience, all-knowing, all-seeing, or any other similar superpower. The Kochen-Specker lemma shows that there are properties of particles which are not locally determined, and thus cannot be observed without measurement. A Stern-Gerlach device allows us to make such a measurement. The same device shows that particles midway through the device, accelerated but not yet measured, are indeterminate – if some deity were measuring them, then the particles would be deflected measurably.
To be blunt: You’re using a device laden with semiconductors, and the theories which were used to design that device have no room for omniscient beings. Also, the device was programmed using theories of logic which have no room for omnipotent beings and can only implement the realizable theorems.
Not gonna lie, most of the math/theory kinda went over my head here. But it was nice to get some validation that the way that I think about modules, as a sort of type boundary, in a language that is kinda pretty far from this level of theory (Python) is kinda not that wrong.
Sorry, I have a “FP vs OOP debates miss the point” draft blog post in my head for years at this point, so I feel like I need to pour some fire and brimstone of my own. The “point” being modules of course!
So, yeah, modules are not discussed nearly enough. This is the most important thing when building large systems, and yet almost everyone treats them as just something extra, just as a place to store the actually interesting stuff in.
But I think there are two competing views of what the module is. On is a type-theoretician view, that a module is one of the many inhabitants of a type system zoo. The other is a view of practitioner, compiler writer, that the module is a chunk of code, which can be separately compiled, and then a bunch of independent modules can be linked together to form a coherent program.
I want to make a strong claim that it’s the second view that is actually important for practical software, and that, historically, we only have been touching this view as a side effect of fancy programming-paradigm-of-the-day modules.
To give a specific example, I attribute the success of OOP to the fact that classes make poor modules. Like, of course
is not really a great module for all the specified reasons, but it is a great improvement over just having a bunch of
my_lib_array_list_push()functions in the global namespace.Similarly, I think ML modules are an improvement over classes, as they allow, eg, having several types in a single module, but, like classes, they also bring too much unrelated stuff. To be clear, those extra abstraction capabilities, like inheritance for the classes and functors for the modules, are important to have for “programming in the small” somewhere in the language, but it would be a mistake to re-use them for programming in the large.
My somewhat provocative list of languages to learn modularity from would be C, Rust and Swift :-) I don’t think that any of them nails the module system exactly, but, of the three, Rust is the one with the biggest and the most consequential ideas.
Here’s what I think what matters in the module system for programming in the large.
First, modules should be concrete. Abstraction, substitution principle, and reusability are very useful in a pinch, but most code out there is doing some specific concrete thing. https://crates.io/crates/ has 109786 concrete modules, and they absolutely do compose beautifully in practice. Diagram in https://www.tedinski.com/2018/02/27/the-expression-problem.html is very useful. The bulk of the software (especially “in the large”) is in the closed-closed quadrant.
Second, module systems should be two-level. There should be a distinction between a library and a module. The difference between the two is that modules allow circular dependencies and libraries don’t. Or rather, you would have circular dependencies somewhere, if you allow recursion at all, so you need to place some boundary on it. The right granularity here is a collection of files developed and compiled together as a single unit. Rust nails this requirement, with crates and modules being the two levels (although the mapping between modules and files could have been better).
Third, there should no global namespace of symbols. If A uses B, then “B” belongs to the dependency edge between the two. Again, rust handles this beautifully. OCaml fails: modules are compiled in order, and earlier modules are visible to the latter ones.
Fourth, modules should have well-defined public interface (while still being concrete!). Visibility should be tied to modules, rather than classes. Here, Rust’s record it mixed. It used to have
.mli-like.cratefiles, but they were removed. The all importantpub(crate)visibility was added after1.0, so it doesn’t play as central role as it should.rustdocsomehow compensates for that by automatically compiling modules’ interface. C, with.hand ML with.mliare the languages to learn from hereFifth, modules should allow separate compilation. Here C is the language to learn from, C’s compilation model is actually great for that language. But today’s king is Swift, as it showed the world how to reconcile monomorphisation and separate compilation.
I think Oberon ticks most of your boxes. It’s an example of module system “done right” that was mostly ignored.
I’m not sure that’s quite correct. Of the top of my head in Ocaml you need the interface of dependencies to be compiled before you can compile a module — not the dependencies themselves. So as long as you compile the interfaces first (and those do need to be compiled in a specific order), the modules themselves can be compiled in any order.
OCaml does well on separate compilation point. OCaml fails at global namespace: what’s logically visible in you program is determined by the physical compilation order. It should be the opposite! Logical dependencies between modules should dictate compilation order.
ocamldepis a horrible thing: no sane module system should rely on heuristic parsing to figure out dependencies between modules! This somehow feels even worse than C, as that doesn’t depend on order of compilation, and dependencies are explicitly specified via header inclusion.My, yes, good point. I remember having some trouble because of that.
Yes, definitely. My dream there is that I just point the compiler to the entry point, and it pulls the dependencies for me, no further thinking required. And if my dependency graph is broken, or if a dependency is unreachable, the compiler would just tell me.
Though perhaps that’s not quite possible in a world where you also have to talk to C. I’m not sure.
I’d say they compose very well compared to C or C++ libraries; the process and experience of using a library is indeed seamless with Cargo. On the other hand, trying to write something in
#[no_std]and bringing in new libraries is a minefield; async ecosystem is fragmented into tokio/async_std/smol niches (at least as of now). Having “interface crates” likehttporlogis definitely an improvement, but I wish for more fine-grained interface modularity. I wish that libraries would beno_stdby default, explicitly taking a capability-like implementation of a dependency (e.g. https://crates.io/crates/filesystem or an allocator) instead. A crate A and a crate B might describe one thing in slightly different ways and often there’s no flexible easy way to bridge them unless you make both depend on it. Many of those 109786 crates are just glue crates between other crates.Maybe these are symptoms of inherent technical complexity. Or maybe some kind of structural compatibility of types and traits or some other flexible glue can help (while keeping abstractness in check, ideally).
I’m on the fence on this one. Having a strict separate interface description sounds like a good thing in theory. On the other hand, the programmer is forced to duplicate definitions, to update them in sync, to switch to the interface file to see if a top-level entity is public. The current solution gives the programmer some flexibility: they can either use it as it is or implement a separate public interface file manually via
pub modand reexporting items withpub use.I do agree with the other points. I wish Rust leaked less low-level details (like a fixed memory layout) in crate interaces and was more like Swift in making boundaries more abstract and flexible.
This is a good writeup. It leans a little too much on the Milner doctrine that “well-typed programs cannot go wrong”, but it’s a nice contrast to Java interface tutorials.
This is sleight of hand. If working in OCaml or SML, then the type system only lets you specify first-order membership predicates. Here is an old series of examples using Haskell, but they can be translated into strict ML without issues; each example demonstrates a hole in the typical ML type system.
This is a goalpost that begs to be moved as we consider which facts are useful. Gödel’s Incompleteness applies to type systems which have type-level Peano arithmetic, after all.
This is the curiously recurring template pattern! I bet that your observation works both ways – when we find CRTP in C++ or Java codebases, we can analyze it in terms of recursively-bounded quantification.
That is naturality! Consider
Mas a functor on types;Mtakes a collection of parameter types and returns a parameterized type.Nis a collection of functors, one for each possibleM, such that we can naturally deform any particularN(M(p1))intoN(M(p2))for any particularp1orp2used to parameterizeM; the deformation is just syntactic replacement of thep1type withp2! This is the rationale behind the word “functor” in OCaml.Ah, but I’m not talking about SML or OCaml there. I was talking about OCaml hypothetically extended with dependent types. And really, I had a dependently-typed language like Coq or Agda in mind. It’s not that “well-typed programs cannot go wrong”; it’s that, in Coq or Agda, the “type” can contain a full correctness theorem!
Pretty funny. Touché that I hadn’t been thinking of Gödelian concerns when writing this. I’ll be interested in an example where this comes up for real.
A friend once quipped “If it’s nontrivial to prove your program terminates, your program probably doesn’t run,” and that about sums up my attitude to the relevance of undecidability.
I definitely recommend reading Cook’s (RIP) original F-bounded polymorphism paper. I think it’s on the simpler side for type theory paper, but I haven’t seen any other write-ups explaining it.
Good point!
That’s a fine perspective, honestly. I might be grouchy about this because lately I’ve been working in a total functional context; my programs always terminate, but sometimes it takes longer than I’m willing to wait! Similarly, I hear sometimes from folks working in dependently-typed languages that the compiler could prove something, but it would take too long for their taste. (I personally didn’t have that issue when using Coq or Idris.)
This is a great write-up, but I often find these module-focused posts frustrating because they do two things when comparing OCaml to Haskell:
They discuss how Type Classes are global in scope and how challenging it is to solve this problem, but they never discuss
newtype, which does solve the problem with a little boilerplate.They never discuss the amount of explicit boilerplate involved at the call site when using the module-functor-based approach. Just try printing an arbitrary type in OCaml without a ppx.
I understand the theoretical advantages of modules, but in my opinion type classes are almost as good 90% of the time with no boilerplate, and the other 10% of the time
newtypecan be used with an equivalent amount of boilerplate as every functor invocation.What am I missing here? As an OCaml newbie, I feel like there’s a counterpoint to this argument, but I’m not seeing it.
Hi restrictedchoice!
Yeah, this post probably does sound like it was written by an ML afficionado. It was actually written by a hardcore Haskeller of over 10 years who was even on the PC of the Haskell Symposium last year, although I was explaining a blog post by an SML maximalist.
But actually, the lack of ML-style modules has been at the top of my Haskell wishlist for about as long as I’ve been using it, next to the ability to have finer-grained control of typeclass instantiation at use-sites. I was pretty disappointed by Backpack for that reason; they missed their chance to fix this problem, and Backpack is still little used a decade later.
A big difference between typeclasses and modules is that typeclass instances are chosen per function and need to be specified. Module implementations can be chosen at the top level.
So here’s an example of where I want modules: https://github.com/jkoppel/ecta/blob/main/src/Data/ECTA/Internal/ECTA/Operations.hs#L73 . This for my implementation of equality-constrained tree automata (ECTAs), from my ICFP ’22 paper “Searching Entangled Program Spaces.”
I have two implementations of the memoization library, and expect at some point to add a third based on concurrent hash tables. I switch between them by commenting out an import statement at the top. There is nothing in the type system that forces these two modules to have the same interface. If I wanted better support for switching between them, I would add a build flag and #ifdef’s.
How would I do this with typeclasses? The normal way is to add a typeclass constraint to every single function that needs it. I would go further and add said parameter to many that don’t, because it’s an implementation detail whether a given operation is memoized, and interfaces should be stable. Now my choices are to either wrap each ECTA in an ECTAUsingSingleThreadedMemoization or ECTAUsingConcurrentMemoization newtype, to add a new proxy parameter to every function, or to go full on AllowAmbiguousTypes and force every caller to give a type parameter specifying the memoization library used. Also, did I mention that memoization libraries are based on global state (either “not very Haskelly” or “extremely Haskelly,” depending on your perspective), and that if you supply different instances at different call-sites, the code will function fine, but have a silent performance bug. This puts a burden on the caller to maintain consistency in which the easiest solution is for the caller to….use a module system! The final option is to make the ECTA data structure itself have a phantom type parameter used to select the memoization implemenatiton. E.g.: instead of passing around an
ECTA, you always pass around anECTA Concurrentor anECTA SingleThreaded.In any of these, you are exposing implementation details to callers, or even to transitive callers. They are based on universally-quantified types, when I need existentially-quantified types, synonymous with information-hiding.
How to get existentials? I can go object-oriented. In Haskell, that can look like stuffing a typeclass instance inside a GADT. But that doesn’t work for binary functions; I wouldn’t be able to guarantee that, when intersecting two ECTAs, they use the same memoization library (and they would thus use different global state when they need to use the same).
But, yeah, I totally agree with you about the poor ergonomics of actually writing all your code as a module-valued function (functor) over all its dependencies. I think this could be fixed rather easily using a new kind of import or open statement, but the MLers haven’t yet.
I am adding this answer to a Q&A on the blog post.
Oh hey, I didn’t realize that jkoppel (you) had written this post! I’ve listened to you on several podcasts and I’m very impressed with your work. Thanks for this excellent response, I’ll take some time to digest it and the linked materials you provided. Perhaps this is the push I need to try writing real programs with OCaml.
I, too, think that it is perfectly reasonable to draw conclusions about the best practices in computer science from a 10 line module written in a language that is unused outside of academia.
I actually regret the snark of my previous ^ comment.
I do NOT want to discourage young people in academia from writing things and pushing ideas. And snark like mine is a great way to discourage people from “putting themselves out there”. Shame on me for being that asshole. In my defense, I like to write controversial things online for no apparent reason.
What I was trying to say (hidden in the snark) was that it’s dangerous to accept conclusions from experiments in the small. Yet those same experiments can be excellent catalysts for building experiments in the large, and sometimes the key to discovering scalable solutions is found in the elegance of the small (metaphorical) crystal that shows how to solve some challenge of composition in the large.
So while I hesitate to accept grandiose ideas based on small examples, particularly those from carefully controlled environments like academia, I also want to celebrate that process of learning and experimenting and sharing ideas, which academia excels at.
I hope this exposition at least slightly redeems my previous comment.
There are no experiments in this post. There are several small examples used for teaching a well-known concept. Everyone, industry and academia, uses small examples. Complaining about them can be used to attack any explanation whatsoever.
I was thinking the exact same thing FWIW
The linked blog post is evidence free – https://existentialtype.wordpress.com/2011/04/16/modules-matter-most/
There are definitely many ideas in programming and computer science that can be approached from a purely mathematical perspective, where the math models the problem closely
I’d argue that module systems are not one of them. Any counter-argument to that? It seems obvious
For example
A module system that’s useful for 1000 line programs is not necessarily useful for 1M line programs
1M and 10M line programs are where the real test of a module system is (e.g. browsers, compilers, kernels, and I would even bet the Glasgow Haskell Compiler itself is getting up there, although I haven’t looked)
That’s an interesting article. You did well showing how many languages try to patch on the effects of a good, module system. Those patch-ups do extra damage. I was looking at functional programming via preprocessor in C just last month. I think the scariest thing about such hacks are how there are systems composing that don’t really understand what each other are doing. There’s no consistency protection across those separate formalisms or applications. If anything, it’s like we’d need real, module theory with formal specs for each thing we used to fake the modules. We don’t have that either. So, it might always be a mess to deal with.
I especially loved how you illustrated that that many interfaces might have satisfied an implementation. I’ve been thinking of software rewriting again (eg language-to-language translation). Others are using machine learning to improve software. Tools aiming for one-to-one correspondence between an original and improved version might write different, unintended pieces of software. While they’d treat it as a bug, it might be inherent to how they try to guess interfaces (or other abstract info) from the implementations people feed them. Issues like you mentioned might mean there are upper limits to what we can do.
One thing missing, but almost there in “Not Just for…” section, is you can publish a clean, prototype module as documentation along with code in a different language. This is basically the old concept of prototyping with a high-level language before implementing in a low-level language. Instead, we’re applying it as a specification technique for interfaces which might be easier to learn than full, formal specification. It would help if the readers in the messy language knew the cleaner language. If they didn’t, it could be an excuse to expose them to unfamiliar ideas that broaden their mind.
On your Trinity reference, I think verses 19-20 here apply. God said He designed all of creation to testify to His presence. Thinking of articles here, one way is that what should be a random mess of a universe follows specific laws that follow mathematical/logical rules like you shared. Many of the same maths show up in seemingly-unrelated things like how an artist leaves repeating signatures on their work. While they should changed often, the machinery consistently works with no deviations from its specs. God said in v35-36 here that the fixed laws, which secure our existence physically, were a reminder that He’d keep a greater promise to hold us secure forever. If we repent of our lives’ many sins and put our faith in Jesus Christ (God) instead.
I put up a short explanation with proof of that up here. I hope you receive His free gift, old friend. If you do, you get to meet the Creator of those abstractions, know Him personally, and explore the depths of His designs over eternity.
The “computational trinity” is an older name for what we now call the computational trilogy, a grand connection between logic/syntax/type theory, semantics/category theory, and computation. Harper is quoted on that page, too:
So, when we consider syntactic modules as presented in the blog post, we should also consider the category-theoretic meaning of modules.
The “Holy Trinity” is an older name for God as one being of three persons. People have a history of taking his name in vain or re-applying it in different ways. His names, like His creation, are meant to give Him glory. I just point it back to Him when I see it.
That said, I thank you for sharing the link. It’s very interesting. On top of mathematical education, there’s even another theological concept in it which is potentially useful:
“The central dogma of computational trinitarianism holds that Logic, Languages, and Categories are but three manifestations of one divine notion of computation. There is no preferred route to enlightenment: each aspect provides insights that comprise the experience of computation in our lives.”
This is great wording for a concept that’s hard to explain. One indeed similar to the Trinity. We have God existing as His own essence with all His properties (or nature). Then, each person has their own attributes, sets an example for us, takes seemingly-independent action, and are highly interdependent. After describing specifics, one might say something similar to the above quote: “each aspect provides insights that represent the experience of God moving in our lives.”
This might be another example where God creates things on earth to be shadows of things in heaven to help us understand them and marvel at Him.
Thanks for sharing a second off-topic comment! I appreciate it. In return, here is a quick proof that Jehovah and other omnipotent beings don’t exist. First, consider potentially-infinite matrices of Booleans. If any row of such a matrix is all true, then there cannot be any column which is all false, and vice versa, and vice versa; proofs left to the reader.
Create an open tournament. By tradition, it will be a rock-throwing tournament. Entrants can register rocks which will be thrown, and also champions which will throw rocks. A judgemental person decides whether each champion/rock pair is a successful throw, and tallies the result in a matrix of Booleans. Then, by the above lemma, there cannot be an entrant who simultaneously registers an unthrowable rock and also a champion who can throw any rock whatsoever. Dually, there also cannot be an entrant who simultaneously registers an always-throwable rock and also a champion who is unable to throw rocks. Proof: what does the judge tally after each attempt? This is just a rigorous version of the paradox of the stone, with fluff removed.
In general, the logical relations between our observable reality are sufficient to exclude the possibility of omnipotence. Similar basic statements can be used to exclude trivialism, solipsism, and dialethism/paraconsistency from our reasoning, too.
The article is the topic. Many authors like to drag our faith into unrelated writing. So, my response was to multiple angles. Plus, just out compassion for my old buddy who submitted it. I’d like to see the man be saved by the very God he referenced. :) Back to the tangent.
Re proof. Although interesting, your proof ditches the scientific method for conjecture based on imagined worlds. Science says we must observe our universe’s attributes, how things work in it, build hypotheses based on those observations, test them with controlled experiments, and have skeptical parties independently replicate that. The evidentiary method used in historical situations at least requires corroborated evidence from honest observers. Divine revelation with prophecy and miracles works similarly to the evidentiary method. So, let’s also start with observation of the real world.
We see a universe whose parameters are very fine-tuned. Even non-believers argue this point. They tend to dodge the implication. I wrote that we never see such well-maintained order emerge from chaos. If working from observations, we’re forced to default on God made the universe.
We struggle to make physics work precisely in tiny areas (example). Our AI’s, whether NN or GA, require lots of intelligent design to even operate, much less work correctly. People struggle to develop, optimize, and verify logics with consistency. We marvel at mathematicians and engineers who pull off these feats. How much more should we marvel at God who drives all of that to work with no failures?! We say those people’s output was clearly design as they fought an uphill battle against chaos. Then, we treat the universe like we could make it by shaking up a shoebox long enough. Logically inconsistent. Why do we do this?
“Boast no more so very proudly, Do not let arrogance come out of your mouth; For the Lord is a God of knowledge, And with Him actions are weighed.” (1 Sam. 2:3)
“The LORD Almighty has a day in store for all the proud and lofty, for all that is exalted (and they will be humbled).” (Isa. 2:12)
I was the most guilty of this. Although a good tool, science has failed countless times with so many rewrites of our books. Empirical observation should lead scientists to be the most humble of all people with carefully-worded statements they know might be disproven the next day. Instead, they tell believers what’s definitely true, what’s definitely not possible, and often believe theories with neither observation nor skeptical replication (aka faith). Many mock people who believe in God with far greater evidence than exists for some theories they have much confidence in.
God’s Word said people like me were arrogant people who wanted to be god, had no interest in submitting to a real one, and ignored all the evidence He existed. When God judged how we lived our lives, we’d still be trying to argue with Him about why our moral theories and lifestyles made more sense. The proof was all around us but we already saw god in the mirror. We’d speak so certainly about our beliefs due to our wicked, arrogant hearts. I had to repent.
It gets better still! If you humble yourself and seek God, then He gives you a shortcut around all of those proof requirements. God’s Word says the Father draws us in, “my sheep hear my voice,” and faith comes by hearing the Word. After digging into His Word, God will supernaturally do something that makes it click at some point. Then, a testable prediction is that we’re transformed from inside out by His power. We may also experience answered prayers and miracles. That one message, without modification, has gotten those same results in around 2,000 people groups for thousands of years. It’s power is proven.
Pray to God that He reveals Himself and saves you and start in John. You’ll meet Him. Then, what happens to His followers in His Word will happen to you as well.
Thanks for a third off-topic comment. Let’s see if you’re really a person of science.
Rock-throwing tournaments are completely scientific. Nothing I described is impossible to build in a laboratory, and because Jehovah doesn’t exist, of course they can’t show up and participate in a contradictory fashion. You’re going to have to reply with logic and maths if you don’t like the rock-throwing tournament!
Quantum mechanics is incompatible with omniscience, all-knowing, all-seeing, or any other similar superpower. The Kochen-Specker lemma shows that there are properties of particles which are not locally determined, and thus cannot be observed without measurement. A Stern-Gerlach device allows us to make such a measurement. The same device shows that particles midway through the device, accelerated but not yet measured, are indeterminate – if some deity were measuring them, then the particles would be deflected measurably.
To be blunt: You’re using a device laden with semiconductors, and the theories which were used to design that device have no room for omniscient beings. Also, the device was programmed using theories of logic which have no room for omnipotent beings and can only implement the realizable theorems.
Not gonna lie, most of the math/theory kinda went over my head here. But it was nice to get some validation that the way that I think about modules, as a sort of type boundary, in a language that is kinda pretty far from this level of theory (Python) is kinda not that wrong.