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?

Talk Back!

Have an opinion? Readers have already posted 9 comments about this weblog entry. Why not add yours?

RSS Feed

If you'd like to be notified whenever Christopher Diggins adds a new entry to his weblog, subscribe to his RSS feed.

Digg | del.icio.us | Reddit

About the Blogger

Christopher Diggins is a software developer and freelance writer. Christopher loves programming, but is eternally frustrated by the shortcomings of modern programming languages. As would any reasonable person in his shoes, he decided to quit his day job to write his own ( www.heron-language.com ). Christopher is the co-author of the C++ Cookbook from O'Reilly. Christopher can be reached through his home page at www.cdiggins.com.