The beauty and the beast: explicit and implicit types

Working with Haskell has brought on an unexpected question:

• Is it more productive to work with implicit types or explicit types?

By this I mean: “Should major types be mostly inferred or mostly specified with type signature”?

The bizarre fact is that you may well use two different parts of your brain to work with inferred types or with “defined” types!  Here is the reasoning:

Programming is an incremental process: changes are made locally and then overall consistency is assured. When programming around types, changes are made to type specifications or to expressions which affect type. The two kinds of changes lead to two styles of programming: the first is to start by changing a type definition or type annotation, the second is to start by changing an expression, which results in a change to the inferred types, and possibly needing a fix to a type signature.

The bare minimum of type annotation is not even to provide argument to “top level” functions, such as in let f = fun a b -> … , where we only know that the function f has two arguments because it is inferred from its body. This style may sound contrived but is a way to work around the type class restriction in F#.

So how does this affect productivity? Mental work is much about having a good inner dialog; Your mind is taking a very static view of the program’s design when you worry about type signatures. While when you worry about the result of the type inference, you are effectively “re-running” the program in your head. It is not the same thing! And I find in many cases the second thought process, the reliance on inferred types, the more productive way to work.

Addendum:

This study goes very much in this direction: https://news.mit.edu/2022/your-brain-your-brain-code-1221

Modeling software systems: data centric, and then what?

For many years I favored a declarative data centric view to software architecture: Graphs with a compositional hierarchy were my mantra. I once explained that these design were like the one ring in the lord of the ring: “One pattern to rule them all and in the design simply them”.

Yet in the end I have changed my beliefs. I now favor a more “equation solving” view to modeling. I find more and more, and especially in the context of real time automation that the models are inherently “sustained” between a data centric model and what I call a dynamic model, which is easier to describe differently. I find easiest to describe dynamic properties as domain specific type theories in a functional framework. These are expressed as DSL with ad hoc types and type inference solvers.