
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