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.