Int = <pos : Nat, neg : Nat>;

fminus =
  fix (lambda f : Nat -> Nat -> Int.
    lambda n : Nat. lambda m : Nat.
      if iszero m then
        <pos = n> as Int
      else if iszero n then
        <neg = m> as Int
      else
        f (pred n) (pred m));

divides =
  lambda m : Nat.
    fix (lambda f : Nat -> Bool. lambda n : Nat.
      case fminus n m of
        <pos = x> ==> f x
      | <neg = y> ==> iszero n);

NatStream = Rec X. Unit -> {hd : Nat, tl : X};
NatStreamCell = {hd : Nat, tl : NatStream};

nats2 =
  fix (lambda f : Nat -> NatStream. lambda n : Nat.
    lambda u : Unit. {hd = n, tl = f (succ n)}) 2;

filter =
  lambda p : Nat.
    fix (lambda f : NatStream -> NatStream.
      lambda s : NatStream.
        lambda u : Unit.
          let c = s unit in
          if divides p c.hd then
            f c.tl unit
          else
            {hd = c.hd, tl = f c.tl});

sieve =
  fix (lambda f : NatStream -> NatStream. lambda s : NatStream.
    lambda u : Unit.
      let c = s unit in
      {hd = c.hd,
       tl = f (filter c.hd c.tl)});

primes = sieve nats2;

NatList = Rec X. <nil : Unit, cons : {hd : Nat, tl : X}>;

nil = <nil = unit> as NatList;

cons =
  lambda h : Nat. lambda t : NatList.
    <cons = {hd = h, tl = t}> as NatList;

take =
  fix (lambda f : Nat -> NatStream -> NatList.
    lambda n : Nat. lambda s : NatStream.
      if iszero n then
        nil
      else
        let c = s unit in
        cons c.hd (f (pred n) c.tl));

take 10 primes;
