CODEWITHSUNDEEP
typesfunctional-programmingocaml
Brandon
Brandon

Reputation: 1605

What is the general way to determine the type of an OCaml expression?

I am a beginner in OCaml and functional programming in general. If I have an expression, how do I determine its type, other than by just entering it into the top level and compiling it?

For example, if I have

fun x -> fun (y, z) -> (x y) (z () )

How do I even go about determining the type of this expression? Does it involve any cleverness, or is there a simple algorithm I can follow that will help me think about how to determine the type of any expression?

Upvotes: 2

Views: 460

Answers (2)

Marcin Łoś
Marcin Łoś

Reputation: 3246

No cleverness needed. There is, indeed, an algorithm to determine the types. Ocaml is based on Hindley-Milner type system. There are few type inference algorithms, you can find the details in the article. As for your example, let's try figuring it out piece by piece:

fun x -> fun (y, z) -> (x y) (z () )

  • whole expression is a function, from some type A = typeof(x) to type of B = typeof(fun(y, z) -> (x y) (z ())).

  • z is of type () -> D, since it is called with () and passed to x

  • so, the type of z () is D

  • hence the type of (x y) is (D -> E)

  • let C be the type of y

  • type of x is therefore C -> (D -> E)

  • and the type of (x y) (z ()) is just E

  • knowing types of x, y and the last expression, we conclude that the whole expression has the type (C -> D -> E) -> C * (() -> D) -> E

Upvotes: 8

Pascal Cuoq
Pascal Cuoq

Reputation: 80255

The words to search for are “Hindley-Milner type system”. You should find plenty of resources on the web, just steer clear of research articles which may be arbitrarily complex extensions of the basic system.

There is an algorithm and a type system. The type system is not syntax-directed: at any step a choice must be made to either follow the syntax or instanciate/generalize.

The “algorithm” is syntax-directed (only one rule applies at any step), which is why it is called “algorithm”. That makes it very efficient although it is still presented as a set of inference rules. It can be made more efficient yet by using mutable references for unification.

Upvotes: 3

Related Questions