Lambda Calculus Conversion
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 -&gt; (a -&gt; [a] -&gt; T) -&gt; ([a] -&gt; 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] -&gt; a) -&gt; ([a] -&gt; a)
F := λ f -&gt; match_list 0 (λ x -&gt; (λ xs -&gt; x + f xs))

and then
sum := λ x -&gt; (fix F) x
     = λ x -&gt; (fix (λ f -&gt; match_list 0 (λ x -&gt; (λ xs -&gt; 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 -&gt; match_list 0 (λ x -&gt; (λ xs -&gt; x + f xs))) (fix F) [1,2]
          = match_list 0 (λ x -&gt; (λ xs -&gt; x + ((fix F) xs))) [1,2]
          = 2 + ((fix F) [1])
          = 2 + ((F (fix F)) [1])
          = 2 + ((λ f -&gt; match_list 0 (λ x -&gt; (λ xs -&gt; x + f xs))) (fix F) [1])
          = 2 + (match_list 0 (λ x -&gt; (λ xs -&gt; x + ((fix F) xs))) [1])
          = 2 + (1 + ((fix F) []))
          = 2 + 1 + ((F (fix F)) [])
          = 2 + 1 + ((λ f -&gt; match_list 0 (λ x -&gt; (λ xs -&gt; x + f xs))) (fix F) [])
          = 2 + 1 + (match_list 0 (λ x -&gt; (λ xs -&gt; 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 &quot;internal&quot; constructs and are not explicit terms in the language.