[bitc-dev] BitC Records

[Jonathan S. Shapiro]

On Thu, 2004-12-23 at 19:53 -0500, Swaroop Sridhar wrote:
> In the presence of Record Polymorphism, What is the type of x in
> 
> fun x => If  (f ()) then x.a else x.b  ?
> 
> It should actually be:
> 
> [_={a:_} or _={b:_}]
> 
> Do we handle this case, or do we make the conservative assumption that x 
> should be of type _={a:_, b:_}?

PLEASE let's stop writing ML syntax to describe BitC questions. It will
lead us badly astray!

I believe you mean:

(lambda (x) (if (f) x.a x.b))

The correct question, I think, is what is the type of 'x'. In BitC, the
two legs of an 'if' are required to return the same type. Thus, the type
of the fields 'a' and 'b' must be the same. Therefore (if I may invent a
syntax) the type of the lambda must be:

  [{..., a:'a, ..., b:'a, ...} or
   {..., b:'a, ..., a:'a, ...}] => 'a

where '...' means any number (including zero) of fields.

Note, however, that ML explicitly does NOT do polymorphism for 'fn'
forms!

> Again, field-order should not be specified. So we may want to modify out 
> tree of types in the following way (if at all it is feasible):
> 
> 	.
> 	.
> 	.
>       _={* a:_, b:_} // * means that the record
>   	|		has fields a and b in no
> 	|		particular order
> 	|
>      -------------------
>      |	               |
> _={a:_, b:_}        _={b:_ , a:_}   // Combinations of
> 					ordered fields
> 					will be subtypes

I really hope that this isn't necessary.

> So, the above function will have the type _={* a:_, b:_}.

I think that it should be viewed as a union type, rather than as an
underspecified type.


shap
-- 
Jonathan S. Shapiro <shap at eros-os.org>