Maybe.lol

Maybe_Polytype (X:*) : *p
 = (Data:*) -> Data -> (X -> Data) -> Data
Maybe (X:*) : *m
 = Monotype (Maybe_Polytype X)
Nothing (X:*) : Maybe X
 = monotype (Maybe_Polytype X)
   (λ(Data:*) (Nothing:Data) (Just:X -> Data) -> Nothing)
Just (X:*) (x:X) : Maybe X
 = monotype (Maybe_Polytype X)
   (λ(Data:*) (Nothing:Data) (Just:X -> Data) -> Just x)
maybe (X:*) (Data:*) (nothing:Data) (just:X -> Data) (m:Maybe X) : Data
 = polytype (Maybe_Polytype X) m Data nothing just

:load Monad.lol
Monad_return_Maybe
 (X:*)
 : Monad_Return Maybe X
 = Just X
Monad_bind_Maybe
 (X:*) (Y:*)
 : Monad_Bind Maybe X Y
 = λ(mx:Maybe X) (my:X -> Maybe Y) ->
     maybe X (Maybe Y) (Nothing Y) my mx
Monad_Maybe
 : Monad Maybe
 = monad Maybe
 Monad_return_Maybe
 Monad_bind_Maybe