Pal-Kristian Engstad <pal_engstad@naughtydog.com> writes:

> Honestly, I'd prefer to have to annotate non-exhaustive records:
>     let { foo = foo; bar = bar } = x
> should only match { foo; bar }, but
>     let { foo = foo; bar =  bar; .. } = x,
> can match records with more labels.
> PKE.
> Yaron Minsky wrote:

I would actually like to propose that to work on a type
level. Currently we have:

----------------------------------------------------------------------
# type base = { x : int }
  let get_x r = r.x
  type more = { x : int; y : int };;

type base = { x : int; }
val get_x : base -> int = <fun>
type more = { x : int; y : int; }

# get_x { x=1; y=2; };;
Error: This expression has type more but is here used with type base
----------------------------------------------------------------------

I propose that records can be subtyped if their prefix matches and
".." would be used to denote the subtype of any record with this prefix:

# type base = { x : int }
  let get_x r = r.x
  type more = { x : int; y : int };;

type base = { x : int; }
val get_x : base -> int = <fun>
type more = { x : int; y : int; }

# get_x ({ x=1; y=2; } :> base);;
- : int = 1


One could also declare get_x to accept supertypes:

# let get_x (r : { x : int; .. }) = r.x;
val get_x : { x : int; .. } -> int = <fun>

# get_x { x=1; y=2; };;
- : int = 1


I think there is only one thing that would need to be changed for the
compiled code with record subtypes like the above. Copying and
modifying a record would need allocate a block matching the size of
the input record and not the size of the subtype. Think about this
code:

# let change_x (r : { x : int; .. }) x = { r with x = x }
val change_x : { x : int; .. } as 'a -> int -> 'a = <fun>
# change_x { x=1; y=2; } 2;;
- : more = {x = 2; y = 2}

All other changes would only affect the grammar and type inference I think.



Now what would happen with your example?

# type record = { foo : int; bar : float; baz : string }
type record = { foo : int; bar : float; baz : string; }

# let f x = let { foo = foo; bar = bar; .. } = x in (foo, bar)

What type is that?

1) val f : { foo : int; bar : float; baz : string; .. } -> int * float = <fun>
2) val f : record -> int * float = <fun>
3) val f : { foo : int; bar : float; .. } -> int * float = <fun>
4) val f : { foo : 'a; bar : 'b; .. } -> 'a * 'b = <fun>

I would say it should result in 3. And the type should always be the
minimum prefix required to match all occuring fields:

# let f x = let { foo = foo; baz = baz; .. } = x in (foo, baz)
val f : { foo : int; bar : float; baz : string; .. } -> int * string = <fun>



As a further extention the following syntax would be usefull:

# type base = { x : int }
  type more = { base with y : int };;

type base = { x : int; }
type more = { x : int; y : int; }

With this syntax more would always be a supertype of base even if the
base type gets altered.


MfG
        Goswin