As-binding #-types

As-binding #-types

[Frank Christoph]

  The manual says you can use "as" to bind row variables in a type, so
"#myclass as 'a -> 'a" would be the type of a function to and from equal
types, instead of possibly different descendants of "#myclass".

  But I've had trouble using this type expression in type definitions.

  #type 'a mytype = Mk of #myclass;;
  Unbound row variable in #myclass

is an error as expected, but

  #type 'a mytype = Mk of #myclass as 'a;;
  Unbound row variable in #myclass

yields the same problem.  Shouldn't this be possible?

------------------------------------------------------------------------
Frank Christoph                 Next Solution Co.      Tel: 0424-98-1811
christo@nextsolution.co.jp                             Fax: 0424-98-1500

Re: As-binding #-types

[Jerome Vouillon]

>   #type 'a mytype = Mk of #myclass as 'a;;
>   Unbound row variable in #myclass

In a type definition, type parameters *must* be free variables. But, here,
you try to bind the type parameter 'a to #myclass. So, this definition
fails. Actually, the compiler sees that #myclass contains a row variable
that obviously cannot be a type parameter, and hence rejects this phrase.

You can remove the constraint and just write
    #type 'a mytype = Mk of 'a;;
I don't think omitting the type constraint is a problem in practice.

However, I plan to add constrained type definitions to the language in the
future. Then you will probably be able to write your type definition as
    #type (#myclass as 'a) mytype = Mk of 'a;;

        Jerome

Re: As-binding #-types/Evaluation order & State

[Frank Christoph]

  In the last message, I wrote:

>   The manual says you can use "as" to bind row variables in a type, so
> "#myclass as 'a -> 'a" would be the type of a function to and from equal
> types, instead of possibly different descendants of "#myclass".

>   But I've had trouble using this type expression in type definitions.

>   #type 'a mytype = Mk of #myclass;;
>   Unbound row variable in #myclass

> is an error as expected, but

>   #type 'a mytype = Mk of #myclass as 'a;;
>   Unbound row variable in #myclass

> yields the same problem.  Shouldn't this be possible?

but I think I misunderstood the difference between "#myclass" and simply
"myclass".  I wasn't expecting to be able to use the methods of an arbitrary
descendant of myclass after pattern matching mytype, I just wanted to
constrain the polymorphic variable 'a -- so I suppose the correct declaration
would be

  #type 'a mytype = Mk of myclass;;

and use coercion on descendants I want to instantiate it with.

  In fact, I have a completely different question, though, and I expect most
people will probably be familiar with it.  Quite often I have come across
problems because of the interaction of evaluation order and state updates.
The most recent example I encountered was with writing a function that
converts a Queue.t to a list.

  #let rec list_of_queue q =
  #  try Queue.take q :: list_of_queue q with Queue.Empty -> []

Clearly this function will not terminate because the right argument of "::"
gets evaluated first.  So either we need to sequence the evaluation of the two
sides or pass a different argument to the recursive call of list_of_queue.
But if we use ";", then the result of the first computation is discarded, so
the only way I see to do it explicitly is something like,

  #let rec list_of_queue q =
  #  let e = ref None in
  #  try e := Some (Queue.take q);
  #      (match !e with Some x -> x) :: list_of_queue q
  #  with Queue.Empty -> []

where the option type is necessary since there is no other reasonable
initialization value for the reference.

  Of course, there is a much simpler way,

  #let rec list_of_queue q =
  #  let cons tl hd = hd :: tl in
  #  try cons (list_of_queue q) (Queue.take q)
  #  with Queue.Empty -> []

but this also seems pretty contrived.  Furthermore, in those cases where we
CAN implicitly rely on the evaluation order to do the updates in the proper
order, we're setting ourselves up for disaster if the function gets modified
later on by some unsuspecting soul.

  So, how do most people usually handle this problem?  Is there a
straightforward, safe, efficient solution?

------------------------------------------------------------------------
Frank Christoph                 Next Solution Co.      Tel: 0424-98-1811
christo@nextsolution.co.jp                             Fax: 0424-98-1500

Re: As-binding #-types/Evaluation order & State

[Francois Rouaix]

Dear Frank,

about the evaluation order question:

> [this is bogus because of right-to-left order]
>  #let rec list_of_queue q =
>  #  try Queue.take q :: list_of_queue q with Queue.Empty -> []

I would have written

let rec list_of_queue q =
  try
    let h = Queue.take q in 
       h::list_of_queue q
  with
    Queue.Empty -> []

in this case, which seems pretty natural.

In general, if I have a doubt about consequences of evaluation order on the
state, say for:
   ef e1 e2 en

I'd write (assuming I want left-to-right order of course)
   let f = ef  in
   let x1 = e1 in
   ...
   let xn = en in
     ef x1 ... xn

Or did I miss something ?


-- 
Francois.Rouaix@inria.fr                   Projet Cristal - INRIA Rocquencourt
Programming is dreadfully impermanent;  it's more like performance art
than literature -- Bruce Sterling (dixit Wired)