[Caml-list] GADTs and parsers

[Caml-list] GADTs and parsers

[Dario Teixeira]

Hi,

I'm revisiting an old problem with 4.00's newfangled GADTs.  Suppose you have
four kinds of inline nodes, two of which (Text and Link) are leaves, while
the other two (Bold and Mref) are the parents of other nodes.  Moreover,
you want to enforce the invariant that a "linkish" node (Link and Mref)
may not be the ancestor of another linkish node.  One possible implementation:

type _ inline_t =
    | Text: string -> [> `Nonlink ] inline_t
    | Bold: 'a inline_t list -> 'a inline_t
    | Link: string -> [> `Link ] inline_t
    | Mref: string * [< `Nonlink ] inline_t list -> [> `Link ] inline_t


Defining a simple transformation function (in this case one which uppercases
all text) is also straightforward, just as long as one includes the proper
type annotations:

let uppercase seq =
    let rec process: type a. a inline_t -> a inline_t = function
        | Text txt       -> Text (String.uppercase txt)
        | Bold xs        -> Bold (List.map process xs)
        | Link lnk       -> Link lnk
        | Mref (lnk, xs) -> Mref (lnk, List.map process xs)
    in List.map process seq


But suppose now that I got from a parser a ast_t value with an almost identical
structure to inline_t, with the exception that it does not intrinsically
satisfy the latter's invariant:  (Note: for this toy example it may well be
easy to design the parser grammar such that the invariant is always preserved;
but suppose you're dealing with a "dumb" parser)

type ast_t =
    | Ast_Text of string
    | Ast_Bold of ast_t list
    | Ast_Link of string
    | Ast_Mref of string * ast_t list


Below is one possible implementation of a function that converts the possibly
"broken" ast_t into an inline_t.  Note how the processing is split into two
separate functions -- one which deals only with nonlinks, and other that
takes anything -- so we can be sure to satisfy the GADT constraints.

let inlineseq_from_astseq seq =
    let rec process_nonlink = function
        | Ast_Text txt  -> Text txt
        | Ast_Bold xs   -> Bold (List.map process_nonlink xs)
        | _             -> assert false in
    let rec process_any = function
        | Ast_Text txt       -> Text txt
        | Ast_Bold xs        -> Bold (List.map process_any xs)
        | Ast_Link lnk       -> Link lnk
        | Ast_Mref (lnk, xs) -> Mref (lnk, List.map process_nonlink xs)
    in List.map process_any seq


Now here's my problem: suppose I wanted to avoid the branch duplication
present in the above function.  The code below seems to do the trick,
while at the same time ensuring that the result is always a valid inline_t.
However, the compiler has trouble seeing that the code is a sound way to
produce convert an ast_t into an inline_t, and rejects the code.  Moreover,
it is not enough to simply add the type annotations for subfunction 'process',
as was done in 'uppercase'.

let inlineseq_from_astseq seq =
    let rec process allow_link ast = match (allow_link, ast) with
        | (_, Ast_Text txt)          -> Text txt
        | (x, Ast_Bold xs)           -> Bold (List.map (process x) xs)
        | (true, Ast_Link lnk)       -> Link lnk
        | (false, Ast_Link _)        -> assert false
        | (true, Ast_Mref (lnk, xs)) -> Mref (lnk, List.map (process false) xs)
        | (false, Ast_Mref _)        -> assert false
    in List.map (process true) seq


Can the single function approach be made to work?  I'm having trouble figuring
out just exactly what sort of help the compiler may require to see the code
above as correct...  (Assuming it is correct, of course...)

Thanks in advance for your time!
Cheers,
Dario Teixeira

Re: [Caml-list] GADTs and parsers

[Gabriel Scherer]

I suspect the problem may be one of variance: you are using
polymorphic variants, but implicitly assuming that ([ `Nolink ]
inline_t) is a subtype of ([ `Nolink | `Link ] inline_t), which means
that "inline_t" is covariant in its first parameter. However, variance
of GADTs is currently very strict, and your inline_t definition is in
fact considered invariant (to check that, replace "type _ inline_t" by
"type (+'a) inline_t" and watch the error), so this conversion does
not pass. On the contrary, with a phantom type definition, the
parameter is inferred to be irrelevant (any variance is accepted), so
you can do whatever you want inside the abstraction boundary.

Note that it may well be something else: with polymorphic variants
it's often hard to distinguish subtyping from polymorphic
instantiation (which will work just as well with GADTs), when you are
manipulating types polymorphic in the row variable ([< ... ] and [>
...]).

(For more information on GADTs and variance, see the previous thread
on this on the mailing-list; the summary is that it's complicated, but
I still hope we could get something finer in the future. It would
probably not work with polymorphic variant instances, anyway.)

On Sun, Jul 15, 2012 at 9:54 AM, Dario Teixeira <darioteixeira@yahoo.com> wrote:
> Hi,
>
> I'm revisiting an old problem with 4.00's newfangled GADTs.  Suppose you have
> four kinds of inline nodes, two of which (Text and Link) are leaves, while
> the other two (Bold and Mref) are the parents of other nodes.  Moreover,
> you want to enforce the invariant that a "linkish" node (Link and Mref)
> may not be the ancestor of another linkish node.  One possible implementation:
>
> type _ inline_t =
>     | Text: string -> [> `Nonlink ] inline_t
>     | Bold: 'a inline_t list -> 'a inline_t
>     | Link: string -> [> `Link ] inline_t
>     | Mref: string * [< `Nonlink ] inline_t list -> [> `Link ] inline_t
>
>
> Defining a simple transformation function (in this case one which uppercases
> all text) is also straightforward, just as long as one includes the proper
> type annotations:
>
> let uppercase seq =
>     let rec process: type a. a inline_t -> a inline_t = function
>         | Text txt       -> Text (String.uppercase txt)
>         | Bold xs        -> Bold (List.map process xs)
>         | Link lnk       -> Link lnk
>         | Mref (lnk, xs) -> Mref (lnk, List.map process xs)
>     in List.map process seq
>
>
> But suppose now that I got from a parser a ast_t value with an almost identical
> structure to inline_t, with the exception that it does not intrinsically
> satisfy the latter's invariant:  (Note: for this toy example it may well be
> easy to design the parser grammar such that the invariant is always preserved;
> but suppose you're dealing with a "dumb" parser)
>
> type ast_t =
>     | Ast_Text of string
>     | Ast_Bold of ast_t list
>     | Ast_Link of string
>     | Ast_Mref of string * ast_t list
>
>
> Below is one possible implementation of a function that converts the possibly
> "broken" ast_t into an inline_t.  Note how the processing is split into two
> separate functions -- one which deals only with nonlinks, and other that
> takes anything -- so we can be sure to satisfy the GADT constraints.
>
> let inlineseq_from_astseq seq =
>     let rec process_nonlink = function
>         | Ast_Text txt  -> Text txt
>         | Ast_Bold xs   -> Bold (List.map process_nonlink xs)
>         | _             -> assert false in
>     let rec process_any = function
>         | Ast_Text txt       -> Text txt
>         | Ast_Bold xs        -> Bold (List.map process_any xs)
>         | Ast_Link lnk       -> Link lnk
>         | Ast_Mref (lnk, xs) -> Mref (lnk, List.map process_nonlink xs)
>     in List.map process_any seq
>
>
> Now here's my problem: suppose I wanted to avoid the branch duplication
> present in the above function.  The code below seems to do the trick,
> while at the same time ensuring that the result is always a valid inline_t.
> However, the compiler has trouble seeing that the code is a sound way to
> produce convert an ast_t into an inline_t, and rejects the code.  Moreover,
> it is not enough to simply add the type annotations for subfunction 'process',
> as was done in 'uppercase'.
>
> let inlineseq_from_astseq seq =
>     let rec process allow_link ast = match (allow_link, ast) with
>         | (_, Ast_Text txt)          -> Text txt
>         | (x, Ast_Bold xs)           -> Bold (List.map (process x) xs)
>         | (true, Ast_Link lnk)       -> Link lnk
>         | (false, Ast_Link _)        -> assert false
>         | (true, Ast_Mref (lnk, xs)) -> Mref (lnk, List.map (process false) xs)
>         | (false, Ast_Mref _)        -> assert false
>     in List.map (process true) seq
>
>
> Can the single function approach be made to work?  I'm having trouble figuring
> out just exactly what sort of help the compiler may require to see the code
> above as correct...  (Assuming it is correct, of course...)
>
> Thanks in advance for your time!
> Cheers,
> Dario Teixeira
>
>
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa-roc.inria.fr/wws/info/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
>

Re: [Caml-list] GADTs and parsers

[Dario Teixeira]

Hi,

And thanks for the prompt reply!

> I suspect the problem may be one of variance: you are using

> polymorphic variants, but implicitly assuming that ([ `Nolink ]
> inline_t) is a subtype of ([ `Nolink | `Link ] inline_t), which means
> that "inline_t" is covariant in its first parameter. However, variance
> of GADTs is currently very strict, and your inline_t definition is in
> fact considered invariant (to check that, replace "type _ inline_t" by
> "type (+'a) inline_t" and watch the error), so this conversion does
> not pass. On the contrary, with a phantom type definition, the
> parameter is inferred to be irrelevant (any variance is accepted), so
> you can do whatever you want inside the abstraction boundary.

Ah, indeed.  And on a related note: is there a way to get the compiler
to spill out the variance it infers?  I'm assuming that 'ocamlc -i' does
not include inferred variance because it is generally "obvious" and
not something you usually have to worry about unless you want to
make a type abstract.  However, in a case like this it would help.
(Or does the compiler *always* assume invariance with GADTs?)


> (For more information on GADTs and variance, see the previous thread
> on this on the mailing-list; the summary is that it's complicated, but
> I still hope we could get something finer in the future. It would
> probably not work with polymorphic variant instances, anyway.)

In this case the use of polymorphic variants for the type parameter comes
in handy because there is a subtyping relation and the [> ] declaration
allows for useful mixing:

# let x1 = Text "ola";;
val x1 : [> `Nonlink ] inline_t = Text "ola"

# let x2 = Link "lnk";;
val x2 : [> `Link ] inline_t = Link "lnk"

# let xs = [x1; x2];;
val xs : [> `Link | `Nonlink ] inline_t list = [Text "ola"; Link "lnk"]

Cheers,
Dario

Re: [Caml-list] GADTs and parsers

[Leo P White]

What about something like (not really tested):

type _ guard_t = 
    | Nonlinked: [> `Nonlink ] guard_t
    | Either: [> `Nonlink | `Link ] guard_t

let inlineseq_from_astseq seq =
 let rec process : type a. a guard_t -> ast_t -> a inline_t = 
  fun guard ast -> 
   match (guard, ast) with
   | (Nonlinked, Ast_Text txt)   -> Text txt
   | (Either, Ast_Text txt)      -> Text txt
   | (x, Ast_Bold xs)            -> Bold (List.map (process x) xs)
   | (Either, Ast_Link lnk)      -> Link lnk
   | (Either, Ast_Mref (lnk, xs)) 
         -> Mref (lnk, List.map (process Nonlinked) xs) 
   | _   -> assert false
 in List.map (process Either) seq

Leo



On Jul 15 2012, Dario Teixeira wrote:

>Hi,
>
> I'm revisiting an old problem with 4.00's newfangled GADTs.  Suppose you 
> have four kinds of inline nodes, two of which (Text and Link) are leaves, 
> while the other two (Bold and Mref) are the parents of other nodes.  
> Moreover, you want to enforce the invariant that a "linkish" node (Link 
> and Mref) may not be the ancestor of another linkish node.  One possible 
> implementation:
>
>type _ inline_t =
>    | Text: string -> [> `Nonlink ] inline_t
>    | Bold: 'a inline_t list -> 'a inline_t
>    | Link: string -> [> `Link ] inline_t
>    | Mref: string * [< `Nonlink ] inline_t list -> [> `Link ] inline_t
>
>
> Defining a simple transformation function (in this case one which 
> uppercases all text) is also straightforward, just as long as one 
> includes the proper type annotations:
>
>let uppercase seq =
>    let rec process: type a. a inline_t -> a inline_t = function
>        | Text txt       -> Text (String.uppercase txt)
>        | Bold xs        -> Bold (List.map process xs)
>        | Link lnk       -> Link lnk
>        | Mref (lnk, xs) -> Mref (lnk, List.map process xs)
>    in List.map process seq
>
>
> But suppose now that I got from a parser a ast_t value with an almost 
> identical structure to inline_t, with the exception that it does not 
> intrinsically satisfy the latter's invariant:  (Note: for this toy 
> example it may well be easy to design the parser grammar such that the 
> invariant is always preserved; but suppose you're dealing with a "dumb" 
> parser)
>
>type ast_t =
>    | Ast_Text of string
>    | Ast_Bold of ast_t list
>    | Ast_Link of string
>    | Ast_Mref of string * ast_t list
>
>
> Below is one possible implementation of a function that converts the 
> possibly "broken" ast_t into an inline_t.  Note how the processing is 
> split into two separate functions -- one which deals only with nonlinks, 
> and other that takes anything -- so we can be sure to satisfy the GADT 
> constraints.
>
>let inlineseq_from_astseq seq =
>    let rec process_nonlink = function
>        | Ast_Text txt  -> Text txt
>        | Ast_Bold xs   -> Bold (List.map process_nonlink xs)
>        | _             -> assert false in
>    let rec process_any = function
>        | Ast_Text txt       -> Text txt
>        | Ast_Bold xs        -> Bold (List.map process_any xs)
>        | Ast_Link lnk       -> Link lnk
>        | Ast_Mref (lnk, xs) -> Mref (lnk, List.map process_nonlink xs)
>    in List.map process_any seq
>
>
> Now here's my problem: suppose I wanted to avoid the branch duplication 
> present in the above function.  The code below seems to do the trick, 
> while at the same time ensuring that the result is always a valid 
> inline_t. However, the compiler has trouble seeing that the code is a 
> sound way to produce convert an ast_t into an inline_t, and rejects the 
> code.  Moreover, it is not enough to simply add the type annotations for 
> subfunction 'process', as was done in 'uppercase'.
>
> let inlineseq_from_astseq seq =     let rec process allow_link ast = 
> match (allow_link, ast) with         | (_, Ast_Text txt)          -> Text 
> txt         | (x, Ast_Bold xs)           -> Bold (List.map (process x) 
> xs)         | (true, Ast_Link lnk)       -> Link lnk         | (false, 
> Ast_Link _)        -> assert false         | (true, Ast_Mref (lnk, xs)) 
> -> Mref (lnk, List.map (process false) xs)         | (false, Ast_Mref 
> _)        -> assert false     in List.map (process true) seq
>
>
> Can the single function approach be made to work?  I'm having trouble 
> figuring out just exactly what sort of help the compiler may require to 
> see the code above as correct...  (Assuming it is correct, of course...)
>
>Thanks in advance for your time!
>Cheers,
>Dario Teixeira
>
>
>

Re: [Caml-list] GADTs and parsers

[Gabriel Scherer]

> In this case the use of polymorphic variants for the type parameter comes
> in handy because there is a subtyping relation and the [> ] declaration
> allows for useful mixing

Precisely, your example does *not* use subtyping (it's easy to see: in
OCaml, subtyping is explicit, you have to use (e :> t) casts. If there
are none, you're not using subtyping). [> `Link ] is actually a
shortcut for something like [ `Link | 'r ], where 'r is a polymorphic
row variable that stands for any number of additional cases. So going
from [> `Link ] to [> `Link | `Nolink ] is not subtyping, only
instantiation of 'r into (`Nolink | 'r2) for a fresh 'r2.

So it may be the case that your previous example also could work with
the parameter invariant. I haven't looked at it deeply enough to tell.

On Sun, Jul 15, 2012 at 11:58 AM, Dario Teixeira
<darioteixeira@yahoo.com> wrote:
> Hi,
>
> And thanks for the prompt reply!
>
>> I suspect the problem may be one of variance: you are using
>
>> polymorphic variants, but implicitly assuming that ([ `Nolink ]
>> inline_t) is a subtype of ([ `Nolink | `Link ] inline_t), which means
>> that "inline_t" is covariant in its first parameter. However, variance
>> of GADTs is currently very strict, and your inline_t definition is in
>> fact considered invariant (to check that, replace "type _ inline_t" by
>> "type (+'a) inline_t" and watch the error), so this conversion does
>> not pass. On the contrary, with a phantom type definition, the
>> parameter is inferred to be irrelevant (any variance is accepted), so
>> you can do whatever you want inside the abstraction boundary.
>
> Ah, indeed.  And on a related note: is there a way to get the compiler
> to spill out the variance it infers?  I'm assuming that 'ocamlc -i' does
> not include inferred variance because it is generally "obvious" and
> not something you usually have to worry about unless you want to
> make a type abstract.  However, in a case like this it would help.
> (Or does the compiler *always* assume invariance with GADTs?)
>
>
>> (For more information on GADTs and variance, see the previous thread
>> on this on the mailing-list; the summary is that it's complicated, but
>> I still hope we could get something finer in the future. It would
>> probably not work with polymorphic variant instances, anyway.)
>
> In this case the use of polymorphic variants for the type parameter comes
> in handy because there is a subtyping relation and the [> ] declaration
> allows for useful mixing:
>
> # let x1 = Text "ola";;
> val x1 : [> `Nonlink ] inline_t = Text "ola"
>
> # let x2 = Link "lnk";;
> val x2 : [> `Link ] inline_t = Link "lnk"
>
> # let xs = [x1; x2];;
> val xs : [> `Link | `Nonlink ] inline_t list = [Text "ola"; Link "lnk"]
>
> Cheers,
> Dario

Re: [Caml-list] GADTs and parsers

[Jacques Garrigue]

Actually Leo more or less gave you the answer:
since your recursive process function needs to return either
`Nonlink or any inline_t nodes, it has to be polymorphically
recursive, and use a custom GADT to connect the allow_link
parameter with the result type.

Here is a more complete version of his code.
I also changed a bit your types, because there is another problem
using polymorphic variants with GADTs: when you get a GADT
equation involving a refinable polymorphic variant, you are going
to get get a local private type. If your type is unbounded, you
cannot even use subtyping on it. Also [< `Nonlink] has exactly
the same elements as [ `Nonlink], so it is better to use the latter.

   Jacques

type inkind = [ `Link | `Nonlink ]

type _ inline_t =
    | Text: string -> [< inkind > `Nonlink ] inline_t
    | Bold: 'a inline_t list -> 'a inline_t
    | Link: string -> [< inkind > `Link ] inline_t
    | Mref: string * [ `Nonlink ] inline_t list -> [< inkind > `Link ] inline_t

let uppercase seq =
    let rec process: type a. a inline_t -> a inline_t = function
        | Text txt       -> Text (String.uppercase txt)
        | Bold xs        -> Bold (List.map process xs)
        | Link lnk       -> Link lnk
        | Mref (lnk, xs) -> Mref (lnk, List.map process xs)
    in List.map process seq

type ast_t =
    | Ast_Text of string
    | Ast_Bold of ast_t list
    | Ast_Link of string
    | Ast_Mref of string * ast_t list

let inlineseq_from_astseq seq =
    let rec process_nonlink = function
        | Ast_Text txt  -> Text txt
        | Ast_Bold xs   -> Bold (List.map process_nonlink xs)
        | _             -> assert false in
    let rec process_any = function
        | Ast_Text txt       -> Text txt
        | Ast_Bold xs        -> Bold (List.map process_any xs)
        | Ast_Link lnk       -> Link lnk
        | Ast_Mref (lnk, xs) -> Mref (lnk, List.map process_nonlink xs)
    in List.map process_any seq

type _ linkp =
  | Nonlink : [ `Nonlink ] linkp
  | Maylink : inkind linkp

let inlineseq_from_astseq seq =
  let rec process : type a. a linkp -> ast_t -> a inline_t =
    fun allow_link ast ->
      match (allow_link, ast) with
      | (Maylink, Ast_Text txt)    -> Text txt
      | (Nonlink, Ast_Text txt)    -> Text txt
      | (x, Ast_Bold xs)           -> Bold (List.map (process x) xs)
      | (Maylink, Ast_Link lnk)    -> Link lnk
      | (Nonlink, Ast_Link _)      -> assert false
      | (Maylink, Ast_Mref (lnk, xs)) ->
          Mref (lnk, List.map (process Nonlink) xs)
      | (Nonlink, Ast_Mref _)      -> assert false
    in List.map (process Maylink) seq


On 2012/07/16, at 1:54, Dario Teixeira wrote:

> Hi,
> 
> I'm revisiting an old problem with 4.00's newfangled GADTs.  Suppose you have
> four kinds of inline nodes, two of which (Text and Link) are leaves, while
> the other two (Bold and Mref) are the parents of other nodes.  Moreover,
> you want to enforce the invariant that a "linkish" node (Link and Mref)
> may not be the ancestor of another linkish node.  One possible implementation:
> 
> type _ inline_t =
>     | Text: string -> [> `Nonlink ] inline_t
>     | Bold: 'a inline_t list -> 'a inline_t
>     | Link: string -> [> `Link ] inline_t
>     | Mref: string * [< `Nonlink ] inline_t list -> [> `Link ] inline_t
> 
> 
> Defining a simple transformation function (in this case one which uppercases
> all text) is also straightforward, just as long as one includes the proper
> type annotations:
> 
> let uppercase seq =
>     let rec process: type a. a inline_t -> a inline_t = function
>         | Text txt       -> Text (String.uppercase txt)
>         | Bold xs        -> Bold (List.map process xs)
>         | Link lnk       -> Link lnk
>         | Mref (lnk, xs) -> Mref (lnk, List.map process xs)
>     in List.map process seq
> 
> 
> But suppose now that I got from a parser a ast_t value with an almost identical
> structure to inline_t, with the exception that it does not intrinsically
> satisfy the latter's invariant:  (Note: for this toy example it may well be
> easy to design the parser grammar such that the invariant is always preserved;
> but suppose you're dealing with a "dumb" parser)
> 
> type ast_t =
>     | Ast_Text of string
>     | Ast_Bold of ast_t list
>     | Ast_Link of string
>     | Ast_Mref of string * ast_t list
> 
> 
> Below is one possible implementation of a function that converts the possibly
> "broken" ast_t into an inline_t.  Note how the processing is split into two
> separate functions -- one which deals only with nonlinks, and other that
> takes anything -- so we can be sure to satisfy the GADT constraints.
> 
> let inlineseq_from_astseq seq =
>     let rec process_nonlink = function
>         | Ast_Text txt  -> Text txt
>         | Ast_Bold xs   -> Bold (List.map process_nonlink xs)
>         | _             -> assert false in
>     let rec process_any = function
>         | Ast_Text txt       -> Text txt
>         | Ast_Bold xs        -> Bold (List.map process_any xs)
>         | Ast_Link lnk       -> Link lnk
>         | Ast_Mref (lnk, xs) -> Mref (lnk, List.map process_nonlink xs)
>     in List.map process_any seq
> 
> 
> Now here's my problem: suppose I wanted to avoid the branch duplication
> present in the above function.  The code below seems to do the trick,
> while at the same time ensuring that the result is always a valid inline_t.
> However, the compiler has trouble seeing that the code is a sound way to
> produce convert an ast_t into an inline_t, and rejects the code.  Moreover,
> it is not enough to simply add the type annotations for subfunction 'process',
> as was done in 'uppercase'.
> 
> let inlineseq_from_astseq seq =
>     let rec process allow_link ast = match (allow_link, ast) with
>         | (_, Ast_Text txt)          -> Text txt
>         | (x, Ast_Bold xs)           -> Bold (List.map (process x) xs)
>         | (true, Ast_Link lnk)       -> Link lnk
>         | (false, Ast_Link _)        -> assert false
>         | (true, Ast_Mref (lnk, xs)) -> Mref (lnk, List.map (process false) xs)
>         | (false, Ast_Mref _)        -> assert false
>     in List.map (process true) seq
> 
> 
> Can the single function approach be made to work?  I'm having trouble figuring
> out just exactly what sort of help the compiler may require to see the code
> above as correct...  (Assuming it is correct, of course...)
> 
> Thanks in advance for your time!
> Cheers,
> Dario Teixeira
> 
> 
> -- 
> Caml-list mailing list.  Subscription management and archives:
> https://sympa-roc.inria.fr/wws/info/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
> 

Re: [Caml-list] GADTs and parsers

[Leo P White]

The duplicated Ast_Text case in the process function can also be avoided by 
using another layer of GADT, so that Jacques version becomes:

type _ linkp =
  | Nonlink : [ `Nonlink ] linkp
  | Maylink : inkind linkp

type _ linkp2 = Kind : 'a linkp -> ([< inkind ] as 'a) linkp2

let inlineseq_from_astseq seq =
  let rec process : type a. a linkp2 -> ast_t -> a inline_t =
    fun allow_link ast ->
      match (allow_link, ast) with
      | (Kind _, Ast_Text txt)    -> Text txt
      | (x, Ast_Bold xs)           -> Bold (List.map (process x) xs)
      | (Kind Maylink, Ast_Link lnk)    -> Link lnk
      | (Kind Nonlink, Ast_Link _)      -> assert false
      | (Kind Maylink, Ast_Mref (lnk, xs)) ->
          Mref (lnk, List.map (process (Kind Nonlink)) xs)
      | (Kind Nonlink, Ast_Mref _)      -> assert false
    in List.map (process (Kind Maylink)) seq

Regards,

Leo

On Jul 15 2012, Jacques Garrigue wrote:

>Actually Leo more or less gave you the answer:
>since your recursive process function needs to return either
>`Nonlink or any inline_t nodes, it has to be polymorphically
>recursive, and use a custom GADT to connect the allow_link
>parameter with the result type.
>
>Here is a more complete version of his code.
>I also changed a bit your types, because there is another problem
>using polymorphic variants with GADTs: when you get a GADT
>equation involving a refinable polymorphic variant, you are going
>to get get a local private type. If your type is unbounded, you
>cannot even use subtyping on it. Also [< `Nonlink] has exactly
>the same elements as [ `Nonlink], so it is better to use the latter.
>
>   Jacques
>
>type inkind = [ `Link | `Nonlink ]
>
>type _ inline_t =
>    | Text: string -> [< inkind > `Nonlink ] inline_t Bold: 'a inline_t 
>    | list -> 'a inline_t Link: string -> [< inkind > `Link ] inline_t 
>    | Mref: string * [ `Nonlink ] inline_t list -> [< inkind > `Link ] 
>    | inline_t
>
>let uppercase seq =
>    let rec process: type a. a inline_t -> a inline_t = function
>        | Text txt       -> Text (String.uppercase txt)
>        | Bold xs        -> Bold (List.map process xs)
>        | Link lnk       -> Link lnk
>        | Mref (lnk, xs) -> Mref (lnk, List.map process xs)
>    in List.map process seq
>
>type ast_t =
>    | Ast_Text of string
>    | Ast_Bold of ast_t list
>    | Ast_Link of string
>    | Ast_Mref of string * ast_t list
>
>let inlineseq_from_astseq seq =
>    let rec process_nonlink = function
>        | Ast_Text txt  -> Text txt
>        | Ast_Bold xs   -> Bold (List.map process_nonlink xs)
>        | _             -> assert false in
>    let rec process_any = function
>        | Ast_Text txt       -> Text txt
>        | Ast_Bold xs        -> Bold (List.map process_any xs)
>        | Ast_Link lnk       -> Link lnk
>        | Ast_Mref (lnk, xs) -> Mref (lnk, List.map process_nonlink xs)
>    in List.map process_any seq
>
>type _ linkp =
>  | Nonlink : [ `Nonlink ] linkp
>  | Maylink : inkind linkp
>
>let inlineseq_from_astseq seq =
>  let rec process : type a. a linkp -> ast_t -> a inline_t =
>    fun allow_link ast ->
>      match (allow_link, ast) with
>      | (Maylink, Ast_Text txt)    -> Text txt
>      | (Nonlink, Ast_Text txt)    -> Text txt
>      | (x, Ast_Bold xs)           -> Bold (List.map (process x) xs)
>      | (Maylink, Ast_Link lnk)    -> Link lnk
>      | (Nonlink, Ast_Link _)      -> assert false
>      | (Maylink, Ast_Mref (lnk, xs)) ->
>          Mref (lnk, List.map (process Nonlink) xs)
>      | (Nonlink, Ast_Mref _)      -> assert false
>    in List.map (process Maylink) seq
>
>
>On 2012/07/16, at 1:54, Dario Teixeira wrote:
>
>> Hi,
>> 
>> I'm revisiting an old problem with 4.00's newfangled GADTs. Suppose you 
>> have four kinds of inline nodes, two of which (Text and Link) are 
>> leaves, while the other two (Bold and Mref) are the parents of other 
>> nodes. Moreover, you want to enforce the invariant that a "linkish" node 
>> (Link and Mref) may not be the ancestor of another linkish node. One 
>> possible implementation:
>> 
>> type _ inline_t =
>>     | Text: string -> [> `Nonlink ] inline_t
>>     | Bold: 'a inline_t list -> 'a inline_t
>>     | Link: string -> [> `Link ] inline_t
>>     | Mref: string * [< `Nonlink ] inline_t list -> [> `Link ] inline_t
>> 
>> 
>> Defining a simple transformation function (in this case one which 
>> uppercases all text) is also straightforward, just as long as one 
>> includes the proper type annotations:
>> 
>> let uppercase seq =
>>     let rec process: type a. a inline_t -> a inline_t = function
>>         | Text txt       -> Text (String.uppercase txt)
>>         | Bold xs        -> Bold (List.map process xs)
>>         | Link lnk       -> Link lnk
>>         | Mref (lnk, xs) -> Mref (lnk, List.map process xs)
>>     in List.map process seq
>> 
>> 
>> But suppose now that I got from a parser a ast_t value with an almost 
>> identical structure to inline_t, with the exception that it does not 
>> intrinsically satisfy the latter's invariant: (Note: for this toy 
>> example it may well be easy to design the parser grammar such that the 
>> invariant is always preserved; but suppose you're dealing with a "dumb" 
>> parser)
>> 
>> type ast_t =
>>     | Ast_Text of string
>>     | Ast_Bold of ast_t list
>>     | Ast_Link of string
>>     | Ast_Mref of string * ast_t list
>> 
>> 
>> Below is one possible implementation of a function that converts the 
>> possibly "broken" ast_t into an inline_t. Note how the processing is 
>> split into two separate functions -- one which deals only with nonlinks, 
>> and other that takes anything -- so we can be sure to satisfy the GADT 
>> constraints.
>> 
>> let inlineseq_from_astseq seq =
>>     let rec process_nonlink = function
>>         | Ast_Text txt  -> Text txt
>>         | Ast_Bold xs   -> Bold (List.map process_nonlink xs)
>>         | _             -> assert false in
>>     let rec process_any = function
>>         | Ast_Text txt       -> Text txt
>>         | Ast_Bold xs        -> Bold (List.map process_any xs)
>>         | Ast_Link lnk       -> Link lnk
>>         | Ast_Mref (lnk, xs) -> Mref (lnk, List.map process_nonlink xs)
>>     in List.map process_any seq
>> 
>> 
>> Now here's my problem: suppose I wanted to avoid the branch duplication 
>> present in the above function. The code below seems to do the trick, 
>> while at the same time ensuring that the result is always a valid 
>> inline_t. However, the compiler has trouble seeing that the code is a 
>> sound way to produce convert an ast_t into an inline_t, and rejects the 
>> code. Moreover, it is not enough to simply add the type annotations for 
>> subfunction 'process', as was done in 'uppercase'.
>> 
>> let inlineseq_from_astseq seq =
>>     let rec process allow_link ast = match (allow_link, ast) with
>>         | (_, Ast_Text txt) -> Text txt (x, Ast_Bold xs) -> Bold 
>>         | (List.map (process x) xs) (true, Ast_Link lnk) -> Link lnk 
>>         | (false, Ast_Link _) -> assert false (true, Ast_Mref (lnk, xs)) 
>>         | -> Mref (lnk, List.map (process false) xs) (false, Ast_Mref _) 
>>         | -> assert false
>>     in List.map (process true) seq
>> 
>> 
>> Can the single function approach be made to work? I'm having trouble 
>> figuring out just exactly what sort of help the compiler may require to 
>> see the code above as correct... (Assuming it is correct, of course...)
>> 
>> Thanks in advance for your time!
>> Cheers,
>> Dario Teixeira
>> 
>> 
>> -- 
>> Caml-list mailing list.  Subscription management and archives:
>> https://sympa-roc.inria.fr/wws/info/caml-list
>> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
>> Bug reports: http://caml.inria.fr/bin/caml-bugs
>> 
>
>
>

Re: [Caml-list] GADTs and parsers

[Leo P White]

Sorry there was a typo in my previous e-mail, and the second GADT should be:

type _ linkp2 = Kind : 'a linkp -> ([< inkind > `Nonlink] as 'a) linkp2

However, the broken version does appear to be allowed by the type checker, 
which (assuming I haven't misunderstood Jacques' version of the inline_t 
type) seems to be a bug in the compiler, because it also allows:

# let broken seq =
  let rec process : type a. a linkp2 -> ast_t -> a inline_t =
    fun allow_link ast ->
      match (allow_link, ast) with
      | (Kind _, Ast_Text txt)    -> Link txt
      | (x, Ast_Bold xs)           -> Bold (List.map (process x) xs)
      | (Kind Maylink, Ast_Link lnk)    -> Link lnk
      | (Kind Nonlink, Ast_Link _)      -> assert false
      | (Kind Maylink, Ast_Mref (lnk, xs)) ->
          Mref (lnk, List.map (process (Kind Nonlink)) xs)
      | (Kind Nonlink, Ast_Mref _)      -> assert false
    in List.map (process (Kind Maylink)) seq;;
                      val broken : ast_t list -> inkind inline_t list = 
<fun>

# broken [Ast_Mref("foo", [Ast_Text "bar"])];;
- : inkind inline_t list = [Mref ("foo", [Link <abstr>])]

which breaks the desired invariant that an MRef doesn't contain a Link node.

Have I misunderstood something, or is this indeed a bug?

Regards,

Leo




On Jul 16 2012, Leo P White wrote:

>
> The duplicated Ast_Text case in the process function can also be avoided 
> by using another layer of GADT, so that Jacques version becomes:
>
>type _ linkp =
>  | Nonlink : [ `Nonlink ] linkp
>  | Maylink : inkind linkp
>
>type _ linkp2 = Kind : 'a linkp -> ([< inkind ] as 'a) linkp2
>
>let inlineseq_from_astseq seq =
>  let rec process : type a. a linkp2 -> ast_t -> a inline_t =
>    fun allow_link ast ->
>      match (allow_link, ast) with
>      | (Kind _, Ast_Text txt)    -> Text txt
>      | (x, Ast_Bold xs)           -> Bold (List.map (process x) xs)
>      | (Kind Maylink, Ast_Link lnk)    -> Link lnk
>      | (Kind Nonlink, Ast_Link _)      -> assert false
>      | (Kind Maylink, Ast_Mref (lnk, xs)) ->
>          Mref (lnk, List.map (process (Kind Nonlink)) xs)
>      | (Kind Nonlink, Ast_Mref _)      -> assert false
>    in List.map (process (Kind Maylink)) seq
>
>Regards,
>
>Leo
>
>On Jul 15 2012, Jacques Garrigue wrote:
>
>>Actually Leo more or less gave you the answer:
>>since your recursive process function needs to return either
>>`Nonlink or any inline_t nodes, it has to be polymorphically
>>recursive, and use a custom GADT to connect the allow_link
>>parameter with the result type.
>>
>>Here is a more complete version of his code.
>>I also changed a bit your types, because there is another problem
>>using polymorphic variants with GADTs: when you get a GADT
>>equation involving a refinable polymorphic variant, you are going
>>to get get a local private type. If your type is unbounded, you
>>cannot even use subtyping on it. Also [< `Nonlink] has exactly
>>the same elements as [ `Nonlink], so it is better to use the latter.
>>
>>   Jacques
>>
>>type inkind = [ `Link | `Nonlink ]
>>
>>type _ inline_t =
>>    | Text: string -> [< inkind > `Nonlink ] inline_t Bold: 'a inline_t 
>>    | list -> 'a inline_t Link: string -> [< inkind > `Link ] inline_t 
>>    | Mref: string * [ `Nonlink ] inline_t list -> [< inkind > `Link ] 
>>    | inline_t
>>
>>let uppercase seq =
>>    let rec process: type a. a inline_t -> a inline_t = function
>>        | Text txt       -> Text (String.uppercase txt)
>>        | Bold xs        -> Bold (List.map process xs)
>>        | Link lnk       -> Link lnk
>>        | Mref (lnk, xs) -> Mref (lnk, List.map process xs)
>>    in List.map process seq
>>
>>type ast_t =
>>    | Ast_Text of string
>>    | Ast_Bold of ast_t list
>>    | Ast_Link of string
>>    | Ast_Mref of string * ast_t list
>>
>>let inlineseq_from_astseq seq =
>>    let rec process_nonlink = function
>>        | Ast_Text txt  -> Text txt
>>        | Ast_Bold xs   -> Bold (List.map process_nonlink xs)
>>        | _             -> assert false in
>>    let rec process_any = function
>>        | Ast_Text txt       -> Text txt
>>        | Ast_Bold xs        -> Bold (List.map process_any xs)
>>        | Ast_Link lnk       -> Link lnk
>>        | Ast_Mref (lnk, xs) -> Mref (lnk, List.map process_nonlink xs)
>>    in List.map process_any seq
>>
>>type _ linkp =
>>  | Nonlink : [ `Nonlink ] linkp
>>  | Maylink : inkind linkp
>>
>>let inlineseq_from_astseq seq =
>>  let rec process : type a. a linkp -> ast_t -> a inline_t =
>>    fun allow_link ast ->
>>      match (allow_link, ast) with
>>      | (Maylink, Ast_Text txt)    -> Text txt
>>      | (Nonlink, Ast_Text txt)    -> Text txt
>>      | (x, Ast_Bold xs)           -> Bold (List.map (process x) xs)
>>      | (Maylink, Ast_Link lnk)    -> Link lnk
>>      | (Nonlink, Ast_Link _)      -> assert false
>>      | (Maylink, Ast_Mref (lnk, xs)) ->
>>          Mref (lnk, List.map (process Nonlink) xs)
>>      | (Nonlink, Ast_Mref _)      -> assert false
>>    in List.map (process Maylink) seq
>>
>>
>>On 2012/07/16, at 1:54, Dario Teixeira wrote:
>>
>>> Hi,
>>> 
>>> I'm revisiting an old problem with 4.00's newfangled GADTs. Suppose 
>>> you have four kinds of inline nodes, two of which (Text and Link) are 
>>> leaves, while the other two (Bold and Mref) are the parents of other 
>>> nodes. Moreover, you want to enforce the invariant that a "linkish" 
>>> node (Link and Mref) may not be the ancestor of another linkish node. 
>>> One possible implementation:
>>> 
>>> type _ inline_t =
>>>     | Text: string -> [> `Nonlink ] inline_t
>>>     | Bold: 'a inline_t list -> 'a inline_t
>>>     | Link: string -> [> `Link ] inline_t
>>>     | Mref: string * [< `Nonlink ] inline_t list -> [> `Link ] inline_t
>>> 
>>> 
>>> Defining a simple transformation function (in this case one which 
>>> uppercases all text) is also straightforward, just as long as one 
>>> includes the proper type annotations:
>>> 
>>> let uppercase seq =
>>>     let rec process: type a. a inline_t -> a inline_t = function
>>>         | Text txt       -> Text (String.uppercase txt)
>>>         | Bold xs        -> Bold (List.map process xs)
>>>         | Link lnk       -> Link lnk
>>>         | Mref (lnk, xs) -> Mref (lnk, List.map process xs)
>>>     in List.map process seq
>>> 
>>> 
>>> But suppose now that I got from a parser a ast_t value with an almost 
>>> identical structure to inline_t, with the exception that it does not 
>>> intrinsically satisfy the latter's invariant: (Note: for this toy 
>>> example it may well be easy to design the parser grammar such that the 
>>> invariant is always preserved; but suppose you're dealing with a "dumb" 
>>> parser)
>>> 
>>> type ast_t =
>>>     | Ast_Text of string
>>>     | Ast_Bold of ast_t list
>>>     | Ast_Link of string
>>>     | Ast_Mref of string * ast_t list
>>> 
>>> 
>>> Below is one possible implementation of a function that converts the 
>>> possibly "broken" ast_t into an inline_t. Note how the processing is 
>>> split into two separate functions -- one which deals only with 
>>> nonlinks, and other that takes anything -- so we can be sure to satisfy 
>>> the GADT constraints.
>>> 
>>> let inlineseq_from_astseq seq =
>>>     let rec process_nonlink = function
>>>         | Ast_Text txt  -> Text txt
>>>         | Ast_Bold xs   -> Bold (List.map process_nonlink xs)
>>>         | _             -> assert false in
>>>     let rec process_any = function
>>>         | Ast_Text txt       -> Text txt
>>>         | Ast_Bold xs        -> Bold (List.map process_any xs)
>>>         | Ast_Link lnk       -> Link lnk
>>>         | Ast_Mref (lnk, xs) -> Mref (lnk, List.map process_nonlink xs)
>>>     in List.map process_any seq
>>> 
>>> 
>>> Now here's my problem: suppose I wanted to avoid the branch duplication 
>>> present in the above function. The code below seems to do the trick, 
>>> while at the same time ensuring that the result is always a valid 
>>> inline_t. However, the compiler has trouble seeing that the code is a 
>>> sound way to produce convert an ast_t into an inline_t, and rejects the 
>>> code. Moreover, it is not enough to simply add the type annotations for 
>>> subfunction 'process', as was done in 'uppercase'.
>>> 
>>> let inlineseq_from_astseq seq =
>>>     let rec process allow_link ast = match (allow_link, ast) with
>>>         | (_, Ast_Text txt) -> Text txt (x, Ast_Bold xs) -> Bold 
>>>         | (List.map (process x) xs) (true, Ast_Link lnk) -> Link lnk 
>>>         | (false, Ast_Link _) -> assert false (true, Ast_Mref (lnk, 
>>>         | xs)) -> Mref (lnk, List.map (process false) xs) (false, 
>>>         | Ast_Mref _) -> assert false
>>>     in List.map (process true) seq
>>> 
>>> 
>>> Can the single function approach be made to work? I'm having trouble 
>>> figuring out just exactly what sort of help the compiler may require to 
>>> see the code above as correct... (Assuming it is correct, of course...)
>>> 
>>> Thanks in advance for your time!
>>> Cheers,
>>> Dario Teixeira
>>> 
>>> 
>>> -- 
>>> Caml-list mailing list.  Subscription management and archives:
>>> https://sympa-roc.inria.fr/wws/info/caml-list
>>> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
>>> Bug reports: http://caml.inria.fr/bin/caml-bugs
>>> 
>>
>>
>>
>
>

Re: [Caml-list] GADTs and parsers

[Dario Teixeira]

Hi,

> What about something like (not really tested):

> 
> type _ guard_t =    | Nonlinked: [> `Nonlink ] guard_t
>    | Either: [> `Nonlink | `Link ] guard_t
> 
> let inlineseq_from_astseq seq =
> let rec process : type a. a guard_t -> ast_t -> a inline_t =  fun guard 
> ast ->   match (guard, ast) with
>   | (Nonlinked, Ast_Text txt)   -> Text txt
>   | (Either, Ast_Text txt)      -> Text txt
>   | (x, Ast_Bold xs)            -> Bold (List.map (process x) xs)
>   | (Either, Ast_Link lnk)      -> Link lnk
>   | (Either, Ast_Mref (lnk, xs))         -> Mref (lnk, List.map (process 
> Nonlinked) xs)   | _   -> assert false
> in List.map (process Either) seq

I see what you mean -- using an auxiliary GADT basically.
Nice technique to keep in mind -- thanks!

Cheers,
Dario

Re: [Caml-list] GADTs and parsers

[Dario Teixeira]

Hi,

> Here is a more complete version of his code.

> I also changed a bit your types, because there is another problem
> using polymorphic variants with GADTs: when you get a GADT
> equation involving a refinable polymorphic variant, you are going
> to get get a local private type. If your type is unbounded, you
> cannot even use subtyping on it. Also [< `Nonlink] has exactly
> the same elements as [ `Nonlink], so it is better to use the latter.
> 
>    Jacques
> 
> type inkind = [ `Link | `Nonlink ]
> 
> type _ inline_t =
>     | Text: string -> [< inkind > `Nonlink ] inline_t
>     | Bold: 'a inline_t list -> 'a inline_t
>     | Link: string -> [< inkind > `Link ] inline_t
>     | Mref: string * [ `Nonlink ] inline_t list -> [< inkind > `Link ] 
> inline_t

Thanks for the input!  You are right, it is easy to forget that a declaration
such as [> `Nonlink ] is way more open than intended, particularly in this
case where only `Nonlink and `Link are in play.

Anyway, this sort of "closed variant", though mentioned in the language reference,
is a subtlety of polymorphic variants which is not mentioned in section 4.2 (tutorial)
of the manual.  I know the manual is not intended as a full-blown tutorial on the
language, but I reckon it could benefit from mentioning this aspect...

Best regards,
Dario Teixeira