2 ms·

The point is that in Haskell, once you start chaining Maybes together you are forced to deal with the Nothings, even if they won't actually arise. For example:

The point is that in Haskell, once you start chaining Maybes together you are forced to deal with the Nothings, even if they won't actually arise. For example: :t Data.Map.lookup 123 (singleton 123 "hello") Data.Map.lookup 123 (singleton 123 "hello") :: Maybe [Char] Even though this lookup will clearly succeed, I am forced to handle the Nothing case. Dependent types let me encode more information about the value in my types, providing evidence that it will always be a Just, which I can use at compile time to convince the type checker that the Nothing case is unreachable. As soon as the Nothing case is unreachable, I can easily unwrap the Maybe, since my only remaining branch is a "Just x", so I can simply return "x".

codygman 12y ago
fmap is very useful for dealing with Maybes also: Prelude M> import qualified Data.Map as M Prelude M> let val = M.lookup 123 (M.singleton 123 "hello") Prelude M> fmap reverse val Just "olleh" So this means that you only deal with the chained maybes at the top level or in a call-site that needs to know a Nothing existed as the Nothings are propagated.
- chriswarbo 12y ago
  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!

codygman 12y ago

fmap is very useful for dealing with Maybes also: Prelude M> import qualified Data.Map as M Prelude M> let val = M.lookup 123 (M.singleton 123 "hello") Prelude M> fmap reverse val Just "olleh" So this means that you only deal with the chained maybes at the top level or in a call-site that needs to know a Nothing existed as the Nothings are propagated.

chriswarbo 12y ago
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!