Hi all, Let me restate the reasons of introducing the concept of "partially defined functions".
1. One would like to introduce functions by pattern matching. 2. Full covering is an undecidable problem. However, with the concept of partiality, it is not a problem any more because partially defined functions are harmless. Two more examples are in the following. The inhabitation of ....-> Nat is obvious, and it is unnecessary to check pattern coverage. See more details on: http://www.cs.kent.ac.uk/people/staff/yl41/TPF.ps f :: Nat -> Nat -> Nat -> Nat f 0 0 0 = 1 f 0 (succ y) z = g1 y z f (succ x) y 0 = g2 x y f x 0 (succ z) = g3 x z f (succ x) (succ y) (succ z) = f (succ x) (succ y) z + f (succ x) y (succ z) + f x (succ y) (succ z) where g1 g2 and g3 were defined beforehand. Nested patterns: np :: List (List Nat)-> Nat -> Nat np (nil (List Nat)) n = n np (cons (List Nat) (nil Nat) xss) n = np xss n np (cons (List Nat) (cons Nat x xs) xss) = np (cons (List Nat) xs xss) (succ n) In Haskell, one can write np as follows. np :: [[Int]] -> Int -> Int np [] n = n np ([]:xss) n = np xss n np ((x:xs):xss) n = np (xs:xss) (n+1)
