--- Pascal's triangle is the arrangement of binomial coefficients in a triangular array. --- The rows of the triangle are staggered so that each number can be computed as the --- sum of the numbers to the left and right in the previous row. --- The function ;pascal; produces the triangle to a given depth. module PascalsTriangle; open import Stdlib.Prelude; zipWith : {A : Type} → {B : Type} → {C : Type} → (A → B → C) → List A → List B → List C; zipWith f nil _ := nil; zipWith f _ nil := nil; zipWith f (x ∷ xs) (y ∷ ys) := f x y ∷ zipWith f xs ys; --- Return a list of repeated applications of a given function iterate : {A : Type} → Nat → (A → A) → A → List A; iterate zero _ _ := nil; iterate (suc n) f a := a ∷ iterate n f (f a); --- Produce a singleton List singleton : {A : Type} → A → List A; singleton a := a ∷ nil; infixr 5 ++str; --- Concatenation of ;String;s axiom ++str : String → String → String; compile ++str { c ↦ "concat"; }; --- Concatenates a list of strings --- ;concat (("a" ∷ nil) ∷ "b" ∷ nil); evaluates to ;"a" ∷ "b" ∷ nil; concat : List String → String; concat := foldl (++str) ""; intercalate : String → List String → String; intercalate sep xs := concat (intersperse sep xs); --- Joins a list of strings with the newline character unlines : List String → String; unlines := intercalate "\n"; showList : List Nat → String; showList xs := "[" ++str intercalate "," (map natToStr xs) ++str "]"; --- Compute the next row of Pascal's triangle pascalNextRow : List Nat → List Nat; pascalNextRow row := zipWith (+) (singleton zero ++ row) (row ++ singleton zero); --- Produce Pascal's triangle to a given depth pascal : Nat → List (List Nat); pascal rows := iterate rows pascalNextRow (singleton one); main : IO; main := putStrLn (unlines (map showList (pascal 10))); end;