MonadFail proposal (MFP): Moving fail out of Monad

Felipe Lessa felipe.lessa at
Thu Jun 11 15:15:53 UTC 2015

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.


  (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?



-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
URL: <>

More information about the Libraries mailing list