example of function definitions with lazar

lazar-example.scm

;; α | Any | a'        => literally any type
;; Num { ℕ | ℤ | ... } => numerical tower, natural numbers, integers etc.
;; Fn                  => procedure/function
;; Ø? (null list predicate), Ø (null list), ¬ (negation, not)
;; hd (car = first of list), tl (cdr = all but first of list), :: (cons operator)

(define/c (foldl ((f : Fn) (n : α) (xs : List)) -> α)
  (case-with || (Ø? xs) => n
             || _       => (foldl f (f n (hd xs)) (tl xs))))

(define/c (foldr ((f : Fn) (n : α) (xs : List)) -> α)
  (case-with || (Ø? xs) => n
             || _       => (f (hd xs) (foldr f n (tl xs)))))

(define/c (map ((f : Fn) (xs : List)) -> List)
  (case-with || (Ø? xs) => Ø
             || _       => (:: (f (hd xs)) (map f (tl xs)))))

(define/c (sum (xs : (ListOf Num)) -> Num)
  (case-with || (Ø? xs)       => Ø
             || (¬ (List xs)) => ⊥
             || _             => (foldl + 0 xs)))

(define/c (last (xs : List) -> α)
  (case-with || (Ø? xs) => Ø
             || _       => (foldl (λ x y => y) Ø xs)))

(define/c (rev (xs : List) -> List)
  (ε rec aux (λ x y =>
              (case-with || (Ø? x) => y
                         || _      => (aux (tl x) (:: (hd x) y))))
     in (aux xs Ø)))

(define/c (zip-with ((f : Fn) (xs : List) (ys : List)) -> List)
  (ε rec aux (λ f x y acc =>
                (case-with || (⋁ (Ø? x) (Ø? y)) => (rev acc)
                           || _                 => (aux f (tl x) (tl y)
                                                      (:: (f (hd x) (hd y)) acc))))
     in (aux f xs ys Ø)))

;; list-ref with idx starting at 1
(define/c (list-ref ((xs : List) (n : ℕ)) -> α)
  (case-with || (Ø? xs) => ⊥
             || (1? n)  => (hd xs)
             || _       => (list-ref (tl xs) (∇ n))))

(define/c (factorial (n : ℕ) -> ℕ)
  (ε rec aux (λ n acc =>
                (if (0? n) acc
                    (aux (∇ n) (* n acc))))
     in (aux n 1)))