How to figure out the type of this function?

Question

I try to figure out the type of the OCaml function below:

let subst = fun x -> fun y -> fun z -> x z (y z)

(* Or more concisely *)
let subst x y z = x z (y z)

Here's my derivation.

Step 1, assume the type of x, y, and z, and the output value of subst as below:

x: 'a
y: 'b
z: 'c
subst: 'a -> 'b -> 'c -> 'd

Step 2, notice that both x and y can be applied to z, so we get: (two more types are introduced, 'e and 'f)

'a = 'c -> 'e
'b = 'c -> 'f
(y z):'f

Step 3, notice that (x z) can be applied to (y z):'f, so we get:

(x z) : 'f -> 'd  (* note that 'd is the type of the final output value *)

Step 4, recall that we have x : 'c -> 'e, and the type of x's output is unique, so with step 3 we get:

'e = 'f -> 'd

Step 5, expand all and we get:

'a = 'c -> 'e = 'c -> 'f -> 'd   (* type of x, actually I am a bit uncertain about the expansion of 'e to 'f -> 'd *)
'b = 'c -> 'f  (* type of y *)
'c    (* type of z *)

Finally, the type of the function subst is:

subst: ('c -> 'f -> 'd) -> ('c -> 'f) -> 'c ->   'd
       ----------------    ----------    ---   -------
              x                y          z     output

Replace c, f, d with a, b, c, we get:

subst: ('a -> 'b -> 'c) -> ('a -> 'b) -> 'a -> 'c

I am new to type theory and functional programming. I'm not sure if my derivation is optimal or even correct. Could anyone provide some insight?

Is there any better solution?

Question edited by removing the tend-to-be off-topic content. — smwikipedia
– smwikipedia, Commented Feb 12 at 1:47
You're still explicitly asking for opinion (which is the close reason, not being off-topic). I do however also consider this question too broad, and perhaps also too theoretical for Stack Overflow, which is generally focused on practical programming questions, while more theoretical questions belong on Computer Science. — glennsl
– glennsl, Commented Feb 12 at 9:21
I think this is kind of like algorithm optimization. And that should be appropriate for SO. — smwikipedia
– smwikipedia, Commented Feb 13 at 1:40

smwikipedia · Accepted Answer · 2025-02-13 06:48:43Z

0

I just found a shorter way to infer the type of the function subst.

The key is to start from the right-most variable z.

Step 1, assume z : 'a.

Step 2, it must hold y : 'a -> 'b because of y z.

Step 3, it must hold x : 'a -> 'c because of x z.

Step 4, it must hold 'c = 'b -> 'd because (x z) can be applied to (y z). So x : 'a -> 'b -> 'd. And btw, 'd is the type of subst output.

So the type of subst is:

('a -> 'b -> 'd) -> ('a->'b) -> 'a -> 'd

Replace 'd with 'c:

('a -> 'b -> 'c) -> ('a->'b) -> 'a  ->   'c
----------------    --------    ---    ------
       x                y        z      output

However, I am not sure if this right-most trick is universal or not.

edited Feb 13 at 6:48

answered Feb 13 at 6:43

smwikipedia

65k98 gold badges333 silver badges519 bronze badges

Sign up to request clarification or add additional context in comments.

Comments

Chris · Accepted Answer · 2025-02-14 21:08:17Z

0

Not quite how I'd approach this. Your approach isn't wrong per se, but it feels overly complex.

let subst x y z = x z (y z)

What's the first thing we can grasp about this?

x is a function which takes two arguments.
y is a function which takes one argument.
z is something
And of course, subst must return something.

So if we give these types some names in alphabetical order we get the following. Then we'll see which ones must be the same by applying logic.

('a -> 'b -> 'c) -> ('d -> 'e) -> 'f -> 'g

First thing we can notice: the return type of fully applying x must be the return type of subst, so the 'c and 'g types unify.

('a -> 'b -> 'c) -> ('d -> 'e) -> 'f -> 'c

Next: z is passed as the first argument to x, so the 'a and 'f types unify.

('a -> 'b -> 'c) -> ('d -> 'e) -> 'a -> 'c

But z is also passed as the first argument to y, so 'a and 'd unify.

('a -> 'b -> 'c) -> ('a -> 'e) -> 'a -> 'c

And finally the result of (y z) is passed as the second argument to x, so 'b and 'e unify.

('a -> 'b -> 'c) -> ('a -> 'b) -> 'a -> 'c

And there we have it. At each step I had fewer type variables to reason about.

An example from the standard library

If we looked at something like List.fold_left:

let rec fold_left f accu l =
  match l with
    [] -> accu
  | a::l -> fold_left f (f accu a) l

We know fold_left takes three arguments.
We can see that f is a function which takes two arguments.
We can see from the pattern match that l is a list.

('a -> 'b -> 'c) -> 'd -> 'e list -> 'f

accu is returned in the empty list case, so we can unify 'd and f.

('a -> 'b -> 'c) -> 'd -> 'e list -> 'd

accu is also passed as the first argument to f, so we can unify 'a and 'd.

('a -> 'b -> 'c) -> 'a -> 'e list -> 'a

The first element of l is passed as the second argument to f, so we can unify 'b and 'e.

('a -> 'b -> 'c) -> 'a -> 'b list -> 'a

And the result of (f accu a) is passed as the second argument to fold_left, so we can unify 'a and 'c.

('a -> 'b -> 'a) -> 'a -> 'b list -> 'a

This now perfectly matches the type of List.fold_left.

edited Feb 14 at 21:08

answered Feb 13 at 6:41

Chris

38.2k6 gold badges33 silver badges59 bronze badges

4 Comments

smwikipedia Feb 13 at 6:46

Thanks. But I was hammered with the fact that OCaml functions take only 1 argument. So I strived to stick to that.

Chris Feb 13 at 6:48

They do and they don't depending on whether you're working with theory or practicality. ('a -> 'b -> 'c) could be ('a -> ('b -> 'c)) if you like, but they're the same thing.

smwikipedia Feb 13 at 6:57

I feel the ('a -> ('b -> 'c)) is better at reflecting the functional aspect of OCaml. It explicitly shows that x takes something of type 'a and returns a function. And it is consistent with the right associativity convention of the logic connective imply.

smwikipedia Feb 20 at 1:47

Here's just one more piece of info. This is related to the so-called currying in functional programming. And this is the link about it.

Collectives™ on Stack Overflow

How to figure out the type of this function?

2 Answers 2

Comments

An example from the standard library

4 Comments

Your Answer

Hot Network Questions

Collectives™ on Stack Overflow

2 Answers 2

Comments

An example from the standard library

4 Comments

Your Answer

Sign up or log in

Post as a guest

Related