Re: Latest suggestion for 202x

[Paul Rubin <no.email@nospam.invalid>]

"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.