Structural subtyping problem

Structural subtyping problem

[Dario Teixeira]

Hi,

I'm using the structural subtyping aspects of Ocaml's object system to emulate width
subtyping.  I've come across a problem which does not type-check, though intuitively
it seems correct.  I reckon that the compiler may need some help in the form of type
annotations and/or coercions, though their exact shape elludes me.

A simple nonsensical example that illustrates the problem is listed below; the
type-checking error occurs in function "step1", where the optional parameter "story"
is used as an object of type "< title:string; .. >".  In function "step3", this
parameter "story" is actually instantiated with objects of type "< title:string >"
and "< title:string; count:int >".

Anyway, am I correct in assuming this should be feasible?  And if so, what coercions
are required to make this compile?

Thanks in advance!
Best regards,
Dario Teixeira

=============================================================================

let rec step1 ?story () = match story with
	| Some s -> step2 s#title
	| None   -> step2 "title1"


and step2 title =
	let story =
		object
			method title = title
			method count = 0
		end
	in step3 ~story


and step3 ~story = match story#count with
	| 0 ->
		step1 ~story ()
	| 1 ->
		let story =
			object
				method title = "title2"
			end
		in step1 ~story ()
	| _ ->
		true

=============================================================================

Re: [Caml-list] Structural subtyping problem

[Vincent Aravantinos]

[-- Attachment #1: Type: text/plain, Size: 752 bytes --]

Hi, the following seems to do the trick  (?) :

Le 28 mars 10 à 18:38, Dario Teixeira a écrit :

> let rec step1 ?story () = match story with
> 	| Some s -> step2 s#title
> 	| None   -> step2 "title1"
>
>
> and step2 title =
> 	let story =
> 		object
> 			method title = title
> 			method count = 0
> 		end
> 	in step3 ~story
>
>
> and step3 ~story = match story#count with
> 	| 0 ->
>>
-		step1 ~story ()
+               step1 ~story:(story :> <title : string>) ()
> 	| 1 ->
> 		let story =
> 			object
> 				method title = "title2"
> 			end
> 		in step1 ~story ()
> 	| _ ->
> 		true

Cheers,
--
Vincent Aravantinos - PhD Student - Laboratory of Informatics of  
Grenoble
http://membres-lig.imag.fr/aravantinos/


[-- Attachment #2: Type: text/html, Size: 11464 bytes --]

Re: [Caml-list] Structural subtyping problem

[Andreas Rossberg]

On Mar 28, 2010, at 18.38 h, Dario Teixeira wrote:

> Hi,
>
> I'm using the structural subtyping aspects of Ocaml's object system  
> to emulate width
> subtyping.  I've come across a problem which does not type-check,  
> though intuitively
> it seems correct.  I reckon that the compiler may need some help in  
> the form of type
> annotations and/or coercions, though their exact shape elludes me.
>
> A simple nonsensical example that illustrates the problem is listed  
> below; the
> type-checking error occurs in function "step1", where the optional  
> parameter "story"
> is used as an object of type "< title:string; .. >".  In function  
> "step3", this
> parameter "story" is actually instantiated with objects of type "<  
> title:string >"
> and "< title:string; count:int >".
>
> Anyway, am I correct in assuming this should be feasible?  And if  
> so, what coercions
> are required to make this compile?

You problem is just that you try to use step1 polymorphically within a  
recursion. Polymorphic recursion is not (yet) allowed in OCaml.

You can side-step it by coercing the argument to a suitable  
monomorphic type in all uses of step1. In your example, that solution  
just consists of changing step3 as follows:

> and step3 ~story = match story#count with
> 	| 0 ->
> 		let story = (story :> <title:string>)
>                 in step1 ~story ()
> 	| 1 ->
> 		...

/Andreas

Re: [Caml-list] Structural subtyping problem

[Stéphane Glondu]

Dario Teixeira a écrit :
> A simple nonsensical example that illustrates the problem is listed below; the
> type-checking error occurs in function "step1", where the optional parameter "story"
> is used as an object of type "< title:string; .. >".  In function "step3", this
> parameter "story" is actually instantiated with objects of type "< title:string >"
> and "< title:string; count:int >".

As said elsewhere, this is because you are trying to do polymorphic
recursion. Standard tricks work here:

------------------------------------------------------------------------
type steps = {
  step1 : 'a. ?story:(<title : string; ..> as 'a) -> unit -> bool;
  step2 : string -> bool;
  step3 : 'a. story:(<title : string; count : int; ..> as 'a) -> bool
}

let rec steps = {

  step1 =
    begin fun ?story () ->
      match story with
        | Some s -> steps.step2 s#title
        | None -> steps.step2 "title1"
    end;

  step2 =
    begin fun title ->
      let story = object
        method title = title
        method count = 0
      end in
      steps.step3 story
    end;

  step3 =
    begin fun ~story ->
      match story#count with
        | 0 ->
	    steps.step1 ~story ()
        | 1 ->
	    let story = object
              method title = "title2"
            end in
            steps.step1 ~story ()
        | _ ->
	    true
    end
}

let step1 = steps.step1
let step2 = steps.step2
let step3 = steps.step3
------------------------------------------------------------------------

With OCaml 3.12, I guess this should be feasible without using the
intermediate "steps" record.


Cheers,

-- 
Stéphane

Re: [Caml-list] Structural subtyping problem

[Christophe TROESTLER]

Hi,

On Sun, 28 Mar 2010 19:32:37 +0200, Stéphane Glondu wrote:
> 
> type steps = {
>   step1 : 'a. ?story:(<title : string; ..> as 'a) -> unit -> bool;
>   step2 : string -> bool;
>   step3 : 'a. story:(<title : string; count : int; ..> as 'a) -> bool
> }
> 
> let rec steps = {  [...]

IMHO, recursive modules are also a nice way to achieve the same
effect :

module rec X :
sig
  val step1 : ?story:<title : string; ..> -> unit -> bool
  val step2 : string -> bool
  val step3 : story:<title : string; count : int; ..> -> bool
end = struct
  let rec step1 ?story () = match story with
    | Some s -> X.step2 s#title
    | None -> X.step2 "title1"

  and step2 title =
    let story = object
      method title = title
      method count = 0
    end in
    X.step3 story

  and step3 ~story = match story#count with
    | 0 -> X.step1 ~story ()
    | 1 ->
        let story = object
          method title = "title2"
        end in
        X.step1 ~story ()
    | _ -> true
end

My 0.02€,
C.

Re: [Caml-list] Structural subtyping problem

[Dario Teixeira]

Hi,

> I'm using the structural subtyping aspects of Ocaml's object system to emulate width
> subtyping.  I've come across a problem which does not type-check, though intuitively
> it seems correct.  I reckon that the compiler may need some help in the form of type
> annotations and/or coercions, though their exact shape elludes me.

Thank you all for your assistance.  In the real-world code, the solution
based on coercion is the most straightforward to implement.  And it looks
obvious now...

Cheers,
Dario Teixeira