29

I know this is a very broad, ambiguous, and possibly philosophical question. To an extent, that the most important keyword in the question - "strong" type system - itself, is ill-defined. So, let me try to explain what I mean.

Overall context for the question

We've been building a very large scale web-app in Ruby on Rails and we've been generally happy about our stack. When we want to, we can ship stuff really fast - something that works for 90% of the "business" case, without worrying too much about 10% edge cases. On the other hand, with the help of code-reviews & test-coverage, we can be slow & deliberate and make sure we cover all bases - again, only in situations that merit such closer scrutiny & safety.

However, as the team grows, I've started getting uncomfortable with the lack of a "safety net" baked right into our stack.

We recently started doing some native Android development on Java. And I was (pleasantly) reminded of the safety provided by a compiled/static/strongly-typed language.

  • Mis-spelled variables, wrong data types, incorrect function invocations, and a host of trivial errors are caught by your IDE itself. All because the IDE can hook into the compiler and verify certain aspects of program "correctness".
  • Need to change a function signature? Easy. The compiler+IDE can help you spot ALL call sites.
  • Need to ensure that certain exceptions are always handled? Checked exceptions to your rescue.

Now, while these safety features have their advantages, I'm well aware of their disadvantages as well. More so, in the world of "boilerplate heavy" Java. Therefore, instead of Java, I've started looking at the slew of modern, "strongly typed" languages that people have started working on these days. For example: Scala, Rust, Haskell, etc. What interests me most is the power of their type systems and static/compile-time checks.

Now, the question

How do I use these powerful type systems and static/compile-time features in larger applications?

For example, how would I move beyond the standard "hello world" kind of introductions to these powerful features? One that uses a a rich type system to model a business-domain problem? Does the type system help, or hinder, when you're in the 30,000 LOC+ zone? What happens to the safety net provided by these type systems (and compile-time checks) when your system interacts with the weakly typed outside world, eg. via JSON or XML APIs, various data stores, user input, etc.

  • 12
    This is off topic because there's no real answer. The question is intended to provoke opinionated discussion ("I like/dislike static types because..."), not factual explanation. My advice would be to pick one of the more-specific parts of your question such as "What happens to the safety net provided by these type systems when your system interacts with the weakly typed outside world?" and rewrite the question to be about that. You'll get definitive answers which will be useful to future readers that way. – Benjamin Hodgson Dec 20 '15 at 8:57
  • 5
    Resource recommendations are also off-topic here (because such answers go out of date quickly and we really aren't any better than Google at it). As Benjamin said, there are some answerable questions buried in your post, but the whole post in its current state is essentially asking for people to describe their experiences using these languages, which is a much better fit for Quora or Reddit than it is a StackExchange site. I am not downvoting, because this question is well-asked, but it's just not a StackExchange question. – Ixrec Dec 20 '15 at 14:20
  • 4
    A type system is a tool, and like any other tool, it's efficacy largely depends not on the tool itself but on the wielder. You can leverage the type system of a language like Haskell to encode invariants about your business logic at the type level and have those invariants checked by a machine (the compiler) at compiler time, but to do this you need an understanding of the semantics of the type system and type checking. The right question is not "is this a good tool for web stuff", it is "here are some specific problems I face; how could a strong type system be used to address them?" – user2407038 Dec 20 '15 at 15:21
  • 5
    Most of the things you describe have nothing to do with the type system. They are purely IDE features. With the exception (no pun intended) of checked exceptions, all of the features which you mention have been present in Smalltalk IDEs long before they appeared in IDEs for statically typed languages. In fact, one of the most widely-used Java IDEs actually started out as a modified Smalltalk IDE (IBM VisualAge Smalltalk, which was modified to understand Java code but was still written in Smalltalk and released as VisualAge Java, which was then ported to Java and released as … – Jörg W Mittag Dec 20 '15 at 16:25
  • 4
    … VisualAge Java Micro Edition, which was then broken up into re-usable components and released as Open Source under the name Eclipse). Somewhat ironically in the context of this question, it is precisely because of the dynamic nature of Smalltalk systems that Smalltalk IDEs are so powerful. Automated Refactorings were invented and first implemented in Smalltalk, for example. By your logic, Haskell must have the best IDEs since it has the strongest, strictest static type system of all the languages you mentioned. But it doesn't. You also mentioned "hooking into the compiler". This has … – Jörg W Mittag Dec 20 '15 at 16:30
34

I'll give a short answer due to my lack of time at the moment, but I'm currently working on two big projects (> 100.000 LOC in Haskell) - flowbox.io and luna-lang.org. We use Haskell for all the parts, including the backend, compiler of our programming language and even the webGL based GUI. I have to admit that the strong type system and the "dependent type"-like machinery can guide you and save you from burden and hassle known from other languages. We use the types very extensively and everything that could be checked in compile time, is done so. In fact, during the last 3 years of development, we never, ever encountered any runtime error or stack overflow (and this is something really incredible). The only errors are obvious logic errors made by programmers. A lot of people tell, that if something compiles in Haskell, it just works and you should be pretty sure it will not blow in your face some day. This is true for most of the situations and when you know the language well and know what to avoid (like unimplemented typeclass methods), you'll be safe and gain big profits from the type system.

Answering the first part of the question: You can learn about these powerful type system features reading some great blogs, like:

In fact, there are a lot of other nice blogs out there (like planet Haskell). Anyway, the best method to really understand the advanced type systems is to develop a useful open source library. We (at Flowbox & New Byte Order) are releasing a lot of libraries (you can find them at Hackage), so if you don't have an idea what to develop, you can always involve into our projects – just email me whenever you want (mail available at luna-lang.org).

  • 4
    "A lot of people tell, that if something compiles in Haskell, it just works and you should be pretty sure it will not blow in your face some day.": I have only used Haskell for small (even though non-trivial) projects, but I can confirm this: Once the Haskell compiler is satisfied I rarely find any bugs left. – Giorgio Dec 20 '15 at 18:59
  • 1
    I am probably one of the "Haskell" guys who hate types the most (so much I wrote my own version of Haskell without types, after all) - but for different reasons most people do. When it comes to software engineering, I, too, have that feeling that, when GHC is happy, your program just works. Haskell-like type systems are the ultimate tool not only for detecting humanish mistakes in programming, but for keeping huge codebases under your control. (I always remember Giovanni's justification to Mewtwo's armors whenever I have to fix type erros.) – MaiaVictor Dec 21 '15 at 14:20
  • Gabriel Gonzales' blog is the best to start with. – sam boosalis Jul 20 '16 at 10:29
  • @danilo2 Have sent an email to the contact@ address on your company website. Request you to respond. Thanks! – Saurabh Nanda Aug 22 '16 at 10:03
  • @SaurabhNanda: I double checked our inbox and I dont see any message from you. Have you send it to contact <at> luna-lang.org? Please contact me directly writing to my wojciech <dot> danilo <at> gmail <dot> com and we will investigate what was the cause for this problem :) – danilo2 Aug 24 '16 at 17:41
17

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.

  • Note that you don't need to prefix the type-level list with an apostrophe if there is more than element in the list. The apostrophe is only necessary for 0- or 1-element type-level lists since they are ambiguous (they could be referring to the ordinary list type constructor) – Gabriel Gonzalez Dec 20 '15 at 17:17
  • 1
    I'm aware, but I was under the impression the apostrophe was just good form for promoted data types in general. E.G. that Proxy :: Proxy True works, but it's better to write it as Proxy :: Proxy 'True. – Steven Armstrong Dec 20 '15 at 17:23
  • 1
    It seems better to not collapse the various axes according to which type systems can be classified. Barendregt's lambda cube already includes three, and additionally along the single weak-strong axis you are also including static vs. dynamic, and parametric vs. ad hoc polymorphism (the latter being what allows the servant technique for making types do much of the 'work'). – user2141650 Dec 20 '15 at 17:27
  • 1
    Fair point, but the answer is already very long as it is, and you have to be well on your way into studying type theory before the lambda cube really starts to make sense. Further, outside of very niche (and since I'm already including Haskell and even Agda, I really do mean quite niche) languages, you aren't really going to find a language that has, for example, dependent types but no type operators. – Steven Armstrong Dec 20 '15 at 17:35
  • Can you briefly explain the '[xs] syntax? This clearly isn't a Char, but I don't see how either TypeOperators or DataKinds enables an alternate syntax. Is it some sort of quasiquoting? – wchargin Dec 20 '15 at 20:58
10

I just started working on the core team of a large platform written in Scala. You can look at successful open source applications, like Scalatra, Play, or Slick to see how they handle some of your more detailed questions about interactions with dynamic data formats.

One of the great advantages we've found of the strong typing of Scala is in user education. The core team can make decisions and enforce those decisions in the type system, so when other teams who are much less familiar with the design principles have to interact with the system, the compiler corrects them, and the core team is not constantly correcting things in pull requests. This is a huge advantage in a large system.

Of course, not all design principles can be enforced in a type system, but the stronger your type system, the more design principles you can enforce in the compiler.

We can also make things easier for users. Often to them they are just working with regular collections or case classes, and we are converting it to JSON or whatever automatically as needed for network transport.

Strong typing also helps make differentiations between things like unsanitized and sanitized input, which can help with security.

Strong typing also helps your tests be more focused on your actual behavior, instead of needing a bunch of tests that just test your types. It makes testing much more pleasant, more focused, and therefore more effective.

The main disadvantage is unfamiliarity with the language and the language paradigm, and that is correctable with time. Other that, we have found it well worth the effort.

8

While not a direct answer (since I haven't worked on +30.000 LOC code bases in haskell yet :(..), I implore you to check out https://www.fpcomplete.com/business/resources/case-studies/ which features a lot of case-studies of haskell in actual industry settings.

Another good article is IMVU, that describe their experience changing to haskell - http://engineering.imvu.com/2014/03/24/what-its-like-to-use-haskell/.

From personal experience in larger applications, the type-system very much helps you, especially if you try to encode as much as you can in types. The true power is really obvious when it comes to refactoring things - meaning maintenance and such become a much less worrisome task.

I'm gonna dump a couple of links to resources that I recommend, since you are asking quite a lot of questions at once:

As a closing remark, regarding dealing with the outside world is done in several ways. There are libraries to make sure things on your end are type safe, like Aeson for JSON, Esqueleto for SQL and many more.

3

What I've Seen:

I've worked a few large Ruby web applications (Rails), one large Haskell web application, and several smaller ones. With that experience I have to say that life working on the Haskell applications is much easier than in Rails in respects such as maintenance and lower learning curve. I am of the opinion that these benefits are both due to Haskell's type system and functional programming style. However, unlike many, I believe that the "static" part of the type system is just a huge convenience in that there is still benefit to be had when using dynamic contracts.

What I believe

There is nice package called Contracts Ruby which goes along way in providing some of the main features that I feel help Haskell projects achieve better maintenance characteristics. Contracts Ruby performs its checks at run-time so it is best when paired with high test converge but it still does provide the same in-line documentation and expression of intent and meaning as using type annotations in languages such as Haskell.

Anwser to Question

To answer the questions posed above, there are many places where one can become familiar with Haskell and other languages with advanced type systems. However, and to be perfectly honest, while these sources of documenation are excellent in their own right they all seem a bit underwhelming when compared to the plethora of documentation and practical advice found in Ruby, Python, Java and other such languages. In any case, Real World Haskell is getting old but is still a good resource.

Category Theory

If you choose Haskell you will run into large amounts of literature discussing Category theory. IMHO category theory is useful but not necessary. Given it prevalence in the Haskell community its is easy to conflate the pro's and cons of types with feelings about the practicality of Category theory. Its helpful to remember they are two different things, that is to say that implementations guided by Category theory can be done in dynamically typed languages just as well as static (modulo the benefits the type system provides). Advanced type systems in general are not bound to Category theory and Category theory is not bound to type systems.

More on Types

As you learn more about programming with types and the techniques therein (which happens quite quickly because its fun) you are going to want to express more with the type system. In that case I would look into to some of the following resource and join me in making tool vendors aware that we want industrial quality tools with these features only packaged into something that exposes an easy to use interface (like Contracts Ruby):

2

First, I feel like there is a confusion in answers between weakly typed versus strongly typed, and static versus dynamically typed. Link the OP provided clearly makes the distinction :

A strong type system is a type system that has a compile-time restriction or run-time feature that you find attractive.

A weak type system is a type system which lacks that restriction or feature.

For example, C, C++ and Java are statically typed since variables are typed at compile time. Yet, C and C++ can be considered weakly typed because the language allow to bypass restrictions using void * pointers and casts.More on this topic.

On this distinction, strong typing can only be better. The earlier the fail, the better.

However, on writing large programs, I don't think type system plays an important role. Linux kernel is ten million LOC written in C and assembly and is considered a very stable program, it's miles away from my 200 Java lines that are probably full of security holes. Similarly, although dynamically typed "script languages" suffer a bad reputation when it comes to writing large programs, there is occasionally proof it's undeserved (such as Python Django, over 70k LOC)

In my opinion, it's all about quality standard. The responsibility for scalability of large applications should only be held by the programmers and the architects and their will to make the application clean, tested, well documented etc.

-1

Where can one read about how to use these powerful type systems and static/compile-time features in larger applications?

from previous answer https://www.fpcomplete.com/business/resources/case-studies/

How does one move beyond the standard "hello world" kind of introductions to these powerful features?

it's really like any other language to build up strength

How can one use a rich type system to model a business-domain problem?

By using Abstract Data Types, or more generally polymorphism

Does the type system help, or hinder, when you're in the 30,000 LOC+ zone?

It helps all the way. the type system helps you write the code as it tells you the shape of the result you want to have. Actually Agda write code for you.

PS: do not make the mistake of having a type system and having to write the types yourself, which is idiotic : computer can do it for you.

What happens to the safety net provided by these type systems (and compile-time checks) when your system interacts with the weakly typed outside world, eg. via JSON or XML APIs, various data stores, user input, etc.

It's great, as knowing the structure of values via types means the computer can infer a way to write (de)serializer for you.

If you really want to know about types and abstraction, the best introduction is On Understanding Types, Data Abstraction, and Polymorphism

It's a paper, not a case study with pretty pictures, but it's enlightening

-2

As a .net programmer who works on web applications a lot I see both the typed C# and untyped Javascript side of things.

I'm not sure I've seen any literature about the questions you ask. With a typed language you take all these things for granted. With an untyped one you see defining the types as unnecessary overhead.

Personally, I don't think you can deny that a strongly typed language offers the benefits you describe at a very low cost (compared to writing equivalent unit tests). Interacting with weakly typed systems usually involves generic types, such as Arrays or Dictionaries of Objects, such as DataReader, or creative use of string or the new dynamic class. Essentially it all works, you just get a runtime error instead of compile time.

If you want to write a very short program, maybe defining a function in a couple of lines to work with a larger application, then you simply don't have room to declare classes. Surely this is the niche untyped languages such as JS occupy?

  • Do you mean typed / untyped or statically typed / dynamically typed? JavaScript is not untyped but dynamically typed. – Giorgio Dec 20 '15 at 12:48
  • 2
    you dont have to define the types. any decent language will infer the types for you : haskell, ocaml, sml, F#... – nicolas Dec 20 '15 at 14:19
  • 1
    when you are used to a strongly typed language everything else is untyped, when i say define the types i mean 'create the classes' sure you can use var or whatever, but its just a compiler trick – Ewan Dec 20 '15 at 15:53

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.