Friday, March 03, 2017

Trust in Schönfinkel

I'm working through the "20 Intermediate Exercises" that give Functors and Monads and such cute, non-threatening names and ask you to implement them. I've gotten most of the way through, with three or four that I'm stuck on--that's under the assumption that the inductive step from banana to banana2 will make the rest of the banana<n> obvious. (If you have sausage, it's easy to implement moppy, and vice versa, but avoiding circularity is the issue.)

So... I did a Bad Thing and looked at solutions a couple of people have posted, saying to myself, "OK, I'll look at those I've already done with an eye to more elegant expression, and look at the ones I'm having issues with and make sure I understand"... and came face to face with a question about composition.

<andy_rooney>Didja ever notice that the examples of composition you see are what we think of as functions with one argument?</andy_rooney> Well, one of the solutions involved composition that does not have that constraint, and that caused me much puzzlement until I remembered that we are, after all, using Haskell, where every function just has one argument. All it means is that the left-hand operand of (.) had better want to be passed a function...which is why the very next thing I typed at ghci just for the heck of it was stupid:

Prelude> :t ((+) . (-))
((+) . (-)) :: (Num a, Num (a -> a)) => a -> (a -> a) -> a -> a

Uh, yeah. I am pretty sure no function type is in Num, but what the heck, let's bind it to a name.

Prelude> let foo = ((+) . (-))

    Non type-variable argument in the constraint: Num (a -> a)
    (Use FlexibleContexts to permit this)
    When checking that ‘foo’ has the inferred type
      foo :: forall a. (Num a, Num (a -> a)) => a -> (a -> a) -> a -> a

Didn't expect that. Perhaps ghci isn't quite as strict when you're just asking for the type.

UPDATE: I see why the solution didn't look type correct to me. I didn't understand Hindley-Milner well enough. It must be willing to do things like decide "to make this work, type a over here must map to type a -> b over there" in such a way that all is consistent. Now I know what to learn next.

A flashback and analogy

You've probably heard about how the notion of sum types (e.g. Algol 68 union s, Rust enum s, Haskell type s) and product types (e.g. tup...