Re: [Caml-list] GADT and weak polymorphism

[Gabriel Scherer <gabriel.scherer@gmail.com>]

[-- 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 --]