[Caml-list] More existential escapes (or possibly first class polymorphism)

[Caml-list] More existential escapes (or possibly first class polymorphism)

[David Allsopp]

Daniel's recent thread inspired to revisit a recent problem I'd had but had
given up on, with a most inelegant solution. Although what I have no is much
less inelegant, I'm wondering if it can be improved further by a trick or
some such which I can't spot.

I have a GADT containing keys where the type parameter denotes the value
type (my actual use case has many more constructors):

type _ token = Block : int -> string token
             | Role : string -> unit token

and I then want to be able to store these in a structure where I can look
them up by token value. So I define:

type binding = B : ('a token * 'a) -> token

to store a binding and:

type (_, _) eq = Eq : ('a, 'a) eq

let test_key (type r) (type s) (r : r token) (s : s token) : (r, s) eq
option =
  match (r, s) with
    (Role r, Role s) when r = s ->
      Some Eq
  | (Block r, Block s) when r = s ->
      Some Eq
  | _ ->
      None

and so I can define [find] in a manner very like Daniel's in
https://sympa.inria.fr/sympa/arc/caml-list/2015-03/msg00109.html

Given that this application is for a specific set of keys, rather than for a
universal type, I'd quite like to define [iter], which is where I've hit a
bit of inelegance:

let iter f script =
  let rec iter = function
    binding::script ->
      f binding;
      iter script
  | [] ->
      ()
  in
    iter script

but this means that the function passed needs to match on type binding,
which I'd prefer to be hidden:

let f = function
  B(Role role, ()) ->
    Printf.printf "Role %s\n%!" role
| B(Block n, code) ->
    Printf.printf "Block %d\n%!" n code

Is there a way to write [iter] such that it has signature [('a token -> 'a
-> unit) -> binding list -> unit]?

My closest attempt so far is to start with:

let iter f script =
  let rec iter = function
    B(key, binding)::script ->
      f key binding;
      iter script
  | [] ->
      ()
  in
    iter script

which obviously doesn't work because the type of [key] and [binding] in
[iter] escape their scope. Now, if my understanding is correct, the problem
here isn't so much that the existentials escape their scope, but that [f] is
monomorphic. So, if I define a record type:

type f = {f : 'a . 'a token -> 'a -> unit}

then I can alter the definition of iter to allow a polymorphic function to
be passed

let iter {f} script =
  ...

and I can get to a version of [iter] where the functions don't need to know
about the internals of type binding, but they do need to be passed wrapped
up as {f: foo}.

Is there some other wizardry on offer which can allow the polymorphic nature
of [f] to be inferred?


David

Re: [Caml-list] More existential escapes (or possibly first class polymorphism)

[Jeremy Yallop]

On 20 March 2015 at 16:29, David Allsopp <dra-news@metastack.com> wrote:
> Is there some other wizardry on offer which can allow the polymorphic nature
> of [f] to be inferred?

Unfortunately not.  OCaml doesn't infer polymorphic types for function
parameters.

RE: [Caml-list] More existential escapes (or possibly first class polymorphism)

[David Allsopp]

Jeremy Yallop wrote:
> On 20 March 2015 at 16:29, David Allsopp <dra-news@metastack.com> wrote:
> > Is there some other wizardry on offer which can allow the polymorphic
> > nature of [f] to be inferred?
> 
> Unfortunately not.  OCaml doesn't infer polymorphic types for function
> parameters.

Thanks - it's useful to know to stop looking :o)

Is there an unsoundness reason why there isn't a type annotation which can allow it be specified, rather than inferred, that a function argument is polymorphic? Or is that the "purity" of wanting the type system of the core language to be inferable?


David

Re: [Caml-list] More existential escapes (or possibly first class polymorphism)

[Gabriel Scherer]

> Is there an unsoundness reason why there isn't a type annotation which can allow it be specified,
> rather than inferred, that a function argument is polymorphic?
> Or is that the "purity" of wanting the type system of the core language to be inferable?

The latter: inferrible potentially-polymorphic arguments without
requiring any kind of annotation is undecidable. Various systems exist
which require you to add some annotations in some places, but it's
rather delicate to know where annotations are necessary, and which
kind of principality properties you can expect from the inference
process.

In OCaml, you have to annotate each polymorphic use of a function
parameter (not the abstraction site itself), and that is done by the
explicit projection with a field name having polymorphic type.



On Sun, Mar 22, 2015 at 12:20 PM, David Allsopp <dra-news@metastack.com> wrote:
> Jeremy Yallop wrote:
>> On 20 March 2015 at 16:29, David Allsopp <dra-news@metastack.com> wrote:
>> > Is there some other wizardry on offer which can allow the polymorphic
>> > nature of [f] to be inferred?
>>
>> Unfortunately not.  OCaml doesn't infer polymorphic types for function
>> parameters.
>
> Thanks - it's useful to know to stop looking :o)
>
> Is there an unsoundness reason why there isn't a type annotation which can allow it be specified, rather than inferred, that a function argument is polymorphic? Or is that the "purity" of wanting the type system of the core language to be inferable?
>
>
> David
>
> --
> 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