You can't use fmap to "break out" of a Functor, since its return type is still wrapped in the functor: fmap : (a -> b) -> Maybe a -> Maybe b Likewise we c

You can't use fmap to "break out" of a Functor, since its return type is still wrapped in the functor: fmap : (a -> b) -> Maybe a -> Maybe b Likewise we can't escape from an Applicative: (<*>) : Maybe (a -> b) -> Maybe a -> Maybe b Nor from a Monad: (>>=) : Maybe a -> (a -> Maybe b) -> Maybe b Dependently typed languages use these all the time, but they also allow you to write a function: unMaybe : (A : Type) -> Maybe A -> Type unMaybe _ Nothing = _|_ -- Empty type; impossible to satisfy unMaybe A (Just _) = A -- The raw element type And use it like this: unWrap : (x : Maybe a) -> unMaybe a x unWrap Nothing = ...insert proof that you'll never get a Nothing here... unWrap (Just x) = x I haven't included a proof, since it depends completely on the application, but it's easy to understand how it works. In the "Just" case, we need to return a value of type "a", which is trivial. In the "Nothing" case, we need to return a value of type "_|_", but we no that there aren't any! The only way we can satisfy the type checker is to return a value of type _|_, and the only way we can do that is if we already have such a value. In other words, to get an impossible value we must be in an impossible branch. Hence we can prove by contradiction that the "Nothing" will never be taken!