Re: [Caml-list] Recursive types

[Swaroop Sridhar <swaroop.sridhar@gmail.com>]

Jacques Garrigue wrote:
> No, types are just implemented as (cyclic) graphs.
> All functions in the type checker have to be careful about not going
> into infinite loops. There are various techniques for that, either
> keeping a list/set of visited nodes, or using some mutable fields.

Thanks for the clarification. In order to ensure that I understand you 
correctly, can you please look into the following unification algorithm 
and see if it is reasonably correct?

Considering a language with integers, records and type variables.
Let record types be unified by structural unification.

My representation of type is (please forgive my sloppy syntax at times):

type KindUnion = Integer | Tvar | Record
type 'a option = None | Some 'a

type TYPE =
  { id: int;
         (* unique ID *)

    kind: kindUnion;
         (* type of this type: integer/ tvar/ record *)

    components: mutable vector of TYPE
         (* vector of types containing legs of a record *)

    typeArgs: mutable vector of TYPE
         (* vector of types containing type-arguments / type-parameters
            of a record *)
         (* example
               type ('a, 'b) rec = { a: 'a->'b; b: int}
                     typeArgs          components
         *)

    link: mutable (TYPE option)
         (* to link unified types *)

    unf: mutable (TYPE option)
         (* This is a marker used by the unifier.
            Initially, this field is set to `None' for all types.
            If we are attempting to unify t1 and t2, the unifier
            will mark t1-> unf = Some t2, and t2-> unf = Some t1
            so that we detect them next time when we recurse *)
}

I also assume that a function repr is defined that will traverse the 
links so that (repr t) will provide the "final" type.

So, now the Unifier algorithm can be written as (in some hypothetical 
algorithmic language):

Unify (first:TYPE, second: TYPE)
    will return true on Unification false if not.

1. Start
2. let t1 = repr first
    let t2 = repr second

3.  (* The unifier will set unf field on the way in and will
        clear it on its way out. So, first test if we have a
        recursive case *)

    if(t1.unf != None and t2.unf != None)
        if(t1.unf == t2.unf)
	  return true
        endif
        if(t2.unf == t1.unf)
           return true
        else
           return false
        endif
    endif


4. (* set the unf fields *)
    if(t1.unf == None and t2.unf != None)
        t1.unf := Some t2
    else
      if(t2.unf == None and t1.unf != None)
        t2.unf := Some t1
      else
        t1.unf = Some t2
        t2.unf = Some t1
      endif
    endif

5. match (t1.kind, t2.kind) with

    case (Integer, Integer) ->
            return true

    case (Tvar, _ )  ->
            t1->link = Some t2
            return true

    case (_, Tvar) ->
            t2->link = Some t1
            return true

    case (Record, Record) ->
            if the record lengths don't match
               return false

            for each i in 0 to t1.components.size()
               Unify (t1.components[i], t2.components[i])
               if Unification fails, return false

            for each i in 0 to t1.typeArgs.size()
               Unify (t1.typeArgs[i], t2.typeArgs[i])
               if Unification fails, return false
	   return true

    case (_, _)  ->
            return false

6. t1.unf = None
    t2.unf= None

7. Stop

Is this algorithm correct? If not, how should it be fixed?

> A few years ago, infinite loops were a commonly reported bug :-)

I read a couple of postings about this issue. I understand that one can 
hurt oneself with a type being parameterized itself. I also read that 
the type system needs to deal with this in order to support objects. 
Aren't recursive types necessary even to do a simple linked list like:

type llist = {contents: int; link : mutable llist}

Thanks again,
Swaroop.