It helps to remember that we don't gain any expressiveness from a type system, only safety[1]. Type systems can only restrict which programs we're allowed to wr

It helps to remember that we don't gain any expressiveness from a type system, only safety[1]. Type systems can only restrict which programs we're allowed to write[1], compared to un(i)typed programs. After our programs have passed the type-checker, their types can be erased to leave behind a raw un(i)typed program. In the case of functional programming, we can imagine it compiling down to something like Scheme. The point is that we can handle error conditions just like we do in any other language: if we're compiling to something which looks like Scheme, we can handle errors in the same way: have everything return a sum allowing errors (ie. a Maybe). Even things which don't produce errors can be lifted to this type automatically and chained together using a monad. That's basically what Haskell does. Of course, lifting simple functions to return Maybes isn't very nice, since we're purposefully throwing away information; ie. we're causing our consumers to ask "did this return a value or not?" when we already know that it always will. The problem is that with composing Maybe functions with simple functions. There's no way around this in Haskell, we need to lift the simple functions; after all, that's the point of a monad: we can return a wrapped value and we can join a wrapped-wrapped value into a wrapped value but there's no way to unwrap a value (otherwise we may have a comonad instead!). Dependent types give us more flexibility than Haskell though: if our output value depends on the input, we can also make our output type depend on the input. For example (where "A", "B" and "C" are some concrete types, for simplicity): -- Simple function myFunc1 : A -> B myFunc1 = ... -- Maybe function (ie. might error) myFunc2 : C -> Maybe A myFunc2 = ... -- Maybe monad. Works, but loses some type info liftedChain : C -> Maybe B liftedChain x = case myFunc2 x of Nothing -> Nothing Just y -> Just (myFunc1 y) -- Exactly the same algorithm, but without losing type info myType : Maybe A -> Type myType Nothing = () -- Unit type, equivalent to Nothing myType (Just _) = B -- Result type, equivalent to Just unliftedChain : (c : C) -> myType (myFunc2 c) unliftedChain x = case myFunc2 x of Nothing -> () -- Unit value; matches myType Nothing as required Just y -> myFunc1 y -- Value of type B; matches myType (Just y) as required This makes it easy to handle runtime errors, without having to pretend that everything else might blow up. Typically, we write most of our code in an ideal world assuming all of our requirements are met, then we write simple "driver" functions which justify those assumptions, returning errors otherwise. Exactly like in Haskell, where we write pure functions for manipulating plain values like strings, then write simple "driver" functions to pull those strings out of files, databases, sockets, etc. using IO. [1] Strongly typed languages can be more or less expressive than each other due to their type systems (eg. dependent types make it easy to express homogeneous lists, which can't be done (AFAIK) in System F), but all are less expressive than un(i)typed languages.