2 ms·

I'm talking about the `jonk :: (a -> b) -> ((a -> Int) -> Int) -> ((b -> Int) -> Int)` extended example that you work through. Or take the haskell filter funct

I'm talking about the `jonk :: (a -> b) -> ((a -> Int) -> Int) -> ((b -> Int) -> Int)` extended example that you work through. Or take the haskell filter function: `filter :: (a -> Bool) -> [a] -> [a]`. Some googling says that there's no opposite function for filter, but it's present in a lot of languages, so let's pretend there is. The signature would be the same: `filterNot :: (a -> Bool) -> [a] -> [a]`. Just looking at the types, filling type holes, wouldn't distinguish those two functions—the difference isn't in the types, but in their behavior.

whateveracct 7y ago
That's true (and mostly is due to the concrete nature of Bool) but even so, parametricity does help a lot implementing that function. `forall a.` cuts down on possible implementations, but you still gotta program sometimes :) In a more dependently-typed language, we can write something like this f1 :: (p :: a -> Bool) -> [a] -> [a `suchThat` p a] f2 :: (p :: a -> Bool) -> [a] -> [a `suchThat` not (p a)] and that would make it so f1 couldn't be filterNot and f2 couldn't be filter. And we get the added benefit of giving the caller of our function the proof that the elements have passed that predicate (maybe they can make use of that downstream) But even in this case, there's nothing stopping you from just always returning an empty list. Not all theorems come for free!