From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00
	autolearn=unavailable autolearn_force=no version=3.4.4
Path: 
 eternal-september.org!reader01.eternal-september.org!.POSTED!not-for-mail
From: Paul Rubin <no.email@nospam.invalid>
Newsgroups: comp.lang.ada
Subject: Re: Latest suggestion for 202x
Date: Mon, 17 Jun 2019 08:32:47 -0700
Organization: A noiseless patient Spider
Message-ID: <87tvcons68.fsf@nightsong.com>
References: <728c4668-8fa0-4a57-a502-2bf476fc3940@googlegroups.com>
	<4908c3e3-18dc-4953-bf26-46f160d2ebfd@googlegroups.com>
	<9dcf22a2-2255-4089-b1f0-93e31448415e@googlegroups.com>
	<86h88obeu0.fsf@gaheris.avalon.lan>
	<39e749cd-de5c-44fa-b8ec-50d36f3bd52c@googlegroups.com>
	<qe8b41$pji$1@gioia.aioe.org>
Mime-Version: 1.0
Content-Type: text/plain
Injection-Info: reader02.eternal-september.org;
 posting-host="0dbf938e4e359d630498ea229b57ac43";
	logging-data="28100"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX18hr9ZQxxWnfi9lM+27x/yg"
User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/25.3 (gnu/linux)
Cancel-Lock: sha1:EDVK0KMvN2OHLB7wSqYkZOBf5Ks=
	sha1:tabg8XwL2y3XYUKyDdu37kaNnzU=
Xref: reader01.eternal-september.org comp.lang.ada:56663
Date: 2019-06-17T08:32:47-07:00
List-Id: <comp.lang.ada>

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:
> No, record is not a mapping. A mapping (properly typed) is
>    f : I -> V
> where I and V are *types*. You cannot define record members this
> way. Member names are not 1st class values, member values have
> different types.

Each member name is in effect a mapping.  I don't remember the record
member syntax but something like:

   type person is record:
     name : string;
     age : integer
   end record

Then basically "name" is a mapping from person to string, and "age" is a
mapping from person to integer, and there's some syntax sugar to deal
with member notation (xyz.name) and assignment (xyz.name := "John").
Assignment of xyz.name has type

  person -> string -> person

with the side effect of mutating the name.  If you really want to get
theoretical you can think of threading the state of the world through
the mapping, so it really maps one state of the world (plus a string) to
a new state of the world.  That's how monadic I/O in Haskell works.