caml-list - the Caml user's mailing list
 help / color / mirror / Atom feed
* [Caml-list] Segfault with open GADTs
@ 2016-10-18 12:47 Andre Nathan
  2016-10-18 13:10 ` Pierrick Couderc
  2016-10-18 13:16 ` Jeremy Yallop
  0 siblings, 2 replies; 6+ messages in thread
From: Andre Nathan @ 2016-10-18 12:47 UTC (permalink / raw)
  To: caml-list


[-- Attachment #1.1: Type: text/plain, Size: 884 bytes --]

Hi

I'm trying to use extensible variants to allow users to extend a type
from my library, which is a GADT, but it's resulting in a segfault when
the program is executed. I've managed to reproduce the issue with this code:

  module M0 = struct
    type 'a t = ..
    type 'a t +=
      | I : int -> int t
      | S : string -> string t
      | P : 'a t * 'b t -> ('a * 'b) t

    let rec to_string : type a. a t -> string = function
      | I i -> "I:" ^ string_of_int i
      | S s -> "S:" ^ s
      | P (x, y) -> to_string x ^ to_string y
  end

  module M1 = struct
    include M0
    type 'a t += T : 'a t -> 'a t

    let to_string = function
      | T t -> to_string t
      | x -> to_string x
  end

  let () =
    print_endline @@ M1.to_string (M1.P (M1.T (M1.I 42), M1.S "foo"))


Is this sort of thing supposed to work?

Thanks,
Andre


[-- Attachment #2: OpenPGP digital signature --]
[-- Type: application/pgp-signature, Size: 473 bytes --]

^ permalink raw reply	[flat|nested] 6+ messages in thread

* Re: [Caml-list] Segfault with open GADTs
  2016-10-18 12:47 [Caml-list] Segfault with open GADTs Andre Nathan
@ 2016-10-18 13:10 ` Pierrick Couderc
  2016-10-18 13:52   ` Andre Nathan
  2016-10-18 13:16 ` Jeremy Yallop
  1 sibling, 1 reply; 6+ messages in thread
From: Pierrick Couderc @ 2016-10-18 13:10 UTC (permalink / raw)
  To: Andre Nathan; +Cc: Ocaml Mailing List

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

Hi,

It is supposed to work, but it seems thepattern-matching compiler does not
detect that M0.to_string is non exhaustive, thus it does not add a
Match_Failure in case the variant is unknown. With extensible variants, a
pattern matching is only exhaustive if you provide a wildcard or a variable
for variants added afterwards.

You maybe should report it on the bug tracker!

2016-10-18 14:47 GMT+02:00 Andre Nathan <andre@digirati.com.br>:

> Hi
>
> I'm trying to use extensible variants to allow users to extend a type
> from my library, which is a GADT, but it's resulting in a segfault when
> the program is executed. I've managed to reproduce the issue with this
> code:
>
>   module M0 = struct
>     type 'a t = ..
>     type 'a t +=
>       | I : int -> int t
>       | S : string -> string t
>       | P : 'a t * 'b t -> ('a * 'b) t
>
>     let rec to_string : type a. a t -> string = function
>       | I i -> "I:" ^ string_of_int i
>       | S s -> "S:" ^ s
>       | P (x, y) -> to_string x ^ to_string y
>   end
>
>   module M1 = struct
>     include M0
>     type 'a t += T : 'a t -> 'a t
>
>     let to_string = function
>       | T t -> to_string t
>       | x -> to_string x
>   end
>
>   let () =
>     print_endline @@ M1.to_string (M1.P (M1.T (M1.I 42), M1.S "foo"))
>
>
> Is this sort of thing supposed to work?
>
> Thanks,
> Andre
>
>

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

^ permalink raw reply	[flat|nested] 6+ messages in thread

* Re: [Caml-list] Segfault with open GADTs
  2016-10-18 12:47 [Caml-list] Segfault with open GADTs Andre Nathan
  2016-10-18 13:10 ` Pierrick Couderc
@ 2016-10-18 13:16 ` Jeremy Yallop
  1 sibling, 0 replies; 6+ messages in thread
From: Jeremy Yallop @ 2016-10-18 13:16 UTC (permalink / raw)
  To: Andre Nathan; +Cc: Caml List

On 18 October 2016 at 13:47, Andre Nathan <andre@digirati.com.br> wrote:
> I'm trying to use extensible variants to allow users to extend a type
> from my library, which is a GADT, but it's resulting in a segfault when
> the program is executed. I've managed to reproduce the issue with this code:

It looks like an instance of this bug:

   http://caml.inria.fr/mantis/view.php?id=7330

^ permalink raw reply	[flat|nested] 6+ messages in thread

* Re: [Caml-list] Segfault with open GADTs
  2016-10-18 13:10 ` Pierrick Couderc
@ 2016-10-18 13:52   ` Andre Nathan
  2016-10-18 14:21     ` Goswin von Brederlow
  0 siblings, 1 reply; 6+ messages in thread
From: Andre Nathan @ 2016-10-18 13:52 UTC (permalink / raw)
  To: caml-list


[-- Attachment #1.1: Type: text/plain, Size: 780 bytes --]

On 10/18/2016 11:10 AM, Pierrick Couderc wrote:
> Hi,
> 
> It is supposed to work, but it seems thepattern-matching compiler does
> not detect that M0.to_string is non exhaustive, thus it does not add a
> Match_Failure in case the variant is unknown. With extensible variants,
> a pattern matching is only exhaustive if you provide a wildcard or a
> variable for variants added afterwards. 


Indeed, if I add a catch-all branch in M0.to_string then the code in
that branch is run, with no segfault.

But I guess my original idea of extending the type doesn't really work
as I hoped, since with nested expressions like that, I'd need to find a
way for M0.to_string to call back M1.to_string when a `T` is found.

Back to the drawing board...

Thanks,
Andre


[-- Attachment #2: OpenPGP digital signature --]
[-- Type: application/pgp-signature, Size: 473 bytes --]

^ permalink raw reply	[flat|nested] 6+ messages in thread

* Re: [Caml-list] Segfault with open GADTs
  2016-10-18 13:52   ` Andre Nathan
@ 2016-10-18 14:21     ` Goswin von Brederlow
  2016-10-18 14:50       ` Andre Nathan
  0 siblings, 1 reply; 6+ messages in thread
From: Goswin von Brederlow @ 2016-10-18 14:21 UTC (permalink / raw)
  To: caml-list

On Tue, Oct 18, 2016 at 11:52:40AM -0200, Andre Nathan wrote:
> On 10/18/2016 11:10 AM, Pierrick Couderc wrote:
> > Hi,
> > 
> > It is supposed to work, but it seems thepattern-matching compiler does
> > not detect that M0.to_string is non exhaustive, thus it does not add a
> > Match_Failure in case the variant is unknown. With extensible variants,
> > a pattern matching is only exhaustive if you provide a wildcard or a
> > variable for variants added afterwards. 
> 
> 
> Indeed, if I add a catch-all branch in M0.to_string then the code in
> that branch is run, with no segfault.
> 
> But I guess my original idea of extending the type doesn't really work
> as I hoped, since with nested expressions like that, I'd need to find a
> way for M0.to_string to call back M1.to_string when a `T` is found.
> 
> Back to the drawing board...
> 
> Thanks,
> Andre

You can pass along the outermost to_string to all to_string
functions so they can restart from the outside when they recurse.

MfG
	Goswin

^ permalink raw reply	[flat|nested] 6+ messages in thread

* Re: [Caml-list] Segfault with open GADTs
  2016-10-18 14:21     ` Goswin von Brederlow
@ 2016-10-18 14:50       ` Andre Nathan
  0 siblings, 0 replies; 6+ messages in thread
From: Andre Nathan @ 2016-10-18 14:50 UTC (permalink / raw)
  To: caml-list


[-- Attachment #1.1: Type: text/plain, Size: 810 bytes --]

On 10/18/2016 12:21 PM, Goswin von Brederlow wrote:
> You can pass along the outermost to_string to all to_string
> functions so they can restart from the outside when they recurse.

Yep :) For the record, I got it working like this:

In M0:

  let assert_false _ = assert false
  type f = { f : 'a. 'a t -> string }

  let rec to_string
      : type a b. ?f:f -> a t -> string
      = fun ?(f = { f = assert_false }) e -> match e with
      | I i -> "I:" ^ string_of_int i
      | S s -> "S:" ^ s
      | P (x, y) -> to_string ~f x ^ to_string ~f y
      | e -> f.f e

In M1:

    let rec to_string' : type a. a t -> string = function
      | T t -> to_string ~f:{ f = to_string' } t
      | x -> to_string ~f:{ f = to_string' } x

    let to_string = to_string'

Cheers,
Andre


[-- Attachment #2: OpenPGP digital signature --]
[-- Type: application/pgp-signature, Size: 473 bytes --]

^ permalink raw reply	[flat|nested] 6+ messages in thread

end of thread, other threads:[~2016-10-18 14:51 UTC | newest]

Thread overview: 6+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2016-10-18 12:47 [Caml-list] Segfault with open GADTs Andre Nathan
2016-10-18 13:10 ` Pierrick Couderc
2016-10-18 13:52   ` Andre Nathan
2016-10-18 14:21     ` Goswin von Brederlow
2016-10-18 14:50       ` Andre Nathan
2016-10-18 13:16 ` Jeremy Yallop

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).