Re: [Caml-list] Problem with universal functions in a module

[Goswin von Brederlow <goswin-v-b@web.de>]

On Thu, Jan 08, 2015 at 09:45:47AM +0000, Ben Millwood wrote:
> Parametric polymorphic values in OCaml's type system can be thought of as
> "choose an assignment of the variables in this type, and you can use this
> value with that monomorphic type". But there's no monomorphic type that
> lets 'helper' do the right thing, so you actually need something more
> expressive than ordinary polymorphic types.
> 
> In Haskell there's higher-rank polymorphism, which in this case would look
> something like 'helper :: (forall a. T a -> b) -> Helper b', so that you
> could only pass sufficiently-polymorphic arguments to helper. However, as
> Jeremy said, there's a lot of added complexity involved.

In ocaml that is 'a . 'a -> 'b, or for GADTS: type a . a -> 'b.
The problem is the former is only allowed in records and objects, not
for function arguments and the later is only for annotating code and
not for signatures.


I don't see how there can be much added complexity involved. The
higher-rank polymorphism is already allowed in records and objects so
the type system knows how to deal with them. At least when they are
annotated. I wouldn't need ocaml to infere those types.

> On 7 January 2015 at 17:26, Jeremy Yallop <yallop@gmail.com> wrote:
> 
> > On 7 January 2015 at 13:50, Goswin von Brederlow <goswin-v-b@web.de>
> > wrote:
> > > Why are function arguments less general than their original function?
> >
> > Polymorphic arguments complicate type checking and make type inference
> > impossible, so OCaml doesn't allow them.
> >
> > > B) is there some way around this I'm not seeing?
> >
> > I don't think that there's any way of passing polymorphic arguments
> > that works out simpler than using a record.
> >
> > Of course, in your simple example code it's possible to eliminate the
> > GADT altogether, which would also eliminate the need for polymorphic
> > arguments.  Perhaps GADTs play a more essential role in your real
> > code, though.

The real use case has a GADT as input for a functor. The functor
defines the boxing, an equality and unbox_with_equal operation and
that helper record. Actually I have a few flavours of the same for
different input types: type 'a t, type ('a, 'b) t and GADTs with
detached witness: type 'a key + type 'a value and so on.

I wish I could make a generic helper record with

    type ('b, 'c) helper = { fn : 'a 'b -> 'c }

*sigh*

MfG
	Goswin