Width subtyping

Width subtyping

[Dario Teixeira]

Hi,

Though it is probably been-there-done-that material for the veterans in this list,
for the sake of the not-so-veterans I have to ask: how do you guys typically model
width subtyping in Ocaml?   Consider for example three record types that share some
of their fields:

type t1 = {a: int; b: int; c: int;        }
type t2 = {a: int; b: int; c: int; d: int;}
type t3 = {        b: int; c: int; d: int;}

In some circumstances, the object system can be put to good use for this kind of problem.
Not always though, so I'm curious about other approaches people use.  One approach
I've considered is to create a superset record where each field is an optional type,
and then creating constructors/getters for each valid subset.  Unfortunately this
solution feels a bit kludgy, even if it reduces code duplication.  For safety reasons
I'm therefore currently just declaring each record type independently (concerns about
duplication be damned).

In other words, polymorphic variants provide a very elegant solution for subtyping
with sum types.  Is there some brilliant idea that could do the same for product types?

Best regards,
Dario Teixeira

Re: [Caml-list] Width subtyping

[Jacques Carette]

Dario Teixeira wrote:
> In other words, polymorphic variants provide a very elegant solution for subtyping
> with sum types.  Is there some brilliant idea that could do the same for product types?
>   
The dual of sums is products.  Open (labelled) sums are "polymorphic 
variants".  Their duals are open (labelled) products are "rows" (which 
O'Caml already supports, through its objects).

See TAPL for a nice introduction to the type theory of labelled records 
with subtyping (i.e. rows).

Jacques

PS: note that O'Caml's products are positional while its sums are 
labelled, so the duality present in the theory isn't as clear there.  
The better dual for O'Caml's sums is really records.

RE: [Caml-list] Width subtyping

[David Allsopp]

> Though it is probably been-there-done-that material for the veterans in
> this list, for the sake of the not-so-veterans I have to ask: how do you guys
> typically model width subtyping in Ocaml?

Definitely not a veteran, but might private types help a little?

> Consider for example three record types that share some of their fields:
> 
> type t1 = {a: int; b: int; c: int;        }
> type t2 = {a: int; b: int; c: int; d: int;}
> type t3 = {        b: int; c: int; d: int;}

Modelled as...

module M : sig
  type t' = {a: int; b: int; c: int; d: int}
  type t = private T1 of t' | T2 of t' | T3 of t'
  val makeT1 : int -> int -> int -> t
  val makeT2 : int -> int -> int -> int -> t
  val makeT3 : int -> int -> int -> t
end = struct
  type t' = {a: int; b: int; c: int; d: int}

  type t = T1 of t' | T2 of t' | T3 of t'

  let makeT1 a b c = T1 {a = a; b = b; c = c; d = 0}
  let makeT2 a b c d = T2 {a = a; b = b; c = c; d = d}
  let makeT3 b c d = T3 {a = 0; b = b; c = c; d = d}
end

This way you're always dealing with the same product type, but the sum type tells you which fields are actually valid. Of course, it relies on there being an obvious sentinel value for unused fields (otherwise you just end up with 'a option everywhere) and I still don't think it's that neat as you can still match against fields which aren't valid but at least the type system prevents you from being handed an illegal value. The benefit is that you don't need special "get" functions (just a match on type t to extract the t' value from each constructor). I can't get my head around how private polymorphic variants work to see if they can refine this further...


David

Re: [Caml-list] Width subtyping

[Richard Jones]

On Fri, May 29, 2009 at 07:10:12AM -0700, Dario Teixeira wrote:
> type t1 = {a: int; b: int; c: int;        }
> type t2 = {a: int; b: int; c: int; d: int;}
> type t3 = {        b: int; c: int; d: int;}

I've very tired at the moment, but I think that Garrigue's
polymap syntax extension does what you want:

http://www.math.nagoya-u.ac.jp/~garrigue/code/ocaml.html

If not, just ignore me!

Rich.

-- 
Richard Jones
Red Hat