[Caml-list] what does let () = ... define?

[Caml-list] what does let () = ... define?

[Mr. Herr]

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

Hi,

in a small presentation of OCaml (Linux User Group Bremen) I got some interesting
questions, and
trying to answer I noticed I took something for granted that was not fully understood.

Looking at this in the toplevel:

# let () = () ;;
# () ;;
- : unit = ()
# let _ = () ;;
- : unit = ()
# let None = None;;
Warning 8: this pattern-matching is not exhaustive.
Here is an example of a value that is not matched:
Some _
#

... the question is: okay, pattern matching left of the equal sign, but what does it
define?
It defines unit and None in the environment, and then that value is just sitting there?

/Str.

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

Re: [Caml-list] what does let () = ... define?

[Nick Lucaroni]

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

Pattern matching left of the = sign is helpful for tuple, records and
destructuring variant types with a single constructors.

# let (x,y) = (1,2);;
> val x : int = 1
> val y : int = 2
> # type r = { x : int; y : int; };;
> type r = { x : int; y : int; }
> # let {x=a;y=b} = {x=1;y=2};;
> val a : int = 1
>
>> val b : int = 2
>
> # let {x=a} = {x=1;y=2};;
>
> val a : int = 1
>
# type point = Point of int * int;;
> type point = Point of int * int
> # let Point (x,_) = Point(1,2);;
> val x : int = 1
>

--
nL

On Fri, Mar 18, 2016 at 2:04 PM, Mr. Herr <misterherr@freenet.de> wrote:

> Hi,
>
> in a small presentation of OCaml (Linux User Group Bremen) I got some
> interesting questions, and
> trying to answer I noticed I took something for granted that was not fully
> understood.
>
> Looking at this in the toplevel:
>
> # let () = () ;;
> # () ;;
> - : unit = ()
> # let _ = () ;;
> - : unit = ()
> # let None = None;;
> Warning 8: this pattern-matching is not exhaustive.
> Here is an example of a value that is not matched:
> Some _
> #
>
> ... the question is: okay, pattern matching left of the equal sign, but
> what does it define?
> It defines unit and None in the environment, and then that value is just
> sitting there?
>
> /Str.
>

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

Re: [Caml-list] what does let () = ... define?

[Christoph Höger]

It defines a match-expression with a single case, that is why you get
the warning on None.

In case of let () = ..., everything is fine, since unit has exactly one
constructor (that is, how unit is defined, btw.). You could also have
written let my_unit = ..., but since my_unit = () (even == (), I think),
you do not gain anything from this variable (and hopefully the compiler
gets rid of it). In order to provide more readable and safe code, you
should thus use the ()-syntax (since now everyone, including the
typechecker sees that the rhs is intended to yield unit). The same holds
for records, tuples etc. think of it as a shallow and cheap type annotation.

regards,

Christoph

Am 18.03.2016 um 19:04 schrieb Mr. Herr:
> Hi,
> 
> in a small presentation of OCaml (Linux User Group Bremen) I got some
> interesting questions, and
> trying to answer I noticed I took something for granted that was not
> fully understood.
> 
> Looking at this in the toplevel:
> 
> # let () = () ;;
> # () ;;
> - : unit = ()
> # let _ = () ;;
> - : unit = ()
> # let None = None;;
> Warning 8: this pattern-matching is not exhaustive.
> Here is an example of a value that is not matched:
> Some _
> #
> 
> ... the question is: okay, pattern matching left of the equal sign, but
> what does it define?
> It defines unit and None in the environment, and then that value is just
> sitting there?
> 
> /Str.


-- 
Christoph Höger

Technische Universität Berlin
Fakultät IV - Elektrotechnik und Informatik
Übersetzerbau und Programmiersprachen

Sekr. TEL12-2, Ernst-Reuter-Platz 7, 10587 Berlin

Tel.: +49 (30) 314-24890
E-Mail: christoph.hoeger@tu-berlin.de

Re: [Caml-list] what does let () = ... define?

[Nicolas Barnier]

Le 18/03/2016 19:52, Christoph Höger a écrit :
> It defines a match-expression with a single case, that is why you get
> the warning on None. [...]
> The same holds
> for records, tuples etc. think of it as a shallow and cheap type annotation.

Indeed. And it is quite a common idiom to write the equivalent of a "main"
function at the end of a source file as the last called function of your
program shouldn't return any useful value, for example :

let () =
   let x = int_of_string Sys.argv.(1) in
   solve x

It's better practice than to write :

let _ =
   ...

because it can catch some type error that would silently pass with
the latter: suppose you finally decide to add a parameter to the
solve function (let solve = fun x y -> ...), if you forget to add
the argument to the call to solve in the main function, in the first
case you get a type error, but your program compiles and just does
nothing in the second case (_ matches with a partial application of
solve).

Regards,

-- Nicolas

Re: [Caml-list] what does let () = ... define?

[octachron]

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

Hi,

Maybe defining is not the right word here. An alternative explanation 
would be that "let" binds variables in the pattern on the left in order 
to match the expression on the right. For instance, the following exotic 
expression:

# type alt = Left of int | Right of int
# let (Left a|Right a) = Left 0;;
- : val a: int

is valid and binds the variable "a" to the value 0.

Since there is no variable to be bound in "()" or any constructor 
without argument,

#let () = ();;

just computes the expression on the right and does not bind anything on 
the left.

Note that in some way, the toplevel is already telling you that, since

# let () = ();;

has no output compared to

# ();;
  - : unit = ()

which prints the value of the constructor ().

− octachron


Le 03/18/16 19:04, Mr. Herr a écrit :
> Hi,
>
> in a small presentation of OCaml (Linux User Group Bremen) I got some 
> interesting questions, and
> trying to answer I noticed I took something for granted that was not 
> fully understood.
>
> Looking at this in the toplevel:
>
> # let () = () ;;
> # () ;;
> - : unit = ()
> # let _ = () ;;
> - : unit = ()
> # let None = None;;
> Warning 8: this pattern-matching is not exhaustive.
> Here is an example of a value that is not matched:
> Some _
> #
>
> ... the question is: okay, pattern matching left of the equal sign, 
> but what does it define?
> It defines unit and None in the environment, and then that value is 
> just sitting there?
>
> /Str.


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

Re: [Caml-list] what does let () = ... define?

[Stefan Monnier]

> ... the question is: okay, pattern matching left of the equal sign,
> but what does it define?  It defines unit and None in the environment,
> and then that value is just sitting there?

    let <pat> = <exp1> in <exp2>

is basically syntactic sugar for

    match <exp1> with <pat> => <exp2>


-- Stefan

Re: [Caml-list] what does let () = ... define?

[Raphaël Proust]

On 18 March 2016 at 18:04, Mr. Herr <misterherr@freenet.de> wrote:
> in a small presentation of OCaml (Linux User Group Bremen) I got some
> interesting questions, and
> trying to answer I noticed I took something for granted that was not fully
> understood.
>
> Looking at this in the toplevel:
>
> # let () = () ;;
> # () ;;
> - : unit = ()
> # let _ = () ;;
> - : unit = ()

The specific case of `let () = …` I would consider to be equivalent to
`let (_ : unit) = …`. I.e., it doesn't bind anything in the
environment; it runs something (the right hand-side of the `=`); it
constrains the result to be of type `unit`.


> # let None = None;;
> Warning 8: this pattern-matching is not exhaustive.
> Here is an example of a value that is not matched:
> Some _
> #
>
> ... the question is: okay, pattern matching left of the equal sign, but what
> does it define?

In this case, nothing. Nothing is “defined” by your pattern matching.
There is just a check that the expression on the right-hand-side of
`=` matches the form on the left-hand-side. In the case of `()` that
check is trivial and is guaranteed to succeed by the type checker. In
the case of `None`, the type checker can't make any guarantees about
`None` being exhaustive; hence the warning.


> It defines unit and None in the environment, and then that value is just
> sitting there?

To be clear, it does NOT define unit nor None in the environment. Both
`()` and `None` are constructors (in this case, destructors). They are
not variables that can be introduced in the environment.

The form `let None = <some_expr> in <some_term>` is equivalent to
`match <some_expr> with None -> <some_term>` which gives a warning
because `None` is not the only case for the option type. (The
exhaustiveness check relies on typing.)

Generally, you can transform most (all?) `let` into `match` using the
correspondence above: `let <some_pattern> = <some_expr> in
<some_term>` into `match <some_expr> with <some_pattern> ->
<some_term>`. The former form is limited to one pattern (which is not
useful in some situations).

Note that using a pattern more complex than a simple variable on the
left-hand-side of a let-binding is often useful.
- for destructing tuples (`let (x,y) = <some_expr> in`) or records
(`let {foo; bar} = <some_expr> in`)
- for enforcing typing constraints (`let (_ : baz) = <some_expr> in`)
- for extracting an element that is present in every part of a sum
(`let (A (pos, _, _) | B (pos, _) | C pos) = <some_expr> in`)
- probably some other things I can't think of right now.

-- r

Re: [Caml-list] what does let () = ... define?

[Mr. Herr]

see below

/Str.

On 18.03.2016 22:29, Raphaël Proust wrote:
> On 18 March 2016 at 18:04, Mr. Herr <misterherr@freenet.de> wrote:
>> in a small presentation of OCaml (Linux User Group Bremen) I got some
>> interesting questions, and
>> trying to answer I noticed I took something for granted that was not fully
>> understood.
>>
>> Looking at this in the toplevel:
>>
>> # let () = () ;;
>> # () ;;
>> - : unit = ()
>> # let _ = () ;;
>> - : unit = ()
> The specific case of `let () = …` I would consider to be equivalent to
> `let (_ : unit) = …`. I.e., it doesn't bind anything in the
> environment; it runs something (the right hand-side of the `=`); it
> constrains the result to be of type `unit`.
>
>
>> # let None = None;;
>> Warning 8: this pattern-matching is not exhaustive.
>> Here is an example of a value that is not matched:
>> Some _
>> #
>>
>> ... the question is: okay, pattern matching left of the equal sign, but what
>> does it define?
> In this case, nothing. Nothing is “defined” by your pattern matching.
> There is just a check that the expression on the right-hand-side of
> `=` matches the form on the left-hand-side. In the case of `()` that
> check is trivial and is guaranteed to succeed by the type checker. In
> the case of `None`, the type checker can't make any guarantees about
> `None` being exhaustive; hence the warning.
>
>
>> It defines unit and None in the environment, and then that value is just
>> sitting there?
> To be clear, it does NOT define unit nor None in the environment. Both
> `()` and `None` are constructors (in this case, destructors). They are
> not variables that can be introduced in the environment.
>
> The form `let None = <some_expr> in <some_term>` is equivalent to
> `match <some_expr> with None -> <some_term>` which gives a warning
> because `None` is not the only case for the option type. (The
> exhaustiveness check relies on typing.)
>
> Generally, you can transform most (all?) `let` into `match` using the
> correspondence above: `let <some_pattern> = <some_expr> in
> <some_term>` into `match <some_expr> with <some_pattern> ->
> <some_term>`. The former form is limited to one pattern (which is not
> useful in some situations).
Looks like we are getting near to what I was trying to ask about. So the question
seems to be:
what is the result of successful pattern matching?

OCaml is the language for Coq, to prove properties of programs, and I am asking, what
is the result of

let None = None ;;

and where does this result go? None evaluates to None, is pattern matched to None,
and then QED?

> Note that using a pattern more complex than a simple variable on the
> left-hand-side of a let-binding is often useful.
> - for destructing tuples (`let (x,y) = <some_expr> in`) or records
> (`let {foo; bar} = <some_expr> in`)
> - for enforcing typing constraints (`let (_ : baz) = <some_expr> in`)
> - for extracting an element that is present in every part of a sum
> (`let (A (pos, _, _) | B (pos, _) | C pos) = <some_expr> in`)
> - probably some other things I can't think of right now.
I knew I would get hints about this ;-)