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

["Mr. Herr" <misterherr@freenet.de>]

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