[bitc-dev] BitC Records

[Swaroop Sridhar]

On Fri, 24 Dec 2004, Jonathan S. Shapiro wrote:

> I do not understand the question. Can you give an example?
>
>
> shap
>

Consider the following definition:
let q = function x -> function y -> (x:= y::(!x))
The type of this function is q: 'a list ref -> 'a -> unit

Now,
let p = ref [];;
*IF* the type of p is 'b list ref  (which implicitly means FOR ALL 'b),

then, if
let r = q p,
the type of r will be 'b -> unit, FOR ALL 'b.

Which means,
r 1 ; r true;;
will have to type-check.

This will clearly make the type-system unsound, because, the list p will
now be
val p = 'b list ref {contents = [true; 1]} !

The way ocaml handles this is to give p a monomorphic type '_b, rather
than 'b.
Now,
# let q = function x-> function y-> (x:=y::(!x));;
val q : 'a list ref -> 'a -> unit = <fun>
# let p = ref [];;
val p : '_a list ref = {contents = []}
# let r = q p;;
val r : '_a -> unit = <fun>
# r 1;;                (* At this point, the type of p is changed from '_a
list to int list *)
- : unit = ()
# p;;
- : int list ref = {contents = [1]}
# r true;;
This expression has type bool but is here used with type int

The way SML handles this is by imposing value restrictions. SML does not
give non syntactic values a
polymorphic type, but gives them a dummy (and useless) type like ?.X1
- val p = ref [];
stdIn:17.1-17.15 Warning: type vars not generalized because of
   value restriction are instantiated to dummy types (X1,X2,...)
val p = ref [] : ?.X1 list ref
- 1::p;
stdIn:18.1-18.5 Error: operator and operand don't agree [tycon mismatch]
  operator domain: int * int list
  operand:         int * ?.X1 list ref
  in expression:
    1 :: p

For more information, please refer
http://www.smlnj.org/doc/Conversion/types.html.

Swaroop.



> On Thu, 2004-12-23 at 19:40 -0500, Swaroop Sridhar wrote:
> > I have an important question. Because BitC is stateful, how do we want
> > to handle polymorphism over non-syntactic types in our language?
> >
> > Do we want to impose the value-restriction as in SML? or do we want to
> > do monomorphism ('_a) and single instantiation as in OCaml?
> >
> > I am very nervous about going down the second path, given that we do not
> > have any module-level scoping and we do not guarantee order of
> > compilation when we compile multiple files (i.e., we do not have any
> > "use ...").
> >
> > Swaroop.
> > _______________________________________________
> > bitc-dev mailing list
> > bitc-dev at coyotos.org
> > http://www.coyotos.org/mailman/listinfo/bitc-dev
> --
> Jonathan S. Shapiro <shap at eros-os.org>
>
> _______________________________________________
> bitc-dev mailing list
> bitc-dev at coyotos.org
> http://www.coyotos.org/mailman/listinfo/bitc-dev
>