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)`