4 ms·

Actually I just realized that the law does not hold, the type `Void -> Maybe Void` has two inhabitants, not one: f1 x = Nothing f2 x = Just x

• yummyfajitas 11y ago
  `Just x` cannot be constructed since there is no `x` which is has type `Void`.
  • tel 11y ago
    Well, there's the one in context that does! Except this function can never be called in an empty context so you ultimately are stuck.
  • bweitzman 11y ago
    `Just x` can be constructed given an `x`. The fact that no `x` can be given is somewhat irrelevant to the definition of the function.
• wz1000 11y ago
  Both of them are regarded as the same function(ignoring bottom) because there is no way to differentiate between them as you can never supply them with a value of type Void in order to see their result.
  • bweitzman 11y ago
    They are similar in that they cannot be applied to any non-bottom value, but they are definitely not the same function.
    • sjolsen 11y ago
      >they are definitely not the same function This depends on what equivalence you're using, and the only one in which it's true (definitional equality) isn't very interesting. Extensionally, the functions are identical.
      • bweitzman 11y ago
        Ignoring, bottom, the functions arguably have no extensionality, and therefore are only vacuously equivalent in that sense.