calculus/Calculus/Lambda/Omega/Explicit/lib/Either.cloe

   1 Either_Polytype (L:*) (R:*) : *p
   2  = (Data:*) -> (L -> Data) -> (R -> Data) -> Data
   3 Either (L:*) (R:*) : *m
   4  = Monotype (Either_Polytype L R)
   5 Left (L:*) (R:*) (l:L) : Either L R
   6  = monotype (Either_Polytype L R)
   7     (λ(Data:*) (Left:L -> Data) (Right:R -> Data) -> Left l)
   8 Right (L:*) (R:*) (r:R) : Either L R
   9  = monotype (Either_Polytype L R)
  10     (λ(Data:*) (Left:L -> Data) (Right:R -> Data) -> Right r)
  11
  12 left (L:*) (R:*) (l:L)
  13  : Either L R
  14  = monotype (Either_Polytype L R)
  15    (λ(Data:*) (Left:L -> Data) (Right:R -> Data) -> Left l)
  16 right (L:*) (R:*) (r:R)
  17  : Either L R
  18  = monotype (Either_Polytype L R)
  19    (λ(Data:*) (Left:L -> Data) (Right:R -> Data) -> Right r)
  20 either
  21  (L:*) (R:*) (Data:*)
  22  (l:L -> Data)
  23  (r:R -> Data)
  24  (e:Either L R)
  25  : Data
  26  = polytype (Either_Polytype L R) e Data l r
  27
  28 :load Monad.cloe
  29 Monad_return_Either (L:*) (X:*)
  30  : Monad_Return (Either L) X
  31  = Right L X
  32 Monad_bind_Either (L:*) (X:*) (Y:*)
  33  : Monad_Bind (Either L) X Y
  34  = λ(mx:Either L X) (my:X -> Either L Y) ->
  35      either L X (Either L Y) (Left L Y) my mx
  36 Monad_Either (L:*)
  37  : Monad (Either L)
  38  = monad (Either L)
  39  (Monad_return_Either L)
  40  (Monad_bind_Either L)