[icen]

Another classic use case is that you can have expressions in the types of your function, for example this won't compile:

    stringOrInt : (x : boolean) -> int -> (if x then String else int)
    stringOrInt true x = toString x
    stringOrInt false x = x + 1

    1 + stringOrInt true 37 # this will error, because it knows you've not returned an int

The other example that you can do in depedently typed languages, but is too involved to write out here, is make a type-safe printf, where the format string produces the types for the other arguments.