[Haskell-cafe] Haskell Propeganda

[Jonathan Cast]

On Wed, 2008-08-27 at 13:34 -0700, Aaron Tomb wrote:
> On Aug 27, 2008, at 12:23 PM, Dan Weston wrote:
> 
> > Huh? Type safety buys you not having to worry about dereferencing  
> > stale nonnull pointers (lifetime of reference exceeding lifetime of  
> > referent), but nothing about dereferencing null pointers, which are  
> > the moral equivalent of Nothing.
> 
> What type safety buys you, in my mind, is that Nothing is only a valid  
> value for explicit Maybe types. In cases where you don't use Maybe,  
> the "null" situation just can't occur. In languages with null  
> pointers, any pointer could possibly be null.
> 
> When you do use Maybe, you have to explicitly handle the Just and  
> Nothing cases separately. Pattern matching reminds you that both are  
> possible. I tend to view fromJust as a function you should only use if  
> you're _very_, _very_ sure that the Nothing case is impossible. But,  
> if so, why are you using a Maybe type in the first place?

Consider:

 substType v ty x = fromJust $
           do
              TyVar s <- cast x
              guard $ v == s 
              cast ty
   `mplus` do
              ForAll s ty' <- cast x
              guard $ v == s
              cast $ ForAll s ty'
   `mplus` do
              ForAll s ty' <- cast x
              guard $ s `Set.member` freeTV ty
              let
                v' = Set.findMax (freeTV ty `Set.union` freeTV ty') ++
"1"
                ty'' = substType v ty $ substType s (TyVar v') $ ty'
              cast $ ForAll v' ty''
   `mplus` do
              ForAll s ty' <- cast x
              cast $ ForAll s $ substType v ty ty'
   `mplus` do
              TyLambda s ty' <- cast x
              guard $ v == s
              cast $ TyLambda s ty'
   `mplus` do
              TyLambda s ty' <- cast x
              guard $ s `Set.member` freeTV ty
              let
                v' = Set.findMax (freeTV ty `Set.union` freeTV ty') ++
"1"
                ty'' = substType v ty $ substType s (TyVar v') $ ty'
              cast $ TyLambda v' ty''
   `mplus` do
              TyLambda s ty' <- cast x
              cast $ TyLambda s $ substType v ty ty'
   `mplus` do return $ gmapT (substType v ty) x

 ForAll :: String -> Type -> Type
 TyLambda :: String -> Expr -> Expr

The last `case' is a catch-all, so you do know the result of the mplus's
is a Just, but you still need the Maybe.

jcc