Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

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



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.


They are similar in that they cannot be applied to any non-bottom value, but they are definitely not the same function.


>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.


Ignoring, bottom, the functions arguably have no extensionality, and therefore are only vacuously equivalent in that sense.


`Just x` cannot be constructed since there is no `x` which is has type `Void`.


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.


`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.




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: