caml-list - the Caml user's mailing list
 help / Atom feed
From: Malcolm Matalka <mmatalka@gmail.com>
To: Ivan Gotovchits <ivg@ieee.org>
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 10:49:59 +0100
Message-ID: <86wo9zljy0.fsf@gmail.com> (raw)
In-Reply-To: <CALdWJ+wh0zWbv2ejzeFFPahbY0DKqMW8VJBYkeNSZzuAtSw3-Q@mail.gmail.com>

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

> as
>
>    let x,y : string * int = map2 (bad_id ()) "hello", 42
>
> and will get a segmentation fault, as `y` will now have type int but hold a
> string.
>
> And here comes the syntax as a savior as it lets us specify functions that
> are guaranteed to be syntactic values. Indeed, all three solutions
> syntactically guarantee that the provided argument is a function, not a
> closure. Indeed, let's introduce the universal identity via a record,
>
>    type id = { f : 'a. 'a -> 'a}
>
> and we can see that our `bad_id` is not accepted due to the value
> restriction, while good_id, defined as,
>
>    let good_id x = x
>
> is perfectly fine, e.g.,
>
>   let id1 = {f = good_id} (*accepted *)
>   let id2 = {f = bad_id}   (* rejected *)
>
> moreover, even a fine, but not syntactic, identity is also rejected
>
>   let fine_id () x = x
>   let id3 = {f = fine_id ()} (* rejected *)
>
> with the message
>
>   This field value has type 'b -> 'b which is less general than 'a. 'a -> 'a
>

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?

  reply index

Thread overview: 7+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2020-01-07 19:25 rixed
2020-01-07 20:20 ` Ivan Gotovchits
2020-01-08  6:55   ` rixed
2020-01-08  9:44     ` Jacques Garrigue
2020-01-08 20:32     ` Ivan Gotovchits
2020-01-10  9:50       ` Malcolm Matalka [this message]
2020-01-10 19:51         ` Ivan Gotovchits

Reply instructions:

You may reply publically 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=86wo9zljy0.fsf@gmail.com \
    --to=mmatalka@gmail.com \
    --cc=caml-list@inria.fr \
    --cc=ivg@ieee.org \
    --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

caml-list - the Caml user's mailing list

Archives are clonable: git clone --mirror https://inbox.ocaml.org/caml-list

AGPL code for this site: git clone https://public-inbox.org/ public-inbox