The Artima Developer Community
Sponsored Link

Weblogs Forum
The Importance of Recursive Types

9 replies on 1 page. Most recent reply: Oct 24, 2006 2:43 AM by Kannan Goundan

Welcome Guest
  Sign In

Go back to the topic listing  Back to Topic List Click to reply to this topic  Reply to this Topic Click to search messages in this forum  Search Forum Click for a threaded view of the topic  Threaded View   
Previous Topic   Next Topic
Flat View: This topic has 9 replies on 1 page
Christopher Diggins

Posts: 1215
Nickname: cdiggins
Registered: Feb, 2004

The Importance of Recursive Types (View in Weblogs)
Posted: Oct 14, 2006 3:46 PM
Reply to this message Reply
Summary
I've heard a lot about recursive types, but I never really paid attention until I found a weakness in the Cat type system which demanded one.
Advertisement
It has been a while since I released a version of Cat (if all goes well, there should be one released this weekend). This is due to some interesting challenges I ran into while testing the type inference engine. Inferring types is very easy for trivial functions, but when the functions take type variables, it quickly becomes very challenging to implement the type inference engine correctly. I had made a lot of progress over the last couple of week but my testing yielded a very simple program which I was unable to infer the type for:
  define f { dup eval }
The types of dup and eval are expressed as follows:
  dup : (A:any*) -> (A A);
  eval : (A (A:any*)->(B:any*)) -> (B);
The reverse of f is easy enough:
  define g { eval dup }
  g : (A (A:any*)->(B:any*)) -> (B B)
But the type of f requires a self-referential function. On the surface the type of f appears to be:
  f : ((A:any*) -> (B:any*)) -> (B)  
But there is an additional constraint, A must have the type:
  A : ((A:any*)->(B:any*))->(C:any*)
This still does not completely express the constraint because the requirement on A is recursive. The only solution I could come up with is:
  f : ((self)->(B:any*)) -> (B)
Unfortunately this is not yet supported by the Cat type system. I wonder if recursive types are an inevitable result of a non-trivial type system?


Howard Lovatt

Posts: 321
Nickname: hlovatt
Registered: Mar, 2003

Re: The Importance of Recursive Types Posted: Oct 15, 2006 5:03 AM
Reply to this message Reply
You can write your example in Java, but note types of eval, f, and g are not exactly the same as you propose.
package cat;
 
import static java.lang.System.*;
 
public class Main {
  static < A > T2< A, A > dup( final A a ) { return t( a, a ); }
  
  static < R, A > R eval( final A a, final F< ? extends R, ? super A > f ) { return f.call( a ); }
  
  static < R, A > T2< R, R > g( final A a, final F< R, ? super A > f ) { return dup( eval( a, f ) ); }
  
  static < A extends F< A, A > > A f( final A f ) {
    final T2< A, A > d = dup( f );
    return eval( d.e1, d.e2 );
  }
  
  public static void main( final String[] notUsed ) {
    out.println( g( 1, inc ) );
    out.println( f( id ) );
  }
  
  final static F< Integer, Integer > inc = new F< Integer, Integer >() {
    public Integer call( final Integer a ) { return a + 1; }
  };
 
  final static Id id = new Id() {
    public Id call( final Id a ) { return a; }
    public String toString() { return "id"; }
  };
 
  interface Id extends F< Id, Id > {};
  
  interface F< R, A > { R call( A a ); }
  
  static class T1< E1 > {
    E1 e1;
    T1( final E1 e1 ) { this.e1 = e1; }
    public String toString() { return "t(" + e1 + ")"; }
  }
  static < E1 > T1< E1 > t( final E1 e1 ) { return new T1< E1 >( e1 ); }
  
  static class T2< E1, E2 > extends T1< E1 > {
    E2 e2;
    T2( final E1 e1, final E2 e2 ) { 
      super( e1 );
      this.e2 = e2; 
    }
    public String toString() { return "t(" + e1 + ", " + e2 + ")"; }
  }
  static < E1, E2 > T2< E1, E2 > t( final E1 e1, final E2 e2 ) { return new T2< E1, E2 >( e1, e2 ); }
}

James Watson

Posts: 2024
Nickname: watson
Registered: Sep, 2005

Re: The Importance of Recursive Types Posted: Oct 17, 2006 2:40 PM
Reply to this message Reply
I don't quite get what you mean when you say:

"
<pre>
A : ((A:any*)->(B:any*))->(C:any*)
</pre>

This still does not completely express the constraint because the requirement on A is recursive. The only solution I could come up with is:
"

I would consider any type that is defined in terms of itself to be recursive based on the general definition of the term 'recursive'. It seems like you are talking about 'self-referential types' (I'd say self-types but that has a slightly different meaning in Scala, as I understand it.

For example, Java has recursive type defintions:
class Example<T extends Example<T>>


But does not have self-referential types. The distinction is that the following (B) is legal with recursive types and can only be disallowed with a true self-referential type.

class A extends Example<A>{}
 
class B extends Example<A>{}

Cleo Saulnier

Posts: 77
Nickname: vorlath
Registered: Dec, 2005

Re: The Importance of Recursive Types Posted: Oct 18, 2006 3:53 PM
Reply to this message Reply
f: ((A)->(A (A:any*)->(B:any*)))->(B)

Would you be ok to leaving it at that? Maybe reducing isn't the best option.

If you want to state the constraint of A, it's:

A: (A:any*)->(B:any*)

A function that takes itself as argument.

The following is what it comes down to... If you have duplication in the production_type_list as so:

X: (Y)->(Y Y) [2 or more Y's]

you risk that one of those Y's is going to be a consumption_type of the other Y if it/they is/are a function when used as parameters to another type.

Ex:
P: (Q Q->R)->R

If you use X as a parameter to P, then Q is both a function and an input to that same function caused by the duplication. So whenever a type is duplicated in the production_type_list [as in (Y)->(Y Y)], you have to check that they are all the same upon usage as a parameter to another type. If they are not the same, then you have to check if one of them is a function and if that same function takes a parameter that is the same as one of the duplicated types.

EX:
From using (Y Y) as parameters to (Q Q->R), we get two constraints.

Y: Q
Y: Q->R

These are not the same (note that Q should be expanded as well to find the final type). So we check if the arguments of the function (Q->R) are the same as any of the other types/constraints of Y. Here, we find that indeed Q is an argument of the function and also the type of the other Y. Now you must decide how to represent this. Either insert a recursive definition or don't reduce. If you choose recursion, you have to be careful when expanding the difinition of types (Q) when finding matches so that you don't get into an infinite recursive loop.

Choice:
func: ((Y)->(Y Y->R))->R [not reduced]
func: (@->R)->R [recursive]

Note: @ meaning the function type that contains it.

However, if the function (Q->R) did not contain an argument of the same type, then you can reduce to the function if the other type is 'any' (or a function that takes 'any' as arguments, etc. where overlaps are allowed), otherwise error.

Ex:
Y: S
Y: Q->R
S: any

Y can be 'any' (after S is reduced) or a function. 'any' can itself be a function, so no contradiction and we can reduce to just the function "Y: Q->R" and ditch the rest which is less specific anyhow. I believe your problem to be a case of trying to reduce N constraints to 1 and you end up with a loss of information. Maybe only reducing on 1 to 1 relations would be better, no?

Although my terminology may be off, is this what your problem is? Seems more like a representational problem than a strictly recursive one.

I've only looked at your type system today, so I may not understand it too well.

Cleo Saulnier

Posts: 77
Nickname: vorlath
Registered: Dec, 2005

Re: The Importance of Recursive Types Posted: Oct 18, 2006 4:10 PM
Reply to this message Reply
Sorry for the double post... I made a mistake. Scratch that first line. It should be an input A, not a function (which I wrote as being the same as dup) which is incorrect. I meant maybe a syntax that would allow a definition of the transformation.

f: (A: (A:any*)->(B:any*))->(B)

HAHA! Ok, you're right. It is recursive.
This looks right. Eval processes a function that takes itself as argument and produces the output type of that same function.

BTW, is the above allowed? Can you name the function type as you can other parameters? Maybe that's all you need. It would solve nesting problems too by allowing not just the next level up as 'self' implies.

R: (S: (T: (S)->(U))->(U))->U
or
R: (S: ((S)->(U))->(U))->U

This is recursive two levels out. With the ability to name function parameters, specifying it is no problem.

Christopher Diggins

Posts: 1215
Nickname: cdiggins
Registered: Feb, 2004

Re: The Importance of Recursive Types Posted: Oct 18, 2006 8:31 PM
Reply to this message Reply
> You can write your example in Java, but note types of
> eval, f, and g are not exactly the same as you propose.

Very interesting.

Christopher Diggins

Posts: 1215
Nickname: cdiggins
Registered: Feb, 2004

Re: The Importance of Recursive Types Posted: Oct 18, 2006 8:32 PM
Reply to this message Reply
> I don't quite get what you mean when you say:
>
> "
> <pre>
> A : ((A:any*)->(B:any*))->(C:any*)
> </pre>
>
> This still does not completely express the constraint
> because the requirement on A is recursive.

Yes. Sorry I wasn't being clear it was my intention to indicate that this was the failure of the current type system.

Christopher Diggins

Posts: 1215
Nickname: cdiggins
Registered: Feb, 2004

Re: The Importance of Recursive Types Posted: Oct 18, 2006 8:35 PM
Reply to this message Reply
> Sorry for the double post... I made a mistake. Scratch
> that first line. It should be an input A, not a function
> (which I wrote as being the same as dup) which is
> incorrect. I meant maybe a syntax that would allow a
> definition of the transformation.
>
> f: (A: (A:any*)->(B:any*))->(B)
>
> HAHA! Ok, you're right. It is recursive.
> This looks right. Eval processes a function that takes
> itself as argument and produces the output type of that
> same function.
>
> BTW, is the above allowed? Can you name the function type
> as you can other parameters?

That would be a good idea. I haven't yet allowed the naming of function types.

> Maybe that's all you need.
> It would solve nesting problems too by allowing not just
> t the next level up as 'self' implies.
>
> R: (S: (T: (S)->(U))->(U))->U
> or
> R: (S: ((S)->(U))->(U))->U
>
> This is recursive two levels out. With the ability to
> name function parameters, specifying it is no problem.

Agreed. Nice solution. It won't make it in the next version of Cat, but very possibly in a later version.

Howard Lovatt

Posts: 321
Nickname: hlovatt
Registered: Mar, 2003

Re: The Importance of Recursive Types Posted: Oct 18, 2006 11:31 PM
Reply to this message Reply
You could also take a look at Fortress, it has some nice syntax for generic types and also a novel and powerful generic type system.

http://research.sun.com/projects/plrg/

and this paper

http://research.sun.com/projects/plrg/2006-0137.pdf

Kannan Goundan

Posts: 18
Nickname: cakoose
Registered: Nov, 2005

Re: The Importance of Recursive Types Posted: Oct 24, 2006 2:43 AM
Reply to this message Reply
The simplest example is a singly-linked list node. In a language where types are named, you'd write something like:


type List = { Element: Int, Next: List }


But this definition isn't self contained. It relies on a external named reference (to the type "List"). An alternative method of defining the type:


mu(T) { Element: Int, Next: T }


This is a function that, given a type, will yield another type. The "mu" construct is like the "lambda" construct except for types instead of values. For recursive types, the convention is that you're passed in a single parameter, which is the type you're currently defining.

"Types and Programming Languages" has good introductory material on recursive types.

Flat View: This topic has 9 replies on 1 page
Topic: The Importance of Recursive Types Previous Topic   Next Topic Topic: Crippled By DRM & An 800-Pound Gorilla


Sponsored Links



Google
  Web Artima.com   

Copyright © 1996-2014 Artima, Inc. All Rights Reserved. - Privacy Policy - Terms of Use - Advertise with Us