4 ms·

I would be interested in you giving an example of a problem that is not solvable or expressible in a typed language. I am not able to think of such a thing of t

by foxes 5y ago

I would be interested in you giving an example of a problem that is not solvable or expressible in a typed language. I am not able to think of such a thing of the top of my head. I disagree that performance is a big advantage. Perhaps there are certain optimisations that can be done if you have added more constraints? But that seems like an added benefit. I feel like there are a plethora of examples of type errors however. Obviously it doesn't rule out logical errors, but at least at the type level its "correct". You can even lift problems to just be type problems. For example only being able to construct inputs as something in the type system. Seems like that rules out a whole class of possible errors with parsing input.

dgb23 5y ago
> I would be interested in you giving an example of a problem that is not solvable or expressible in a typed language. I meant to say that some of many solutions can better, typically simpler, while being just as correct because you don't need to express it in static types. > Obviously it doesn't rule out logical errors, but at least at the type level its "correct". You can even lift problems to just be type problems. For example only being able to construct inputs as something in the type system. That is orthogonal to a type system though. If you take care of the invariants of a data-structure you are almost always going to need more than what most type systems can express. In fact I would argue that type systems provide immediate documentation of very basic properties, which is often an advantage, but from my experience the errors it covers for you are rare, yet can be severe and confusing. Again, having used both I'm not entirely happy with either. I prefer when static, or more generally developer-time-checks are opt-in and expressive, which seems to be a growing trend.

by foxes 5y ago

dgb23 5y ago

> I would be interested in you giving an example of a problem that is not solvable or expressible in a typed language. I meant to say that some of many solutions can better, typically simpler, while being just as correct because you don't need to express it in static types. > Obviously it doesn't rule out logical errors, but at least at the type level its "correct". You can even lift problems to just be type problems. For example only being able to construct inputs as something in the type system. That is orthogonal to a type system though. If you take care of the invariants of a data-structure you are almost always going to need more than what most type systems can express. In fact I would argue that type systems provide immediate documentation of very basic properties, which is often an advantage, but from my experience the errors it covers for you are rare, yet can be severe and confusing. Again, having used both I'm not entirely happy with either. I prefer when static, or more generally developer-time-checks are opt-in and expressive, which seems to be a growing trend.