; Iter 15d — third stdlib module: tagged-disjoint values.
; Either<e, a> is the canonical 2-type-var ADT. First stdlib module
; with two type parameters; first to ship an eliminator combinator
; (`either`) that introduces a third type var on top of the data.

(module std_either

  (data Either (vars e a)
    (doc "Disjoint sum: Left<e> for the failure branch, Right<a> for the success branch. Right is the conventional 'success' side.")
    (ctor Left e)
    (ctor Right a))

  (fn from_right
    (doc "Project the Right<a> payload, or use the default for Left<_>.")
    (type
      (forall (vars e a)
        (fn-type
          (params a (con Either e a))
          (ret a))))
    (params default x)
    (body
      (match x
        (case (pat-ctor Right v) v)
        (case (pat-ctor Left _) default))))

  (fn is_left
    (doc "Returns true iff x is Left<_>.")
    (type
      (forall (vars e a)
        (fn-type
          (params (con Either e a))
          (ret (con Bool)))))
    (params x)
    (body
      (match x
        (case (pat-ctor Left _) true)
        (case (pat-ctor Right _) false))))

  (fn is_right
    (doc "Returns true iff x is Right<_>.")
    (type
      (forall (vars e a)
        (fn-type
          (params (con Either e a))
          (ret (con Bool)))))
    (params x)
    (body
      (match x
        (case (pat-ctor Left _) false)
        (case (pat-ctor Right _) true))))

  (fn map_right
    (doc "Apply f to the Right<a> payload; pass Left<e> through untouched.")
    (type
      (forall (vars e a b)
        (fn-type
          (params (fn-type (params a) (ret b))
                  (con Either e a))
          (ret (con Either e b)))))
    (params f x)
    (body
      (match x
        (case (pat-ctor Right v)
          (term-ctor Either Right (app f v)))
        (case (pat-ctor Left l)
          (term-ctor Either Left l)))))

  (fn either
    (doc "Eliminator: apply on_left to a Left payload, on_right to a Right payload, fold both branches into the same result type c.")
    (type
      (forall (vars e a c)
        (fn-type
          (params (fn-type (params e) (ret c))
                  (fn-type (params a) (ret c))
                  (con Either e a))
          (ret c))))
    (params on_left on_right x)
    (body
      (match x
        (case (pat-ctor Left l) (app on_left l))
        (case (pat-ctor Right r) (app on_right r))))))