luochen1990/the-concept-of-totality.md

## the-concept-of-totality.md

      
    Raw
  

              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 []