何かのタネ

Esty.idr

-- :l Esty
module Esty

%default total
%hide fib
%hide fact

syntax "sif(" [t] "," [e] ")." [bool] = ifThenElse bool t e

namespace Fun
  -- 階乗、ポイントフリーにはできない
  partial
  fact : Nat -> Nat
  fact x = sif(1, (*x) . fact . (flip minus 1) $ x). (0==) $ x

  -- フィボナッチ
  partial
  fib : Nat -> Nat
  fib x = sif((sif(0, 1). (0==) $ x), (+ fib . (flip minus 2) $ x) . fib . (flip minus 1) $ x). (1>=) $ x

  -- コラッツ
  partial
  collatz : Nat -> List Nat
  collatz x = col x [x] where
    col x ls = sif(ls, sif(col d $ d :: ls, col m $ m :: ls). t). (1==) $ x
    partial
    d : Nat
    d = div x 2
    m : Nat
    m = 3 * x + 1
    partial
    t : Bool
    t = (0==) $ mod x 2