I find it best to let confidence guide me. If I'm not confident something's right, that's usually a sign I didn't type it enough. If I think I know it already, then it doesn't need more types. It affects the design but it should affect the design, I would say; decisions about which invariants are important are design decisions.
> Is there a good rule for when to use a sum type vs distinct types?
If at some point you have a value that you know (and care) is one particular, well, type, make it a real type. If you only ever have values that could be one or the other and it doesn't matter which they are (or the section where it matters can be reasonably confined to a match block) then a sum type.
> but the choice of what gets to be parent and what gets the child is arbitrary and often turns out super limiting further down the line.
I find this is much less true in an immutable-by-default language. E.g. in the standard circle/ellipse example it becomes completely obvious which is the parent and which is the child.
> Tables on the other hand, supported by light usage of manually coded lookup tables, have been the real game changer for me. When I'm back in a normal imperative language I can be so naturally productive and write efficient programs without relying on black compiler magic. I don't see how most of the invariants in my programs could ever be codified in a practical type system. They are so relational - they involve variables with very diverse lifetimes and expressions depending on dynamic values.
Heh, this is the opposite of my experience. I find tables always confuse me, and are usually a sign that my model needs to have an intermediate entity - like the experience described in http://wiki.c2.com/?WhatIsAnAdvancer
Sum types are a major headache. Is there a good rule for when to use a sum type vs distinct types? The expression problem is very practically relevant to me. Also the typical flat vs hierarchial data storage wisdom applies: Trees and hierarchies are very much encouraged by HM type systems, but the choice of what gets to be parent and what gets the child is arbitrary and often turns out super limiting further down the line. Similarly, there's the choice of what to include in a hierarchy and what to put in a separate one.
Tables on the other hand, supported by light usage of manually coded lookup tables, have been the real game changer for me. When I'm back in a normal imperative language I can be so naturally productive and write efficient programs without relying on black compiler magic. I don't see how most of the invariants in my programs could ever be codified in a practical type system. They are so relational - they involve variables with very diverse lifetimes and expressions depending on dynamic values.
In the end, I feel writing assertions is just much better for me, because I can be somewhat sure in a few tries that my invariants hold, in the same language that I use for coding, and having the same values available. Meanwhile I would waste hours trying to codify a small fraction of them in an HM type system.