data Maybe () where { Nothing : Maybe Just : Int -> Maybe }; fmap : (Int -> Int) -> Maybe -> Maybe ; fmap f ma = case ma of { Nothing => Nothing ; Just a => Just (f a) ; }; pure : Int -> Maybe ; pure x = Just x ; ap mf ma = case mf of { Just f => case ma of { Nothing => Nothing; Just a => Just (f a); }; Nothing => Nothing; }; return = pure; bind ma f = case ma of { Nothing => Nothing ; Just a => f a ; };