The thing to notice here is that your function sum is defined on lists, which are inductively defined. Theoretically, the inductive definition of a list defines for every type T a term
match_list :: T -> (a -> [a] -> T) -> ([a] -> T)
satisfying the property
match_list s t [] = s
match_list s t (x::xs) = (t x xs)
in addition, defining a recursive function requires an untypable fixed-point combinator fix satisfying the property
fix F = F (fix F)
so combining the two, we could write your definition by first defining
F :: ([a] -> a) -> ([a] -> a)
F := λ f -> match_list 0 (λ x -> (λ xs -> x + f xs))
and then
sum := λ x -> (fix F) x
= λ x -> (fix (λ f -> match_list 0 (λ x -> (λ xs -> x + f xs)))) x
To convince oneself that this works, let's try this on the example
sum [1,2] = (fix F) [1,2]
= (F (fix F)) [1,2]
= (λ f -> match_list 0 (λ x -> (λ xs -> x + f xs))) (fix F) [1,2]
= match_list 0 (λ x -> (λ xs -> x + ((fix F) xs))) [1,2]
= 2 + ((fix F) [1])
= 2 + ((F (fix F)) [1])
= 2 + ((λ f -> match_list 0 (λ x -> (λ xs -> x + f xs))) (fix F) [1])
= 2 + (match_list 0 (λ x -> (λ xs -> x + ((fix F) xs))) [1])
= 2 + (1 + ((fix F) []))
= 2 + 1 + ((F (fix F)) [])
= 2 + 1 + ((λ f -> match_list 0 (λ x -> (λ xs -> x + f xs))) (fix F) [])
= 2 + 1 + (match_list 0 (λ x -> (λ xs -> x + (fix F) xs)) [])
= 2 + 1 + 0
This is theoretically what would go on in a purely functional language (for example the untyped lambda calculus), however in languages like haskell, lisp, or ocaml (I am unaware of inductive datatypes in python), the terms match_list and fix are "internal" constructs and are not explicit terms in the language.
