recursive types

recursive types

[nakata keiko]

Can I have recursive types going through both of "normal" types and
class types?

I would like to define something like

type exp = [`Num of obj |`Neg of obj] 
and class type obj = 
  object 
    method eql : exp ->  bool
  end

Thanks,
Keiko 

Re: [Caml-list] recursive types

[Damien Pous]

You can do something this:

type 'a exp_ = [`Num of 'a |`Neg of 'a] 

class type obj = object 
  method eql : obj exp_ ->  bool
end

type exp = obj exp_


Damien

Re: [Caml-list] recursive types

[skaller]

On Mon, 2004-12-13 at 20:58, Damien Pous wrote:
> You can do something this:
> 
> type 'a exp_ = [`Num of 'a |`Neg of 'a] 
> 
> class type obj = object 
>   method eql : obj exp_ ->  bool
> end
> 
> type exp = obj exp_

Or the converse (parameterise the class instead).

-- 
John Skaller, mailto:skaller@users.sf.net
voice: 061-2-9660-0850, 
snail: PO BOX 401 Glebe NSW 2037 Australia
Checkout the Felix programming language http://felix.sf.net

Recursive types

[Swaroop Sridhar]

How are arbitrary recursive types implemented in caml? Is it done using 
an explicit fix point combinator "type" so that the unifier itself does 
not go into an infinite loop?

I apologize if this topic has been previously discussed, and I would 
really appreciate if somebody can point me at the relevant postings.

Thanks,
Swaroop.

Re: [Caml-list] Recursive types

[Jacques Garrigue]

From: Swaroop Sridhar <swaroop@cs.jhu.edu>

> How are arbitrary recursive types implemented in caml? Is it done using 
> an explicit fix point combinator "type" so that the unifier itself does 
> not go into an infinite loop?

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.
A few years ago, infinite loops were a commonly reported bug :-)

Jacques Garrigue

Re: [Caml-list] Recursive types

[Keiko Nakata]

From: Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>

> From: Swaroop Sridhar <swaroop@cs.jhu.edu>
> 
> > How are arbitrary recursive types implemented in caml? 
> 
> 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.

I am very interested in this subject.
Since 1) I can define type abbreviations almost artitrary,
as in  type t = < m : t > ; and 2) type abbreviations can have parameters
as in type 'a t = < m : 'a > , 
just keeping a list/set of visited nodes does not seem to be enough,
especially for structual types.
So I think the type checker does some very clever thing.

Regards,
Keiko.

Re: [Caml-list] Recursive types

[Alain Frisch]

Keiko Nakata wrote:
> I am very interested in this subject.
> Since 1) I can define type abbreviations almost artitrary,
> as in  type t = < m : t > ; and 2) type abbreviations can have parameters
> as in type 'a t = < m : 'a > , 
> just keeping a list/set of visited nodes does not seem to be enough,
> especially for structual types.

Structural loops (those that don't cross a datatype) cannot be
arbitrary. The parameters cannot change:

# type 'a t = < m : 'a t >;;
type 'a t = < m : 'a t >
# type 'a t = < m : ('a * 'a) t>;;
In the definition of t, type ('a * 'a) t should be 'a t

The restriction ensures that structural recursive types are necessarily
regular. So standard coinductive algorithms (implemented by keeping
track of visited nodes or by memoization) are ok.

-- Alain

Re: [Caml-list] Recursive types

[Keiko Nakata]

From: Alain Frisch <Alain.Frisch@inria.fr>
> 
> The restriction ensures that structural recursive types are necessarily
> regular. So standard coinductive algorithms (implemented by keeping
> track of visited nodes or by memoization) are ok.

Thanks for the reply.

I think that it is not easy to know when to apply eta-expansion, 
namely, to replace a type name with its underlying definition.

For instance, to check equivalence betweeen the types t and s below:
 type t = < m : t * t >
 type 'a tuple = 'a * 'a
 type s = < m : s tuple >

the algorithm should memorize that t * t and s tuple are equivalent,
and then expands s tupl into s * s  
so as to check between t * t and s * s? 

When type abbreviations are more verobse as in 

 type 'a id = 'a 
 type 'a tuple = 'a id * 'a id 
 type u = < m : < m : u tuple> * < m : u tuple> > 

it seems difficult to know when to memorize in what representations
and when to eta-expand by the definitions.

I know easy standard coinductive algorithms found in textbooks,
but how to handle abbreviations is still unclear for me.

With best regards,
Keiko.

Re: [Caml-list] Recursive types

[Jacques Garrigue]

From: Keiko Nakata <keiko@kurims.kyoto-u.ac.jp>

> I think that it is not easy to know when to apply eta-expansion, 
> namely, to replace a type name with its underlying definition.
> 
> For instance, to check equivalence betweeen the types t and s below:
>  type t = < m : t * t >
>  type 'a tuple = 'a * 'a
>  type s = < m : s tuple >
> 
> the algorithm should memorize that t * t and s tuple are equivalent,
> and then expands s tupl into s * s  
> so as to check between t * t and s * s? 

No need to memorize equivalences: s tuple expands at its head to s * s.
The type checker guarantees that it is always safe to expand the head
of a type (i.e., definitions are well-founded.)
But you're right that abbreviations complicate the unification
algorithm a lot.
In order for unification to succeed above, t must expand to
(< m: 'a * 'a> as 'a), and s too. But to print nicely types we must
keep the abbreviations. This is done by memoizing expansions inside 
the abbreviations themselves. I.e., the expansion of t is actually:
  (< m : t[t='a] * t[t='a] > as 'a)
and that of s is
  (< m : s[s='b] tuple[s='b]> as 'b)
where [t='a] is an internal annotation to the abbreviation. So when
unifying, you can actually check the underlying type of an
abbreviation. But maintaining these abbreviations is rather
involved...
Fo instance abbreviations must be propagated:
  type u = <m : w> and w = u * u
will expand to
  (<m : w[u='a]> as 'a)
so that, if we expand w, we fall back to
  (<m : u[u='a] * u[u='a]>)

Jacques Garrigue

Re: [Caml-list] Recursive types

[Keiko Nakata]

From: Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>

> No need to memorize equivalences: s tuple expands at its head to s * s.
> The type checker guarantees that it is always safe to expand the head
> of a type (i.e., definitions are well-founded.)

Thanks for the reply.

> In order for unification to succeed above, t must expand to
> (< m: 'a * 'a> as 'a), and s too. But to print nicely types we must
> keep the abbreviations. This is done by memoizing expansions inside 
> the abbreviations themselves. 

This is a pretty nice feature of the type checker.
When programming with polymorphic variants,
the last part of typing error messages, 
which tells me incompatibilities of types using abbreviating names,
always helps me a lot.

With best regards,
Keiko 

Re: [Caml-list] Recursive types

[Swaroop Sridhar]

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.

Re: [Caml-list] Recursive types

[Jacques Garrigue]

From: Swaroop Sridhar <swaroop.sridhar@gmail.com>

> 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?

There is a problem with your algorithm:
the way you check the unf field is buggy (you dereference both sides),
but this seems a trivial a trivial error.
More importantly, even corrected it will fail when unifying a loop of
length 3 with a loop of length 2:
   t1 = (int * (int * 'a) as 'a)
   t2 = (int * (int * (int * 'b)) as 'b)
when you reach the inner 'b, you have already unrolled t1, so it also
has its unf field set, but not to t2...

The approach in ocaml is simpler: link at each type node, so that
already unified types will look equal. As a result, after unification
you have only a loop of length 1.

> > 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}

Note in this case: the definition of llist is nominal, so this type is
only iso-recursive, which is much easier to handle.
The difficulties only appears with
  type llist = < contents: int; link : llist >

Jacques Garrigue

Re: [Caml-list] Recursive types

[Swaroop Sridhar]

Jacques Garrigue wrote:
> There is a problem with your algorithm ... 
> The approach in ocaml is simpler: link at each type node, so that
> already unified types will look equal. 

Let me have another take at the algorithm :

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. 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

  	   t1.link = t2  (***** linked speculatively *****)

            for each i in 0 to t1.components.size()
               Unify (t1.components[i], t2.components[i])
               if Unification fails,
			t1.link = None
			unlink all types that were linked until now
			return false
	      endif

            for each i in 0 to t1.typeArgs.size()
               Unify (t1.typeArgs[i], t2.typeArgs[i])
               if Unification fails,
			unlink all types that were linked until now
			return false
	      endif

        return true

    case (_, _)  ->
            return false

4. Stop

Is this correct/ similar to what Ocaml does?

> Note in this case: the definition of llist is nominal, so this type is
> only iso-recursive, which is much easier to handle.

We might have syntactic restrictions (ex: one of ML's restriction that 
recursion can occur only across variant constructor boundaries, etc) so 
that arbitrary recursion is disallowed. However, from an implementation 
standpoint, I *think* that the above implementation of the unifier is 
easier to do even in the case of iso-recursive types. Is this true?

I thought of introducing explicit fold/unfold operations into the 
algorithm, but it seemed to do more work. If I am wrong, can you please 
suggest modifications to the above algorithm that works (better) only 
for iso-recursive types.

Thanks,
Swaroop.

Re: [Caml-list] Recursive types

[Swaroop Sridhar]

A (small) correction, I forgot to write the base case that will allow 
for termination:

> 
> Unify (first:TYPE, second: TYPE)
>    will return true on Unification false if not.
> 
> 1. Start
> 2. let t1 = repr first
>    let t2 = repr second

   2.5  if t1 equals t2
	   return true
> 
> 3. 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
> 
>         t1.link = t2  (***** linked speculatively *****)
> 
>            for each i in 0 to t1.components.size()
>               Unify (t1.components[i], t2.components[i])
>               if Unification fails,
>             t1.link = None
>             unlink all types that were linked until now
>             return false
>           endif
> 
>            for each i in 0 to t1.typeArgs.size()
>               Unify (t1.typeArgs[i], t2.typeArgs[i])
>               if Unification fails,
>             unlink all types that were linked until now
>             return false
>           endif
> 
>        return true
> 
>    case (_, _)  ->
>            return false
> 
> 4. Stop

Swaroop.

recursive types

[Jacques Le Normand]

[-- Attachment #1: Type: text/plain, Size: 595 bytes --]

hello again list
is it possible to have mutually recursive classes and types? I'm trying to
implement the zipper, and this is what I came up with:

class type node_wrapper =
object
  method identify : string
  method get_child_location : location
end

class virtual nodeable =
object(self)
  method virtual to_node_wrapper : node_wrapper
end

type path = (nodeable list * location * nodeable list) option
and location = Loc of nodeable * path


which, of course, doesn't type check


a simpler test case would be

class a =
  val b : c
end

type c = a

thanks for all the help so far!
--Jacques

[-- Attachment #2: Type: text/html, Size: 723 bytes --]

Re: [Caml-list] recursive types

[Erik de Castro Lopo]

Jacques Le Normand wrote:

> hello again list
> is it possible to have mutually recursive classes and types?

Yes and yes.

I haven't played much with classes at all, but recursive types
can be defined as :

  type x_t =
  {  x : int ; y : y_t ; }
  and
  y_t =
  { z : string }

For recursive classes I beleive that you do

   class xxx = ....

   and yyy =

to define mutually recursive classes xxx and yyy.

Erik
-- 
-----------------------------------------------------------------
Erik de Castro Lopo
-----------------------------------------------------------------
Think of XML as Lisp for COBOL programmers.
	-- Tony-A (some guy on /.)

Re: [Caml-list] recursive types

[Erik de Castro Lopo]

Jacques Le Normand wrote:

> hello again list
> is it possible to have mutually recursive classes and types?

Yes and yes.

I haven't played much with classes at all, but recursive types
can be defined as :

  type x_t =
  {  x : int ; y : y_t ; }
  and
  y_t =
  { z : string }

For recursive classes I beleive that you do

   class xxx = ....

   and yyy =

to define mutually recursive classes xxx and yyy.

Erik
-- 
-----------------------------------------------------------------
Erik de Castro Lopo
-----------------------------------------------------------------
Think of XML as Lisp for COBOL programmers.
	-- Tony-A (some guy on /.)
-- 
-----------------------------------------------------------------
Erik de Castro Lopo
-----------------------------------------------------------------
"Microsoft treats security vulnerabilities as public relations
problems."  -- Bruce Schneier

Re: [Caml-list] recursive types

[Jeremy Yallop]

Jacques Le Normand wrote:
> is it possible to have mutually recursive classes and types?

Yes, using recursive modules.  The syntax is a little heavy, though, 
since you have to write some of the definitions in both the signature 
and the implementation.

> class type node_wrapper =
> object
>   method identify : string
>   method get_child_location : location
> end
> 
> class virtual nodeable =
> object(self)
>   method virtual to_node_wrapper : node_wrapper
> end
> 
> type path = (nodeable list * location * nodeable list) option
> and location = Loc of nodeable * path

This might be written as

   module rec M :
   sig
     class type node_wrapper =
     object
       method identify : string
       method get_child_location : M.location
     end

     class virtual nodeable :
     object
       method virtual to_node_wrapper : node_wrapper
     end

     type path = (nodeable list * M.location * nodeable list) option
     type location = Loc of nodeable * path
   end =
   struct
     class type node_wrapper =
     object
       method identify : string
       method get_child_location : M.location
     end

     class virtual nodeable =
     object
       method virtual to_node_wrapper : node_wrapper
     end

     type path = (nodeable list * M.location * nodeable list) option
     type location = Loc of nodeable * path
   end

The definitions which merely define type aliases (node_wrapper and path) 
can be shortened in the implementation section if you prefer:

   module rec M :
   sig
      [elided]
   end =
   struct
     class type node_wrapper = M.node_wrapper

     class virtual nodeable =
     object
       method virtual to_node_wrapper : node_wrapper
     end

     type path = M.path
     type location = Loc of nodeable * path
   end

Jeremy.