[ufo]

The actual reason for why not both is that its actually very hard to do and is still kind of an open problem. Some things are easy to do statically but hard to check dynamically (for example, parametric polymorphism or type-based overloading and name resolution) and some things are easy to check dynamically but hard to specify using static types (for example, array bounds checking).

[nabla9]

You can do those things that are easy to do statically at development/testing time and those thing that are easy to do dynamically in runtime.

Some things like overloading based on return values don't work dynamically, but you could either choose to not have them or resolve them in development time. I would like to see languages where dynamic vs. static is continuum and programmers can determine how much they need want case by case basis.

[ufo]

> You can do those things that are easy to do statically at development/testing time and those thing that are easy to do dynamically in runtime.

But then you lose the ability to freely mix and match the static and dynamic code. For example, if you want to write a dynamic implementation for some parametrically polymorphic code there must be a way to check at runtime that the dynamic implementation is respecting the type that you assigned to it (there are ways to do that but they are all very tricky).

The list of tricky things also grows very quickly once you put some though into it. You mentioned return type polymorphism but there are also many other things that are hard to check dynamically (record field names) and lots of things that dynamic codes likes to do (like mutability and subtyping) that force extra complexity into the static type system or that can be used to subvert the static types if you are not careful.

[coolsunglasses]

>(for example, array bounds checking)

It's relatively easy to do this statically compared to bringing the benefits of Haskell to a unityped language. We just don't program in languages designed around dependent types typically.

Dependent types aren't hard.

Agda, Idris, Coq for any who are curious as to what that looks like.

Total functional programming is cool ^_^

[ufo]

You are right. The biggest problem I was trying to point out is that you need to make your static type system much more complex in order to be able to even state some things that are easy to check dynamically. Also, dependent types on their own dont solve the problem of interfacing with dynamic code.