MonadFail proposal (MFP): Moving fail out of Monad

[Wolfgang Jeltsch]

Am Donnerstag, den 11.06.2015, 12:15 -0300 schrieb Felipe Lessa:
> On 11-06-2015 12:08, Wolfgang Jeltsch wrote:
> >> A class of patterns that are conditionally failable are `newtype`s,
> >> and single constructor `data` types, which are unfailable by
> >> themselves, but may fail if matching on their fields is done with
> >> failable paterns.
> > 
> > The part about single-constructor data types is not true. A
> > single-constructor data type has a value ⊥ that is different from
> > applying the data constructor to ⊥’s. For example, ⊥ and (⊥, ⊥) are two
> > different values. Matching ⊥ against the pattern (_, _) fails, matching
> > (⊥, ⊥) against (_, _) succeeds. So single-constructor data types are not
> > different from all other data types in this respect. The dividing line
> > really runs between data types and newtypes. So only matches against
> > patterns C p where C is a newtype constructor and p is unfailable should
> > be considered unfailable.
> 
> I think that being failable is a property that is undefined for
> undefined.  Ok, sorry :), what I mean is that you can't do anything to
> distinguish C p from _|_ within pure code.
> 
> For example:
> 
>   Just a <- x
> 
> You can distinguish Just a from Nothing in pure code, so that gets
> translated to a pattern match and a fail call.
> 
> However:
> 
>   (a, b) <- x
> 
> You can't distinguish (a, b) from _|_.  In other words, the pattern (a,
> b) covers every possible value of its type.  So it doesn't need a fail
> call.  And it doesn't matter if it's a newtype or a single-constructor
> data type.  Makes sense?

Well, the pattern (a, b) does not cover every possible value, but every
non-⊥ value, but you cannot use pattern matching to choose a different
branch for ⊥, since matching ⊥ against any refutable pattern, like
(a, b), results in a runtime error. Makes sense. :-) 

All the best,
Wolfgang