The Concept of Totality, with Haskell examples

the-concept-of-totality.md

The Concept of Totality

See the definition of partial function in wikipedia

Total Function & Partial Function

examples of total functions:

inc :: Integer -> Integer
inc x = x + 1

div' :: Integer -> Integer -> Maybe Integer
div' _ 0 = Nothing
div' x y = Just (x `div` y)

examples of partial functions:

fromJust :: Maybe a -> a
fromJust m = case m of Just x -> x

head :: [a] -> a
head xs = case xs of (x:xs') -> x

div'' :: Integer -> Integer -> Integer
div'' x y = x `div` y

Proper Call & Improper Call

examples of proper call:

inc 1
head [1, 2, 3]
fromJust (Just 1)
div'' 3 2

examples of improper call:

head []
fromJust Nothing
div'' 3 0

Total Term & Partial Term

Just think about that we can consider every term as a function with a single argument typed Unit. We can expand the semantic of "total" this way: a term t typed a is total if and only if the function f :: Unit -> a; f () = t is total.

examples of partial terms:

-- | literal undefined
undefined

-- | call builtin function "error"
error "impossible"

-- | dead loop
let x = x + 1 in x

-- | improper call of partial function
head []