[Caml-list] GADT and weak polymorphism

[Caml-list] GADT and weak polymorphism

[Runhang Li]

Hi, camels

Consider the following module:

    module HList = struct

      type (_, _) hlist =
        | Empty : ('a, 'a) hlist
        | Cons  : 'c * ('a, 'b) hlist -> ('c -> 'a, 'b) hlist

      let cons : type a b c. c -> (a, b) hlist -> (c -> a, b) hlist =
        fun h tl -> Cons (h, tl)

      let empty = Empty

      let ( **> ) = cons

      let l = '2' **> "str" **> empty

    end

The type of ``l`` is ``(char -> string -> ‘_a, ‘_a) hlist``. I would like to know the reason that weak polymorphism shows up here.

Thank you


Kindly,

Runhang

Re: [Caml-list] GADT and weak polymorphism

[Gabriel Scherer]

[-- Attachment #1: Type: text/plain, Size: 2400 bytes --]

Hi Runhang,

There is an interaction between two advanced aspects of the OCaml language:

1. The relation between (non)-covariance and (non)-generalization of type
variables due to the "relaxed value restriction"

https://www.reddit.com/r/ocaml/comments/t8g2e/pdf_relaxing_the_value_restriction_by_jacques/
    http://caml.inria.fr/pub/papers/garrigue-value_restriction-fiwflp04.pdf
2. The difficult analysis of variance of GADT parameters
    https://sympa.inria.fr/sympa/arc/caml-list/2012-02/msg00059.html
    https://hal.inria.fr/hal-00772993

There is no simple way to solve any of these questions, so I don't expect
the OCaml language to improve on your example on the short/medium term.
After thinking of these issues a bit more, I would personally support
adding a notion of "pure arrow" ('a => 'b), giving your interface the type
  ( **> ) : 'c => ('a, 'b) hlist => ('c -> 'a, 'b) hlist
which would make any term built solely of ( **> ) and empty (and Empty and
Cons) generalizable. However, this feature would be very limited in scope
(due to the inherent difficulty of tracking effect) and suitable
generalization require advanced type system features (effect systems, for
example as found in Koka or F*). I think a minimal, advanced-uses-only
feature (just a separation of pure and impure arrow) would already be a
nice feature to have (also for functors), but there is no clear consensus
on the question.

On Tue, Nov 17, 2015 at 7:14 PM, Runhang Li <runhang@posteo.net> wrote:

> Hi, camels
>
> Consider the following module:
>
>     module HList = struct
>
>       type (_, _) hlist =
>         | Empty : ('a, 'a) hlist
>         | Cons  : 'c * ('a, 'b) hlist -> ('c -> 'a, 'b) hlist
>
>       let cons : type a b c. c -> (a, b) hlist -> (c -> a, b) hlist =
>         fun h tl -> Cons (h, tl)
>
>       let empty = Empty
>
>       let ( **> ) = cons
>
>       let l = '2' **> "str" **> empty
>
>     end
>
> The type of ``l`` is ``(char -> string -> ‘_a, ‘_a) hlist``. I would like
> to know the reason that weak polymorphism shows up here.
>
> Thank you
>
>
> Kindly,
>
> Runhang
>
>
> --
> 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

[-- Attachment #2: Type: text/html, Size: 3702 bytes --]

Re: [Caml-list] GADT and weak polymorphism

[Jonas Jensen]

I was asked the same question and found the following stackoverflow
discussion in which two possible remedies are suggested:
http://stackoverflow.com/questions/25025091/ocaml-formatters-and-value-restriction.

Jeffrey Scofield suggests changing your ``l`` to

    let l () = '2' **> "str" **> empty

Leo White suggests writing ``l`` so that it's a value rather than an
expression. In your case, you'd write:

    module HList = struct
      type (_, _) hlist =
        | Empty : ('a, 'a) hlist
        | ::  : 'c * ('a, 'b) hlist -> ('c -> 'a, 'b) hlist

      let empty = Empty

      let l = '2' :: "str" :: empty
    end

I believe that ``::`` is the only infix constructor name in OCaml, so
you have to shadow standard list cons in the module of hlist to make
this work.

In the new ocaml-amqp library, we chose the latter remedy. See the
full result here:
https://github.com/andersfugmann/ocaml-amqp/blob/790486dad/src/amqp_protocol.ml#L197

Cheers,
Jonas

On 17 November 2015 at 19:14, Runhang Li <runhang@posteo.net> wrote:
> Hi, camels
>
> Consider the following module:
>
>     module HList = struct
>
>       type (_, _) hlist =
>         | Empty : ('a, 'a) hlist
>         | Cons  : 'c * ('a, 'b) hlist -> ('c -> 'a, 'b) hlist
>
>       let cons : type a b c. c -> (a, b) hlist -> (c -> a, b) hlist =
>         fun h tl -> Cons (h, tl)
>
>       let empty = Empty
>
>       let ( **> ) = cons
>
>       let l = '2' **> "str" **> empty
>
>     end
>
> The type of ``l`` is ``(char -> string -> ‘_a, ‘_a) hlist``. I would like to know the reason that weak polymorphism shows up here.
>
> Thank you
>
>
> Kindly,
>
> Runhang
>
>
> --
> 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