2013/1/5 Jeremy Yallop <yallop@gmail.com>

On 5 January 2013 13:40, Philippe Veber <philippe.veber@gmail.com> wrote:
> I still have a question though: what is the exact meaning of the _
> character in the polymorphic type "< rn : 'a. int * 'a expr -> _>"
> and how is it useful/necessary for your example to run?

It's analogous to '_' in patterns: a kind of anonymous type variable
that you can use to avoid giving a name to a type. (As with "_" in
patterns, there"s no connection between occurrences of "_", so "_ *
int -> _" means "'a * int -> 'b", not "'a * int -> 'a", for example.)

It's not doing anything special here: you could equally give a name to
the type without changing the meaning of the code.

> Could your example be written without a record/object type using
> polymorphic type annotations for functions?

I don't believe it's possible to make function arguments polymorphic
using annotations. However, the code can be significantly simplified
to remove that bit of polymorphism altogether. As written it mixes
two techniques for hiding the type index in the expression GADT during
parsing: CPS (in the inner 'parse' function) and an existential type
(in the return type of 'parse_expr'). In fact, either of these
approaches in isolation is sufficient. Here's a more direct
implementation using only the existential:

(* Well-typed parser. Incomplete -- it doesn't handle fst and snd -- and a

bit careless about error-checking. Perhaps sufficient to give a flavour.
*)
let parse_expr : string -> any_expr =

let rec parse s pos =
match s.[pos] with
| 'T' -> pos + 1, Expr True
| 'F' -> pos + 1, Expr False
| '!' -> let pos', Expr e = parse s (pos + 1) in

(* Check that 'e' has boolean type before we can parse it to
Not. This is more than just good practice: without the
type-checking step the parser won't compile. *)

begin match type_of e with
| TBool -> pos', Expr (Not e)

| t -> typing_failure (pos + 1) pos' s TBool t
end

| '(' -> let pos, Expr l = parse s (pos + 1) in

if s.[pos] <> ',' then parsing_failure pos ',' s else

let pos, Expr r = parse s (pos + 1) in

if s.[pos] <> ')' then parsing_failure pos ')' s else

pos + 1, Expr (Pair (l, r))
in
fun s -> snd (parse s 0)