caml-list - the Caml user's mailing list
 help / color / mirror / Atom feed
From: Ivan Gotovchits <ivg@ieee.org>
To: Malcolm Matalka <mmatalka@gmail.com>
Cc: rixed@happyleptic.org, caml-list <caml-list@inria.fr>
Subject: Re: [Caml-list] Calling a single function on every member of a GADT?
Date: Fri, 10 Jan 2020 14:52:12 -0500	[thread overview]
Message-ID: <CALdWJ+yzfuqni2s_ZhMDhJU=-Jj7NfLtfHqoqGrD9NjBYRbD-Q@mail.gmail.com> (raw)
In-Reply-To: <86wo9zljy0.fsf@gmail.com>

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

On Fri, Jan 10, 2020 at 4:50 AM Malcolm Matalka <mmatalka@gmail.com> wrote:

> Thank you for the explanation Ivan.  I have two questions inline.
>
> Ivan Gotovchits <ivg@ieee.org> writes:
>
> > It has type `unit -> 'a -> 'a` therefore, if we would have the rank-1
> > polymorphism enabled for functions, we could apply it to the function
> >
> >      let map2 : fun ('a. 'a -> 'a) -> 'b -> 'c -> 'b * 'c = fun f (x,y)
> ->
> > f x, f y
>
> Small thing, but wouldn't the faux type be the following, based on your
> usage (making sure I'm following):
>
> fun ('a. 'a -> 'a) -> ('b * 'c) -> 'b * 'c
>

Yep, sure :) That's the problem with faux-typing)


> Why is type checking creating a record different than type checking a
> function argument?
>
> If we had the syntax (or something like it):
>
> let map2 : ('a. 'a -> 'a) -> ('b * 'c) -> ('b * 'c)
>
> Why would the type checker not be able to see that
>
> map2 good_id ("hi", 42)
>
> is valid but
>
> map2 (fine_id ()) ("hi", 32)
>
> is not, using the same logic that is verifying creating the "id" record
> is not valid?
>

I believe it is possible, as it is possible in Haskell (with RankNTypes and
ScopedTypeVariables). The main (theoretical) difference is that in OCaml we
need to check whether an expression is expansive and use a specialized
generalization in case if it is (for the relaxed value restriction). It
will, however, complicate the type inference engine a lot, but most
importantly, changing the typing rule of functions will have a tremendous
impact on the language. So this would be a very impractical solution.
Especially, since we don't have the mechanism of language extensions,
enabling RankNTypes will make a lot of programs untypeable, as they will
now require type annotations (recall that RankN is undecidable in general).
It could probably be implemented as a compiler command line parameter, like
`-rectypes` but this will be still quite impractical since more often code
like `fun f -> f 1, f true` is a programmer error, rather than a true
request for universal polymorphism (the same as with rectypes, recursive
types a more often an error rather than a deliberate attempt). Therefore,
enabling RankN(^1) polymorphism will type too many programs (not that it is
unsound, just many programs won't have sense) at the cost of even more
obscure type errors. On the other hand, we have three syntactic constructs
that let us express non-prenex polymorphism of the necessary rank(^2)
without breaking anything else. So it looks like a good deal - we can have
rankN polymorphism and decidable type checker at the same time. Just think
of polymorphic records/methods as an embedded DSL for rankN polymorphism.

============
Footnotes:

1) An important point, that I forgot to notice, is that enabling scoped
type variables, will inevitably enable rankN polymorphism, e.g., since now
any type could be a polytype, then suppose we have type `'a. ('b.'b -> 'a)
-> 'a` could be instantiated to 'a = 'd. ('c. ->  'd) -> 'd, so that our
type is now `'d. ('b. 'b -> ('c. 'c -> 'd) -> 'd) -> ('c. 'c -> 'd) -> 'd`
which is now rank3. Therefore, enabling arbitrary quantification in the
arrow type will lead to rankN and immediately make undecidable most of the
type checker.

2) We can craft arbitrary rank using records with universally quantified
type variables, e.g., here is an example of rank3 polymoprhism:

  type 'a rank1 = {f1 : 's. 's -> 'a}
  type 'a rank2 = {f2 : 'r. 'r -> 'a rank1}

Indeed, `f2` has type `'a.('r. 'r -> ('s. 's -> 'a)`

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

      reply	other threads:[~2020-01-10 19:51 UTC|newest]

Thread overview: 7+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2020-01-07 19:24 rixed
2020-01-07 20:21 ` Ivan Gotovchits
2020-01-08  6:54   ` rixed
2020-01-08  9:43     ` Jacques Garrigue
2020-01-08 20:32     ` Ivan Gotovchits
2020-01-10  9:49       ` Malcolm Matalka
2020-01-10 19:52         ` Ivan Gotovchits [this message]

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to='CALdWJ+yzfuqni2s_ZhMDhJU=-Jj7NfLtfHqoqGrD9NjBYRbD-Q@mail.gmail.com' \
    --to=ivg@ieee.org \
    --cc=caml-list@inria.fr \
    --cc=mmatalka@gmail.com \
    --cc=rixed@happyleptic.org \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).