> Why is it illogical to say that a Maybe a -> b should be callable as if it were a -> b?
Fundamentally because it would require you to conjure up a value of type b from nowhere when the Maybe a is Nothing. If we view the function type as implication this would not be valid logically without some way of introducing that value of type b.
You could imagine some function from Nothing -> b that could rescue us. But since it only handles one case of the Maybe type, it is partial (meaning it could give undefined as an answer). There is basically two total functions that we could change it to:
* Maybe a -> b in which case we are back where we started.
* Unit -> b which essentially is just b, which can be summed up as meaning we need some kind of default value to be available at all times.
So to be able to call Maybe a -> b as a -> b you would need some default value available at all the call sites for a -> b
Now this is only "illogical" because we don't postulate a value of type b to be used as this default.
> It's like saying (+) works on integers, but not on 3
No, it's like saying (+) must work on all integers AND a special value nil that is not like any other integers, but somehow included in them and all other data types. We can't do anything with this nil value since it doesn't carry any data, so in the case of (+) we would essentially have to treat it as an identity element.
This is good though, since (+) has 0 as an identity element, so we can just treat nil as a 0 when we encounter (+). However, when we want to define multiplication we still need to treat nil as an identity element (since it still doesnt carry any data), except the identity element for multiplication is 1. This would be repeated for every new function that deals with integers.
So by mashing together Maybe and Integer we have managed to get a frankenstein data type with an extra element nil which sometimes means 0 and sometimes means 1.
Why not just decompose them into Maybe and Integer and supply the default argument with a simple convertion function like fromMaybe?
(FWIW, I actually agree with Hickey that using Maybe in api design is problematic and I've encountered what he's talking about. But while that might be an argument for where he wants to take Clojure, it's not an argument for dismissing type theory the way he does.)
Yeah, you're right, I got confused when interpreting the parent comment. Thanks for pointing it out!
I guess I overlooked it because the other way is so logically trivial, since it basically boils down to A -> B => (A || Nothing) -> B, which is just an or-introduction. So if you wanna implement Maybe generically the "work" lies on the other side.
But since Hickey's argument sort of is that we shouldn't implement Maybe generically, I guess my argument here becomes circular. (Begging the question maybe?)
> I guess I overlooked it because the other way is so logically trivial, since it basically boils down
Yeah, that's (part of) Hickey's point. That the "best" type systems fail this test, and require manual programmer work to solve this problem. Again, I'm saying this as someone who really appreciates Haskell.
Fundamentally because it would require you to conjure up a value of type b from nowhere when the Maybe a is Nothing. If we view the function type as implication this would not be valid logically without some way of introducing that value of type b.
You could imagine some function from Nothing -> b that could rescue us. But since it only handles one case of the Maybe type, it is partial (meaning it could give undefined as an answer). There is basically two total functions that we could change it to:
So to be able to call Maybe a -> b as a -> b you would need some default value available at all the call sites for a -> bNow this is only "illogical" because we don't postulate a value of type b to be used as this default.
> It's like saying (+) works on integers, but not on 3
No, it's like saying (+) must work on all integers AND a special value nil that is not like any other integers, but somehow included in them and all other data types. We can't do anything with this nil value since it doesn't carry any data, so in the case of (+) we would essentially have to treat it as an identity element.
This is good though, since (+) has 0 as an identity element, so we can just treat nil as a 0 when we encounter (+). However, when we want to define multiplication we still need to treat nil as an identity element (since it still doesnt carry any data), except the identity element for multiplication is 1. This would be repeated for every new function that deals with integers.
So by mashing together Maybe and Integer we have managed to get a frankenstein data type with an extra element nil which sometimes means 0 and sometimes means 1.
Why not just decompose them into Maybe and Integer and supply the default argument with a simple convertion function like fromMaybe?
(FWIW, I actually agree with Hickey that using Maybe in api design is problematic and I've encountered what he's talking about. But while that might be an argument for where he wants to take Clojure, it's not an argument for dismissing type theory the way he does.)