Given these two procedures (written in JavaScript) …
// comp :: (b -> c) -> (a -> b) -> (a -> c)
const comp = f=> g=> x=> f (g (x))
// comp2 :: (c -> d) -> (a -> b -> c) -> (a -> b -> d)
const comp2 = comp (comp) (comp)
My question is how to derive comp2's Hindley-Milner Type without referencing comp's implementation
If we know comp's implementation, it's easy … We can use the substitution model through the entire evaluation to arrive at the expanded expression …
comp (comp) (comp)
= (f => g => x => f (g (x))) (comp) (comp)
= x => comp (comp (x))
= y => comp (comp (y))
= y => (f => g => x => f (g (x))) (comp (y))
... keep going until ...
= f=> g=> x=> y=> f (g (x) (y))Ring-a-ding. The expanded evaluation matches comp2's type. No one is impressed.
// comp2 :: (c -> d) -> (a -> b -> c) -> (a -> b -> d)
const comp2 = f=> g=> x=> y=> f (g (x) (y))
But what if we only knew comp's type and did not know its implementation? Instead of evaluating the code to determine the type, could I have performed some sort of substitutions/evaluation on comp's type to end up with comp2's type ?
Given only this, the problem becomes much harder … (at least for me)
// comp :: (b -> c) -> (a -> b) -> (a -> c)
// comp2 :: ???
const comp2 = comp (comp) (comp)There's gotta be a way, right ? Isn't this what algebraic data types are all about?
Let's look at a simplified example to clarify my question: If we have a function like add and map …
// add :: Number -> Number -> Number
// map :: (a -> b) -> [a] -> [b]
If we wanted to define a function using map and add we could figure out the type systematically without knowing add or map's implementation
// add :: Number -> Number -> Number
// map :: (a -> b) -> [a] -> [b]
// add6 :: Number -> Number
let add6 = add (6)
// mapAdd6 :: [Number] -> [Number]
let mapAdd6 = map(add6)
This is really powerful because it allows you to reason about code you didn't make without having to go digging through the implementation (as much)
However, when trying to do it with the comp2 example, I get stuck pretty quick
// comp :: (b -> c) -> (a -> b) -> (a -> c)
// comp2 :: ??
const comp2 = comp (comp) (comp)
// initial type
(b -> c) -> (a -> b) -> (a -> c)
// apply to comp once ... ???
[(b -> c) -> (a -> b) -> (a -> c)] -> (a -> b) -> (a -> c)
// apply the second time ... ???
[(b -> c) -> (a -> b) -> (a -> c)] -> [(b -> c) -> (a -> b) -> (a -> c)] -> (a -> c)
// no... this can't be right
HOW TO HINDLEY MILNER
Let’s see what we know. Let’s look at comp2’s implementation in isolation:
comp2 = comp comp comp
And let’s consider comp’s type signature:
comp :: (b -> c) -> (a -> b) -> (a -> c)
Now, the result of comp2 is going to be the result of comp applied to two arguments, which is the far right hand side of the comp type signature. Therefore, we know that the type of comp2 is of type a -> c, we just don’t know what a and c are yet.
However, we can figure it out. We can work through this by hand by manually unifying types (by knowing that two types need to be the same), then substituting known type variables with their concrete types. The two arguments are both comp, but they should have different types: b -> c and a -> b, respectively. Let’s add some type annotations to make that a little more clear:
comp2 = (comp (comp :: b -> c)
(comp :: a -> b))
We can first attempt to unify b -> c with the type of comp to determine what b and c are, but we’ll need to do some alpha-renaming so that our variable names don’t collide:
b -> c
(b1 -> c1) -> (a1 -> b1) -> (a1 -> c1)
b = b1 -> c1
c = (a1 -> b1) -> (a1 -> c1)
Next, we can do the same thing with the second argument, unifying with the type a -> b:
a -> b
(b2 -> c2) -> (a2 -> b2) -> (a2 -> c2)
a = b2 -> c2
b = (a2 -> b2) -> (a2 -> c2)
But wait! We now have two different definitions for the same type variable, b, so those must unify as well. Let’s perform the same process for these two types:
b1 -> c1
(a2 -> b2) -> (a2 -> c2)
b1 = a2 -> b2
c1 = a2 -> c2
Now, returning to the original type we gave for comp2, we can perform a series of substitutions to end up with a complete type:
a -> c | type of comp2, from the return type of comp
(b2 -> c2) -> c | substituting the definition of a
(b2 -> c2) -> (a1 -> b1) -> (a1 -> c1) | substituting the definition of c
(b2 -> c2) -> (a1 -> (a2 -> b2)) -> (a1 -> c1) | substituting the definition of b1
(b2 -> c2) -> (a1 -> (a2 -> b2)) -> (a1 -> (a2 -> c2)) | substituting the definition of c1
(b2 -> c2) -> (a1 -> a2 -> b2) -> a1 -> a2 -> c2 | removing unnecessary parentheses
(c -> d) -> (a -> b -> c) -> a -> b -> d | alpha renaming
You will notice that this is the same as your manually-prescribed type.