CODEWITHSUNDEEP
f#type-inferenceunification
Andri
Andri

Reputation: 1

Unification of types

I am doing this exercise on unifications of types and I am having a hard time understanding if it works. This exercise is specifically being done with f# in mind.

To my understanding my goal is to change the variables of the two types so that the become the same. If that is not possible, the types cannot be unified. Also, to my understanding, I am allowed to change all of the types that are like 'a, 'b, 'c, etc.

This is the first two exercises:

For each of the following pairs of types, say whether they can be unified or not. If they can be unified, list the substitutions for type variables that need to be made to achieve this. You are not allowed to rename apart the occurrences of type variables. Be careful not to create infinite types (for example, ’a and ’a option cannot be unified).

(a) int -> ((’a -> ’b) option) and int -> ’c -> (’d option) (b) int -> int option and 'a -> 'b

My answers are the following:

(a) Can be unified since I can substitute 'a as 'c and 'b as 'd (unsure because of the brackets?) (b) Can be unified since I get substitute 'a with int and 'b with int option: int -> int option

Am I on the right path?

Upvotes: 0

Views: 163

Answers (1)

Tomas Petricek
Tomas Petricek

Reputation: 243106

Given that this is an exercise, I'm not going to give the full answer. There is already a very useful comment that clarifies one issue. In general, the best thing to do is to first figure out what the notations mean. You should also keep in mind that F# functions with multiple arguments can be seen as functions returning other functions, i.e., a -> b -> c is the same as a -> (b -> c).

You can then think of the type as a tree where the nodes are the kinds of type (function, option, primitive type, type variable). So for example, int -> (('a -> 'b) option) would be:

    ->
  /    \ 
int  option
       |
       ->
     /    \
    'a    'b

And int -> 'c -> ('d option), which is the same as int -> ('c -> ('d option)) would be:

    ->
  /    \
int    ->
     /    \
    'c   option
           |
          'd

If you can match the two trees so that the node types match (a function in the left corresponds to a function in the right, primitive types are the same, etc.), then you can unify the types - type variables can be matched with anything (and that gives you the assignment, though you still need to avoid recursive/infinite matching!)

Upvotes: 1

Related Questions