User-definable abstract types

[dhil]

This patch makes it possible to declare abstract types in Links, e.g.

typename MyAbstractType;
typename MyParameterisedAbstractType(a,b,c);

The primary motivation for adding them is to be able to give types to alien data objects.

The representation of user-definable abstract types is distinct from the built-in abstract types. In a future patch we ought to reconcile these two representations.

Another thing left for a future patch is the ability to control kinds. Currently, all abstract types have kind Type and the induced default subkind.

Resolves #1099.

[jamescheney]

I've had a very quick look and am uncertain why the payload type of Abstract is exn. It seems that the only way in which the type of x in Abstract(x) matters is that we use locally declared (generative) exceptions as a form of "gensym", and we use pointer equality to compare these in a couple of places. But these values are never raised or caught as far as I can see.

Is there a reason to make this specifically exceptions per se or would any other gensym-able abstract type also be OK? If so perhaps we could introduce a tiny interface for such types (providing gensym and equality) and make this easy to change later if something else is preferred.

[dhil]

You are right. I am piggybacking on the generativity of exn in OCaml to ensure that identities are globally unique. We can use any other generative type. The reason I didn't use a simple integer counter (as we do for other things) is that it doesn't scale beyond whole-program compilation; it also doesn't work very well if we at some point want to parallelise compilation.

I agree with your point, that it would be good to have a structured facility in the code base (e.g. in utils) for generating guaranteed globally unique identities, e.g.

module Gensym: sig
  type t
  val gensym : unit -> t (* generates a unique identity *)
  val to_string : t -> string (* string representation; used in codegen *)
  val eq : t -> t -> bool (* decides whether two identities are the same *)
end = struct
  type t = exn
  let gensym () = 
    let exception E in E
  let to_string exn = Printf.sprintf "%d" (Hashtbl.hash exn)
  let eq exn exn' = exn == exn'
end

Of course it may be beneficial to include an integer count too for generation of human readable names (would be helpful in codegen and error messages, e.g. to distinguish two distinct entities named Foo), but this can also be viewed as something orthogonal to the generative identity, e.g. something that should be handled by the Binder or Name modules.

[jamescheney]

Looks OK generally, a couple of minor things and one more substantial one:

• consistent use of Gensym.equal
• get rid of now unnecessary pp_exn
• I think piggybacking on alias to preserve type arguments to parameterized abstract types is going to be too fragile, and suggest basically making Abstract take Gensym.t plus a list of type parameter arguments.

[jamescheney]

This seems to assume only one layer of aliasing. I guess it is meant to dealwith the problem that if there are type parameters then the gensym.t generated once and for all for the abstract parameterized type will not know which parameters are applicable to any particular instance. However what about something like this:

typename MyParameterisedAbstractType(a,b,c);

typename MyAlias(a,b,c) = MyParameterisedAbstractType(a,b,c);

Now if I say pass something of type MyAlias(a,b,c) into something expecting MyParameterisedAbstractType(a,b,c) I think I will get a unification error, because we only look at the outer layer of aliasing.

I think it would be cleaner to make Abstract take Gensym.t and then a list of type arguments, and if the Gensyms are equal, unify recursively.

[dhil]

OK, I will have a look at this.

[jamescheney]

See comment on line 93, this part would hopefully go away if we associate type parameter arguments with Abstract directly rather than piggypacking on Alias.