Well, weak vs. strong typing is pretty vaguely defined. Further, since closest there is to a general use of 'strong typing' is to refer things that make it difficult to cast types, that leaves nothing further to describe even stronger type systems. It's like saying if you can carry less than 30 lbs you are weak, and everyone who can lift more is in the same category of 'strong' - a misleading distinction.
So I prefer the definition:
- Weakly typed systems use types to prevent you from doing certain things (like mistakes)
- Strongly typed systems use types to do things for you
What do I mean by do things for you? Well, let's examine writing an image conversion API in the Servant framework (in Haskell, but you don't really need to know it to follow along, you'll see...)
{-# LANGUAGE
TypeOperators,
DataKinds
#-}
import Codec.Picture
import Data.Proxy
import Network.Wai.Handler.Warp (run)
import Servant
import Servant.JuicyPixels
main :: IO ()
main = run 8001 conversion
This is saying that we want some modules including the Servant package and the JuicyPixels plugin to Servant, and that the main entrypoint of the program is to run the 'conversion' function on port 8001 as the server using the Warp backend. Ignore the language bit.
conversion :: Application
conversion = serve (Proxy :: Proxy ConversionApi) handler
This is saying that the conversion function is a server where the API must match type 'ConversionApi' and the requests are handled by the function handler
type ConversionApi
= ReqBody '[BMP, GIF, JPEG 50, PNG, TIFF, RADIANCE] DynamicImage
:> Post '[BMP, GIF, JPEG 50, PNG, TIFF, RADIANCE] DynamicImage
This is specifying the ConvesionApi type. It says that we should accept incoming content types specified by the list '[BMP,GIF,JPEG 50, PNG, TIFF, RADIANCE], and handle them as a DynamicImage, and that we should return a DynamicImage converted into the same range of content types. Don't worry exactly about what :> means, just think of it as happy magic for now.
So, given my preferred definition, a weakly typed system can now ensure things like:
- You don't return the wrong outgoing content type
- You don't parse the incoming request as the wrong content type
- If our server was more complicated, it would prevent us from creating malformed URIs, but we're not actually returning any HTML pages to contain links (and the type ensures that we can't!)
- A really ambitious weak typing system might even check to make sure we're exhaustively handling all the incoming and outgoing content types, allowing the type to also act as a specification document instead of just a constraint.
All lofty goals, but not actually enough to qualify as a strongly typed system, given the above definition. And now we have to get to the hard part of actually writing code that follows this specification. In a really strong type system, we write:
handler = return
And then we're done. That's it, there isn't any more code to write. This is a fully operational web server (modulo any typos I missed). The type has told the compiler everything it needs to create our web server from the types and the packages (modules technically) that we defined and imported.
So, how do you learn to do this at the major application scale? Well, it's really not much different from using them in smaller scale applications. Types that are absolutes don't care how much code is written relating to them.
Run time type inspection is something you're probably going to want to avoid, because that carves away a huge amount of the benefit and allows types to make your project more complicated to work with, rather than having types simplify things.
As such, it's mostly just a matter of practice modelling things with types. The two main ways of modelling things (or building things in general) are bottom up and top down. Top down starts with the highest level of operations, and as you build the model you have parts where you are deferring the modelling until later. Bottom up modelling means you start with base operations, just like you start with base functions, then build larger and larger models until you have fully captured the operation of the project. Bottom up is more concrete and likely faster to build, but top down may better inform your lower level models as to how they need to actually behave.
Types are how programs relate to math, literally, so there isn't really an upper bound on how complicated they can get, or a point where you can be 'done' learning about them. Virtually all of the resources outside higher level university courses are all dedicated to how types work in some particular language, so you need to decide that as well.
As best I can offer, types can be stratified like so:
- Very weakly typed, things like JavaScript where [] + {} is defined
- Weakly typed like Python, where you can't do [] + {}, but that isn't checked until you try
- Weakly typed like C or Java, where you can't do [] + {}, but that's checked at compile time, however you don't have the more advanced type features
- Straddling the border between weakly and strongly typed, such as C++ template metaprogramming, and simpler Haskell code where types are only enforcing properties.
- Fully into Strongly typed, like more complicated Haskell programs where types do things, as shown above
- The very strongly typed, like Agda or Idris, where types and values interact and can constrain each other. This is as strong as type systems get, and programming in them is the same as writing mathematical proofs about what your program does. Note: coding in Agda it is not literally writing mathematical proofs, types are mathematical theories, and functions with those types are constructive examples proving those theories.
Generally, the further down this list you go, the more that types can do for you, but by the very bottom, you're climbing into the stratosphere and the air is getting a bit thin - the package ecosystem is much smaller and you'll have to write more things yourself vs having found a relevant library. The barrier to entry also goes higher as you go down, as you have to actually understand the type system enough to write large scale programs.
