Weblogs Forum
The Importance of Recursive Types

9 replies on 1 page. Most recent reply: Oct 23, 2006 11:43 PM by Kannan Goundan

 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 12:46 PM
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.
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 2:03 AM
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 11:40 AM
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 12:53 PM
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 1:10 PM
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 5:31 PM
> 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 5:32 PM
> 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 5:35 PM
> 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 8:31 PM
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 23, 2006 11:43 PM
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
 Previous Topic Next Topic