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

   1 Maybe_Polytype (X:*) : *p
   2  = (Data:*) -> Data -> (X -> Data) -> Data
   3 Maybe (X:*) : *m
   4  = Monotype (Maybe_Polytype X)
   5 Nothing (X:*) : Maybe X
   6  = monotype (Maybe_Polytype X)
   7    (λ(Data:*) (Nothing:Data) (Just:X -> Data) -> Nothing)
   8 Just (X:*) (x:X) : Maybe X
   9  = monotype (Maybe_Polytype X)
  10    (λ(Data:*) (Nothing:Data) (Just:X -> Data) -> Just x)
  11 maybe (X:*) (Data:*) (nothing:Data) (just:X -> Data) (m:Maybe X) : Data
  12  = polytype (Maybe_Polytype X) m Data nothing just
  13
  14 :load Monad.cloe
  15 Monad_return_Maybe
  16  (X:*)
  17  : Monad_Return Maybe X
  18  = Just X
  19 Monad_bind_Maybe
  20  (X:*) (Y:*)
  21  : Monad_Bind Maybe X Y
  22  = λ(mx:Maybe X) (my:X -> Maybe Y) ->
  23      maybe X (Maybe Y) (Nothing Y) my mx
  24 Monad_Maybe
  25  : Monad Maybe
  26  = monad Maybe
  27  Monad_return_Maybe
  28  Monad_bind_Maybe