> For example, functions that return a different type depending on the values passed in are a useful pattern, but not allowed in staticly typed languages, except those with dependent types (Idris) or runtime downcasting (Go). There's always a way to acheive the same thing, but usually at the cost of safety or much more verbosity.

Look at this verbose OCaml:

    type my_return_type = AFloat of float | AnInt of int | AString of string;;

    let my_fun n =
        if n < 0 then AString "negative"
        else if n == 0 then AFloat 0.0
        else AnInt n

    # my_fun (-4);;
    - : my_return_type = AString "negative"
    # my_fun 0;;
    - : my_return_type = AFloat 0.
    # my_fun 42;;
    - : my_return_type = AnInt 42

(But yes, to use these values you have to do pattern matching, and if you're in a FUD mood, that is "runtime downcasting" and incurs a "cost of safety".)

Yes, you can always generate a new union type for your return type and then pattern match on it. That is certainely better than C where you must use unsafe tagged unions or void pointers. It is more verbose than in dynamic duck-typed languages, though I'll give you that it's quite compact in OCaml.

In a dependently typed language, you could reduce verbosity at the use site as well as avoid the extra runtime branch.

So how exactly would you write the above five lines of OCaml in fewer than five lines in Idris?

The verbosity is not in the function definition, its in the match expression needed at _every single call site_. In Idris, the definition would be similar length or longer, but call sites would not need a match expression.

> provides a (runtime) safe and low-verbosity way to write dynamically-typed code, i.e. `interface{}`

Since Go 1.9 was released with its new Type Aliases feature a few months ago, the verbosity is even lower. By putting `type any = interface{}` somewhere in your package, you can just write `any` instead of the verbose `interface{}` everywhere you want some dynamic typing.