Dream Coder - Algorithm 2

Type Unification and the sample' Function

The core of the sample' function involves generating a program whose type unifies with a desired type $\tau$. The unification process ensures that the program generated has the correct type or can be transformed into one that matches $\tau$.

Understanding Type Unification:

Type unification is the process of making two types compatible by finding a substitution (if needed) such that both types become equal. Specifically:

Case 1: $\tau$ is a function type $\alpha \to \beta$

• Here, we are expected to generate a lambda function of the form:$$\lambda (\text{var})\text{body}$$
• The variable $\text{var}$ is mapped to type $\alpha$.
• The recursive step is then to generate a program body whose type unifies with $\beta$.
  • This is done by calling sample' recursively to generate a program whose type unifies with $\beta$.

Case 2: $\tau$ is not a function type (i.e., a concrete type)

• In this case, the program must have a type ${\tau }^{\prime }$ that unifies with $\tau$.
• The goal is to find a program that has type ${\tau }^{\prime }$ such that ${\tau }^{\prime }$ unifies with $\tau$.

Generating a Program Based on $\tau$

The algorithm proceeds by generating a program from the library $D$ and the environment $\mathcal{E}$, ensuring that the generated program's type matches $\tau$.

1. Picking a Set of Primitives:

   • We first pick a set of primitives (programs $\rho$) from the library $D$ and the environment $\mathcal{E}$.
   • These primitives must have a type ${\tau }^{\prime }$ such that:
     • If ${\tau }^{\prime }$ is a lambda function $\alpha \to \beta$, then $\beta$ must unify with $\tau$.
     • Otherwise, ${\tau }^{\prime }$ must unify (be equal to) $\tau$.

2. Handling Variables:

   • Next, we need to consider variables. These are programs that exist in the environment $\mathcal{E}$.
   • We draw a program $e$ with probability proportional to the weight assigned to $e$ by $\theta$ if $e\in D$.
   • If $e\notin D$, we instead use ${\theta }_{\text{var}}$, which is the $|D|+1$-th component of $\theta$, and we draw $e$ with probability proportional to $\frac{{\theta }_{\text{var}}}{|\text{variables}|}$.

3. Type Checking:

   • Notice that the drawn program $e$ has type ${\tau }^{\prime }$.
   • We check if ${\tau }^{\prime }$ unifies with $\tau$.

4. Handling Lambda Functions:

   • If ${\tau }^{\prime }$ is a lambda function, we retrieve its argument types using $\text{args}$ (this is done in line 24).
   • We then sample all the arguments required to apply $e$ (steps 18 to 20).
   • Finally, we return $e$ with all its arguments bundled into one tuple.