Is this implementation of the Hindley-Milner algorithm correct?

Question

I based this implementation upon the implementation given in this answer and the book linked in it, but modified it to, instead of a constraint list and a substitution stack, generate a substitution tree in a single tree traversal operation.

Each node in the substitution tree is a VariableType. Child nodes are in the Types array. Types with no children represent just variable types, types with one child represent type that have been replaced with the child, and types with two children represent function types.

The Deepest method gets the current substitute given any type, since to replace, say, a with b, provided a is a leaf (has no children), you just set b to be the only child of a. This is what the ReplaceWith method does, which must take a leaf as the type to be replaced.

The Unify method must always get deepest terms (terms with zero or two children).

public interface ILambdaTerm { }

public interface IVariableTerm : ILambdaTerm
{
    string Name { get; }
}

public interface IAbstractionTerm : ILambdaTerm
{
    string ArgumentName { get; }
    ILambdaTerm Body { get; }
}

public interface IApplicationTerm : ILambdaTerm
{
    ILambdaTerm Function { get; }
    ILambdaTerm[] Parameters { get; }
}

public class VariableType
{
    public VariableType[] Types;

    public VariableType(VariableType argType, VariableType resType)
    {
        Types = new VariableType[] { argType, resType };
    }

    public VariableType() 
    {
        Types = new VariableType[0];
    }

    private bool Contains(VariableType type)
    {
        if (Types.Length == 0)
            return this == type;
        else
            return Types.Any(subType => subType.Contains(type));
    }

    public void ReplaceWith(VariableType type)
    {
        if (type.Contains(this))
            throw new Exception("Circular type.");
        Types = new VariableType[] { type };
    }

    public VariableType Deepest()
    {
        VariableType type = this;
        while (type.Types.Length == 1)
            type = type.Types[0];
        return type;
    }
}

public class TypeChecking
{
    private static void Unify(VariableType a, VariableType b)
    {
        if (a == b)
            return;

        if (a.Types.Length == 0)
            a.ReplaceWith(b);
        else
        {
            if (b.Types.Length == 0)
                b.ReplaceWith(a);
            else
            {
                Unify(a.Types[0].Deepest(), b.Types[0].Deepest());
                Unify(a.Types[1].Deepest(), b.Types[1].Deepest());
            }
        }
    }

    private static VariableType TypeOfTerm(ILambdaTerm term, IScope<VariableType> typeContext)
    {
        if (term is IVariableTerm)
        {
            var varTerm = (IVariableTerm)term;
            if (!typeContext.ContainsKey(varTerm.Name))
                throw new Exception(string.Format("Undeclared variable '{0}'.", varTerm.Name));
            return typeContext[varTerm.Name].Deepest();
        }
        if (term is IAbstractionTerm)
        {
            var absTerm = (IAbstractionTerm)term;
            var argType = new VariableType();
            var resType = TypeOfTerm(absTerm.Body, new InnerScope<VariableType>(typeContext, absTerm.ArgumentName, argType));
            return new VariableType(argType, resType);
        }
        if (term is IApplicationTerm)
        {
            var appTerm = (IApplicationTerm)term;
            var resType = new VariableType();
            var argType = TypeOfTerm(appTerm.Parameters[0], typeContext);
            var funType = TypeOfTerm(appTerm.Function, typeContext);
            Unify(funType, new VariableType(argType, resType));
            return resType.Deepest();
        }
        else
            throw new Exception(string.Format("Dunno what to do with a '{0}'.", term));
    }

    public static VariableType TypeOfTerm(ILambdaTerm term)
    {
        return TypeOfTerm(term, new GlobalScope<VariableType>());
    }
}

I also have an extension method which returns a type as a string, that uses a Dictionary<VariableType, string> to automatically assign a name to each type, considering only deepest types (types with zero or two children). I'm not to worried about this method so I skipped it to keep the post short.

I'm not too worried about performance as I'm about correctness of the code above.

Answer 1

I can't say much about the correctness but I have some comments about the design:

1. Whenever you write code like this:

   if (foo is SomeType)
   {
      // do something
   }
   else if (foo is SomeOtherType)
   {
      // do something else
   }
   ...
   

   then this is an indicator that your abstraction is flawed. I'm not saying you should never ever do it but more often than not it indicates a design problem.

2. Another point is the empty ILambdaTerm interface. An interface is like a contract - so what does an empty contract mean? Not much really.

3. Don't throw generic Exception. In your case an InvalidOperationException or maybe your own defined TermValidationException would probably make more sense. This would give the user at least some way of catching specific exceptions.

---

For the design here is what I would consider changing:

1. Move Unify into VariableType and make it public. Unify only operates on VariableTypes so it makes more sense to live on the VariableType class.

2. Types in VariableType can now become private as well which reduces unnecessary exposure of the internal data storage of the class.

3. Add a method VariableType GetVariableType(IScope<VariableType> typeContext) to the ILambdaTerm interface and move the implementation of the logic from the if (term is ...) blocks into the GetVariableType implementation in each of the concrete classes for the terms, e.g.:

   public interface VariableTerm : IVariableTerm 
   {
       public string Name { get; private set; }
   
       public VariableTerm(string name)
       {
           Name = name;
       }
   
       public override VariableType GetVariableType(IScope<VariableType> typeContext)
       {
           if (!typeContext.ContainsKey(Name))
               throw new Exception(string.Format("Undeclared variable '{0}'.", Name));
           return typeContext[Name].Deepest();
       }
   }
   

   Now you can get the VariableType of a term simply by writing:

   ILambdaTerm myTerm = ...
   ...
   
   var variableType = term.GetVariableType(new GlobalScope<VariableType>());
   

   and your TypeChecking class can disappear.