[Caml-list] GADT in an optional parameter

[Caml-list] GADT in an optional parameter

[David Allsopp]

So, continuing my forays into sections of type theory I clearly don't
properly understand! Although I was trying to use it for something else, my
problem here is equivalent to a rather over-discussed problem on this list -
namely, raising exceptions vs wrapping results in 'a option

I defined the following GADT:

type ('a, 'b) wrap = Option : ('a, 'a option) wrap
                   | Exn : ('a, 'a) wrap

I then created the following alternate implementation of Map where find
takes that GADT as its first parameter:

module StringMap =
  struct
    include Map.Make(String)

    let find : type s t . (s, t) wrap -> string -> s Map.Make(String).t -> t
= fun mode key map ->
      match mode with
        Exn ->
          find key map
      | Option ->
          try
            Some (find key map)
          with Not_found -> None
  end

So far so good, as we can have:

StringMap.find Option "foo" StringMap.empty;; (* None *)
StringMap.find Exn "foo" StringMap.empty;;    (* Not_found raised *)

which is quite nice (ignoring any quite optimisable and probably negligible
overhead of the extra match clause verses having two functions find and
find_option).

I then wanted to try to make the first parameter optional, defaulting to Exn
(so you'd get the vanilla behaviour of Map.find):

module StringMap =
  struct
    include Map.Make(String)

    let find : type s t . ?mode:(s, t) wrap -> string -> s
Map.Make(String).t -> t = fun ?(mode = Exn) key map ->
      match mode with
        Exn ->
          find key map
      | Option ->
          try
            Some (find key map)
          with Not_found -> None
  end

But I get: This expression has type (s, s) wrap but an expression was
expected of type (s, t) wrap on the Exn default value.

Now, in my woolly way, I thought that the default value for an optional
parameter behaved /almost/ like syntactic sugar, but clearly not. Is there a
way to annotate this to achieve what I'm after? 


David 

Re: [Caml-list] GADT in an optional parameter

[Jacques Garrigue]

On 2013/07/18, at 23:03, David Allsopp <dra-news@metastack.com> wrote:

> I then wanted to try to make the first parameter optional, defaulting to Exn
> (so you'd get the vanilla behaviour of Map.find):
> 
> module StringMap =
>  struct
>    include Map.Make(String)
> 
>    let find : type s t . ?mode:(s, t) wrap -> string -> s
> Map.Make(String).t -> t = fun ?(mode = Exn) key map ->
>      match mode with
>        Exn ->
>          find key map
>      | Option ->
>          try
>            Some (find key map)
>          with Not_found -> None
>  end
> 
> But I get: This expression has type (s, s) wrap but an expression was
> expected of type (s, t) wrap on the Exn default value.
> 
> Now, in my woolly way, I thought that the default value for an optional
> parameter behaved /almost/ like syntactic sugar, but clearly not. Is there a
> way to annotate this to achieve what I'm after? 

No, clearly no.
Optional arguments have no impact on typing: the absence of an optional
argument cannot force some extra equation.
I agree this would be interesting, but then we would need a way to express
it in the type. Otherwise, why would the user expect (s=t) when there is no
argument, whereas there is no way to see what the default is?
Something like:
val  find : ?mode:(('s,'t) wrap = Exn) -> string -> 's Map.Make(String).t -> 't

It would be good to see whether this has many applications.
In the past, there were some request to be able to default to the identity function.

	Jacques

Re: [Caml-list] GADT in an optional parameter

[oleg]

> Now, in my woolly way, I thought that the default value for an optional
> parameter behaved /almost/ like syntactic sugar, but clearly not. Is there a
> way to annotate this to achieve what I'm after? 

Actually a default parameter is syntactic sugar. When the type checker
sees

        fun ?(p=v) -> body

it essentially macro-expands the expression to the following

   fun xxOpt -> let p = match xxOpt with
                         | Some xxSth -> xxSth
                         | None       -> v
                in body
and then type checks the resulting macro-expansion. Here xxOpt and
xxSth are internally generated identifiers with funky names (the type
checker is fond of generating funny identifiers, especially when
dealing with objects). You can see this expansion process for yourself,
typing/typecore.ml; search for the line

  | Pexp_function (l, Some default, [spat, sbody]) ->

If you apply this expansion to your function

> let find : type s t . 
>     ?mode:(s, t) wrap -> string -> s Map.Make(String).t -> t = 
>  fun ?(mode = Exn) key map ->

you will see the error right away. Let's take a simpler GADT for clarity

    type _ g = 
      | Int : int -> int g 
      | Str : string -> string g
    ;;

and write a consumer of GADT values (which pattern-matches on them)

    let g_consumer : type a. a g -> string = function
      | Int x -> string_of_int x
      | Str x -> x
    ;;

This is a polymorphic function: it can handle data of the type
[int g] and [string g]:

    g_consumer (Int 1);;
    g_consumer (Str "str");;

Let us attempt to write a producer:

let g_producer1 : type a. a g = Int 1;;

we immediately get an error:

  let g_producer1 : type a. a g = Int 1;;
                                  ^^^^^
Error: This expression has type int g but an expression was expected of type
         a g


Although we may consume either [int g] or [string g], we can produce
only one of them. Likewise,
        fun x -> match x with
                   true ->  Int 1
                 | false -> Str "str"
;;
fails similarly.


If we desugar the original example with the optional parameter, we get
something like

        let mode = match xxOpt with
                 | Some x -> x
                 | None   -> Int 1

the parameter mode is supposed to be polymorphic, [a g], but the match
expression, which produces GADT, cannot produce the polymorphic GADT
type. If we see Int 1, then result must be [int g]. 

Again, a function that pattern-matches on GADT can be polymorphic. A
function/expression that _produces_ GADT (that is, uses GADT
constructors to produce values) cannot be polymorphic in the resulting
GADT.

Re: [Caml-list] GADT in an optional parameter

[Alain Frisch]

On 07/19/2013 08:59 AM, Jacques Garrigue wrote:
> val  find : ?mode:(('s,'t) wrap = Exn) -> string -> 's Map.Make(String).t -> 't
>
> It would be good to see whether this has many applications.

The idea would be to have a different kind of optional argument, which 
specifies as part of the function type an expression to be expanded 
syntactically on the call site when the argument is not provided 
explicitly.  (In your example, the Exn constructor would need to be 
available from the call site.  -- Or do you interpret "Exn" as a typed 
reference to the Exn constructor on the value declaration site?)

If we assume that the "default" can be an arbitrary "parse tree" 
(untyped) expression, I guess that type equality would require these 
expressions to be strictly equal (modulo locations).

This could have several interesting usages:

   - Passing the "identity" function as a continuation, or a GADT to 
customize the return type.

   - Implicit arguments, capturing an identifier from the scope of the 
call site:


      let rec eval ??(env = env) x =
      ...
        | ... -> eval y  (* pass "env" implicitly *)
        | ... -> eval env' z


   - Implement the implicit passing of "runtime type representations":

       let variant ??(t : 'a ty = (type of _)) (x : 'a) = ....

     or of values synthesized by -ppx rewriters on the call site:

       let debug ??(loc = [%self_loc]) x =
         Format.eprintf "%a %s@." pp_loc loc x

     (this uses the syntax of extension nodes in the extension_points 
branch, and assumes that the call site will be processed with a -ppx 
rewriter which substitutes a value representing the current location in 
the source code for the [%self_loc] extension node.)


Alain

Re: [Caml-list] GADT in an optional parameter

[Gabriel Scherer]

Another option could be to keep a non-desugaring explanation of
optional arguments, but used a GADT type carrying more static
information than ('a option). Something like:

  type ('default, _) rich_option =
    | RSome : 'a -> ('default, 'a) rich_option
    | RNone : ('default, 'default) rich_option

  let default : type def s . def -> (def, s) rich_option -> s = fun
def -> function
    | RNone -> def
    | RSome v -> v

If optional keywords desugared to rich_option instead of option, we
could maybe (I haven't tested) write something like

  let find_mode : type s t . (s, t) wrap -> (s -> bool) -> s list -> t
= fun mode p li ->
    match mode with
      | Exn -> List.find p li
      | Option -> try Some (List.find p li) with Not_found -> None

  let find : type s t . ?mode:(((s,s) wrap, (s,t) wrap) rich_option)
-> (s -> bool) -> s list -> t =
    fun ?mode p li -> find_mode (default Exn mode) p li

Remark: The OCaml syntax for optional argument uses ?mode:'a rather
than ?mode:('a option), talking of the value type instead of the
option type. This isn't possible anymore with rich_option whose type
cannot be deduced from its second parameter, and arguably using
?mode:('a option) would make slightly clearer the type of "mode" in
the call (f ?mode ...).

On Fri, Jul 19, 2013 at 12:37 PM, Alain Frisch <alain@frisch.fr> wrote:
> On 07/19/2013 08:59 AM, Jacques Garrigue wrote:
>>
>> val  find : ?mode:(('s,'t) wrap = Exn) -> string -> 's Map.Make(String).t
>> -> 't
>>
>> It would be good to see whether this has many applications.
>
>
> The idea would be to have a different kind of optional argument, which
> specifies as part of the function type an expression to be expanded
> syntactically on the call site when the argument is not provided explicitly.
> (In your example, the Exn constructor would need to be available from the
> call site.  -- Or do you interpret "Exn" as a typed reference to the Exn
> constructor on the value declaration site?)
>
> If we assume that the "default" can be an arbitrary "parse tree" (untyped)
> expression, I guess that type equality would require these expressions to be
> strictly equal (modulo locations).
>
> This could have several interesting usages:
>
>   - Passing the "identity" function as a continuation, or a GADT to
> customize the return type.
>
>   - Implicit arguments, capturing an identifier from the scope of the call
> site:
>
>
>      let rec eval ??(env = env) x =
>      ...
>        | ... -> eval y  (* pass "env" implicitly *)
>        | ... -> eval env' z
>
>
>   - Implement the implicit passing of "runtime type representations":
>
>       let variant ??(t : 'a ty = (type of _)) (x : 'a) = ....
>
>     or of values synthesized by -ppx rewriters on the call site:
>
>       let debug ??(loc = [%self_loc]) x =
>         Format.eprintf "%a %s@." pp_loc loc x
>
>     (this uses the syntax of extension nodes in the extension_points branch,
> and assumes that the call site will be processed with a -ppx rewriter which
> substitutes a value representing the current location in the source code for
> the [%self_loc] extension node.)
>
>
> Alain
>
>
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa.inria.fr/sympa/arc/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs

RE: [Caml-list] GADT in an optional parameter

[David Allsopp]

Thanks for replies on this!

Jacques Garrigue wrote:
> On 2013/07/18, at 23:03, David Allsopp <dra-news@metastack.com> wrote:
> 
> > I then wanted to try to make the first parameter optional, defaulting
> > to Exn (so you'd get the vanilla behaviour of Map.find):
> >
> > module StringMap =
> >  struct
> >    include Map.Make(String)
> >
> >    let find : type s t . ?mode:(s, t) wrap -> string -> s
> > Map.Make(String).t -> t = fun ?(mode = Exn) key map ->
> >      match mode with
> >        Exn ->
> >          find key map
> >      | Option ->
> >          try
> >            Some (find key map)
> >          with Not_found -> None
> >  end
> >
> > But I get: This expression has type (s, s) wrap but an expression was
> > expected of type (s, t) wrap on the Exn default value.
> >
> > Now, in my woolly way, I thought that the default value for an
> > optional parameter behaved /almost/ like syntactic sugar, but clearly
> > not. Is there a way to annotate this to achieve what I'm after?
> 
> No, clearly no.
> Optional arguments have no impact on typing: the absence of an optional
> argument cannot force some extra equation.
> I agree this would be interesting, but then we would need a way to express
> it in the type. Otherwise, why would the user expect (s=t) when there is
> no argument, whereas there is no way to see what the default is?
> Something like:
> val  find : ?mode:(('s,'t) wrap = Exn) -> string -> 's Map.Make(String).t
> -> 't

Yes, indeed - a head-crashing-into-the-desk moment!

> It would be good to see whether this has many applications.
> In the past, there were some request to be able to default to the identity
> function.

More follows, but both this and my actual application, in which many functions may return both a value and a list of messages but in many instances the messages can be ignored, are quite useful - but I concede that something which boils down to syntactic sugar is not too compelling an application!

oleg@okmij.org wrote:
> > Now, in my woolly way, I thought that the default value for an
> > optional parameter behaved /almost/ like syntactic sugar, but clearly
> > not. Is there a way to annotate this to achieve what I'm after?
> 
> Actually a default parameter is syntactic sugar. When the type checker
> sees
> 
>         fun ?(p=v) -> body
> 
> it essentially macro-expands the expression to the following
> 
>    fun xxOpt -> let p = match xxOpt with
>                          | Some xxSth -> xxSth
>                          | None       -> v
>                 in body

<snip>
 
> Again, a function that pattern-matches on GADT can be polymorphic. A
> function/expression that _produces_ GADT (that is, uses GADT constructors
> to produce values) cannot be polymorphic in the resulting GADT.

So if I understand correctly, what would be needed here would be a special case for dealing with optional arguments where the default is a GADT constructor.

Two ideas...

Alain Frisch wrote:
> On 07/19/2013 08:59 AM, Jacques Garrigue wrote:
> > val  find : ?mode:(('s,'t) wrap = Exn) -> string -> 's
> > Map.Make(String).t -> 't
> >
> > It would be good to see whether this has many applications.
> 
> The idea would be to have a different kind of optional argument, which
> specifies as part of the function type an expression to be expanded
> syntactically on the call site when the argument is not provided
> explicitly.  (In your example, the Exn constructor would need to be
> available from the call site.  -- Or do you interpret "Exn" as a typed
> reference to the Exn constructor on the value declaration site?)
> 
> If we assume that the "default" can be an arbitrary "parse tree"
> (untyped) expression, I guess that type equality would require these
> expressions to be strictly equal (modulo locations).

That seems very powerful, but presumably similarly hard? I'm guessing that at the moment the .cmi file doesn't contain any indication of whether an optional argument has a default or not (because it's an implementation detail transformed in the code as Oleg explained). Would that be a reasonably easy change to make? It feels very weird suddenly needing code to be included in a type! Or is this is a better halfway house...

Gabriel Scherer wrote:
> Another option could be to keep a non-desugaring explanation of optional
> arguments, but used a GADT type carrying more static information than ('a
> option). Something like:
> 
>   type ('default, _) rich_option =
>     | RSome : 'a -> ('default, 'a) rich_option
>     | RNone : ('default, 'default) rich_option
> 
>   let default : type def s . def -> (def, s) rich_option -> s = fun def ->
> function
>     | RNone -> def
>     | RSome v -> v

I'd experimented with something along these lines - I even tried seeing if redefining 'a option could trick the compiler, but it was not to be fooled!

> If optional keywords desugared to rich_option instead of option, we could
> maybe (I haven't tested) write something like
> 
>   let find_mode : type s t . (s, t) wrap -> (s -> bool) -> s list -> t =
> fun mode p li ->
>     match mode with
>       | Exn -> List.find p li
>       | Option -> try Some (List.find p li) with Not_found -> None
> 
>   let find : type s t . ?mode:(((s,s) wrap, (s,t) wrap) rich_option)
> -> (s -> bool) -> s list -> t =
>     fun ?mode p li -> find_mode (default Exn mode) p li
> 
> Remark: The OCaml syntax for optional argument uses ?mode:'a rather than
> ?mode:('a option), talking of the value type instead of the option type.
> This isn't possible anymore with rich_option whose type cannot be deduced
> from its second parameter, and arguably using ?mode:('a option) would make
> slightly clearer the type of "mode" in the call (f ?mode ...).

This seems quite nice. So, thinking of the syntax used for GADTs themselves we could have something like (note using equals instead of colon):

let find : type s t . ?mode = ((s, s) wrap, (s, t) wrap) rich_option -> (s -> bool) -> s list -> t = ...

with the requirement that the type used for an optional argument specified with equals instead of colon must have at least one constant constructor which should be used as the default. That feels as though it would be pretty easy for both type checking and implementation?

The final question is would one or both of these suggestions be likely to be made/accepted and, if so, is it worth opening a feature request in Mantis?


David

Re: [Caml-list] GADT in an optional parameter

[Alain Frisch]

On 07/25/2013 11:31 AM, David Allsopp wrote:
> Alain Frisch wrote:
>> The idea would be to have a different kind of optional argument, which
>> specifies as part of the function type an expression to be expanded
>> syntactically on the call site when the argument is not provided
>> explicitly.  (In your example, the Exn constructor would need to be
>> available from the call site.  -- Or do you interpret "Exn" as a typed
>> reference to the Exn constructor on the value declaration site?)
>>
>> If we assume that the "default" can be an arbitrary "parse tree"
>> (untyped) expression, I guess that type equality would require these
>> expressions to be strictly equal (modulo locations).
>
> That seems very powerful, but presumably similarly hard? I'm guessing that at the moment the .cmi file doesn't contain any indication of whether an optional argument has a default or not (because it's an implementation detail transformed in the code as Oleg explained). Would that be a reasonably easy change to make? It feels very weird suddenly needing code to be included in a type! Or is this is a better halfway house...

Indedd, it requires to store (untyped) parsetree fragments in types, 
which I'm sure will be considered as an abomination by most.  But from a 
technical point of view, I don't see any difficulty.

Alain