典型的情況是 fibonacci 數列，展示了前面的型別大小如何與程式相關，常見的程式定義如下

def fib : Nat → Nat
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                         | 0   => 1
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                         | 1   => 1
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                         | n+2 => fib n + fib (n+1)

為了抽出計算部分的代數，我們用 inductive type 定義其計算

inductive Fib (a : Type) : Nat → Type where
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                         | z : a → Fib a 0
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                         | o : a → Fib a 1
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                         | s : Fib a n → Fib a (n+1) → Fib a (n + 2)

可以看到 induction case 就是 $(2 \to F a) \to F a = {F a}^2 \to F a = F a \times F a \to F a$ ，所以對應的程式就是兩次呼叫 fib n + fib (n+1) 。當然，因為 fibonacci 還有一個利用矩陣計算的編碼

這個方法對應到 $O(n)$ 的演算法，因此 fibonacci 不一定要用分形遞迴計算。這件事也告訴了我們代數簽名有時候比我們具體的計算更寬鬆，上面的 inductive type 並未限制如何使用 s，也因此可以摺疊時可能存在更快的計算方式。這也說明了當遇到 c : (T -> T) -> T 一類的建構子時，其對應的計算難以寫出的問題，也就是前面沒辦法定義 $T^T$ 的大小的情形。