[MLton-devel] phantom types and directed graphs

[Stephen Weeks]

One problem with the approach I sent earlier is that requires the user
of the Graph module to define the new types and impose the
constraints.  That makes user code messier.  Another approach is to
force the type changes in the graph transform, as follows.

------------------------------------------------------------
signature DIRECTED_GRAPH_PHANTOM = 
   sig
      structure Node: 
	 sig
	    type 'a t
	 end
      
      type 'a t
      type 'a u (* unary notation for number of transforms *)

      val new: unit -> unit t
      val newNode: 'a t -> 'a Node.t
      val nodes: 'a t -> 'a Node.t list
      val transpose: 'a t -> 'a u t * {destroy: unit -> unit,
				       newNode: 'a Node.t -> 'a u Node.t}
   end
------------------------------------------------------------

I prefer this approach even though it has the drawback of confusing
graphs that have been through the same number of transformations.  It
would be possible to combine the approaches and use type ('a, 'b) t,
but that seems too messy to me.

I was a bit worried that all this polymorphism would cause MLton to
duplicate the graph code for every phantom type, but I now see that it
is possible to avoid that.  Here is a signature for non-phantom
graphs, as we have now, along with a functor that transforms them to
phantom graphs.  This shows that everything is happening at the type
level, on top of a monomorphic implementation.

------------------------------------------------------------
signature DIRECTED_GRAPH = 
   sig
      structure Node: 
	 sig
	    type t
	 end
      
      type t

      val new: unit -> t
      val newNode: t -> Node.t
      val nodes: t -> Node.t list
      val transpose: t -> t * {destroy: unit -> unit,
			       newNode: Node.t -> Node.t}
   end

functor Phantom (G: DIRECTED_GRAPH): DIRECTED_GRAPH_PHANTOM =
   struct
      open G
      structure Node =
	 struct
	    open Node
	    type 'a t = t
	 end
      
      type 'a t = t
      type 'a u = unit
   end
------------------------------------------------------------

Unfortunately, the above functor fails to type check in SML/NJ due to
an SML/NJ bug (#1548, which I reported on Feb 9, 2000!).  It does type
check with the other SML implementations.

Fortunately, directly instantiating the functor, as I will do for our
graphs, does type check under SML/NJ.

In trying to understand the SML/NJ bug, I noticed that the following
fails.

------------------------------------------------------------
functor F (S: sig
		 type t
		 val x: t
	      end):
   sig
      type 'a u
      val x: 'a u
   end =
   struct
      open S
      type 'a u = t
   end
------------------------------------------------------------

while the following, directly instantiating F, works

------------------------------------------------------------
structure S =
   struct
      type t = unit
      val x: t = ()
   end

structure F: 
   sig
      type 'a u
      val x: 'a u
   end =
   struct
      open S
      type 'a u = t
   end
------------------------------------------------------------

but the following, adding a signature constraint on S, fails

------------------------------------------------------------
structure S:
   sig
      type t
      val x: t
   end =
   struct
      type t = unit
      val x: t = ()
   end

structure F: 
   sig
      type 'a u
      val x: 'a u
   end =
   struct
      open S
      type 'a u = t
   end
------------------------------------------------------------

Go figure.


-------------------------------------------------------
This SF.NET email is sponsored by:
SourceForge Enterprise Edition + IBM + LinuxWorld = Something 2 See!
http://www.vasoftware.com
_______________________________________________
MLton-devel mailing list
MLton-devel@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/mlton-devel