RE: OCaml bug or feature?

RE: OCaml bug or feature?

[Manuel Fahndrich]

I think the problem you refer to is checking equivalence of parameterized
type definitions "Type Definitions With Parameters" Marvin Solomon 5th POPL.
The problem is equivalent to checking the equivalence of deterministic
pushdown automaton, which has since been shown decidable, although I know of
no practical algorithm.

Keep in mind though that the problem only arises in the presence of
non-regular types. Thus another approach is to simply disallow non-regular
types, which OCaml does for non-datatype definitions.

E.g. It is possible to define general regular parameterized recursive types
using polymorphic variants alone, ie., without explicit datatype
definitions.

type 'a list = [`Nil | `Cons of `a * 'a list ];

-Manuel


-----Original Message-----
From: Daniel C. Wang [mailto:danwang+news@cs.princeton.edu]
Sent: Thursday, November 30, 2000 11:37 AM
To: comp-lang-ml@uunet.uu.net
Subject: Re: OCaml bug or feature?



Henning Makholm <henning@makholm.net> writes:

> Scripsit "Daniel C. Wang" <danwang+news@cs.princeton.edu>
> 
> > The datatype constructors in both OCaml and SML are *type annotations*
they
> > just are unobtrusive and *mandatory* type annotations. Without the
explicit
> > constructor tags the type inference system would have no way to deal
> > properly with reucursive types. 
> 
> Do you have references to good explanations of what the exact
> problems you refer to are?

Nope... sorry.. this just my fuzzy understanding of how recursive types are
treated by type inference.. without the annotations, you have to guess how
many times you need to unfold/fold the recursive type for things to type
check.


> My experience (though not with full-sized
> ML-type languages) is that declaration-free recursive type inference
> is piece of cake once you have a circular unification algorithm.
> Sure, with polymorphism you get the same trouble with principal
> types as SML has with record types, but nothing more.

I was under the impression that the problem without the constructors made
the problem undecidable, but maybe I'm wrong...

> (Strangely enough it is not easy to find literature references
> to this. There was a paper on "Declaration-free type checking"
> by P.Mishra and U.Reddy in POPL'85, but that is much more
> complicated than necessary for mere declaration-free ML-style
> type inference because it includes union types and subtyping).

Have you tried citeseer?

http://www.neci.nj.nec.com/homepages/lawrence/citeseer.html

and doing a reverse citation lookup...