Re: [Caml-list] GADTs and parsers

[Leo P White <lpw25@cam.ac.uk>]

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
>
>
>