| > by encoding more and more responsibility in the type system, you're just pushing your business logic to a different language Yes, this is 100% correct. Type systems are just another language > The same propensity for human error exists there as well. This is where I disagree. Sure you can make errors in types, but it's not the same because strong type systems are more like proof systems. They tell you when you've encoded something that doesnt make logical sense. And they help you figure out if your code can be made to adhere to them. It's a checker that you don't normally have. > But I don't see much difference in putting that logic in the base language or the higher order type system language, except the base language is more expressive and flexible. The type language encodes your assumptions, and the base language has to adhere to those assumptions. If your type language is expressive enough, you can encode pretty complex assumptions. There's value in having the two playing against each other. Similar to tests: you could say tests are just re-stating what you've already written in your code. In reality, it's another check for consistency with your original intention. |