2011-04-30

read-only, constance, and uniqueness

4.22: adda/type/const/for shared-link parameters:

. what is the diff'tween {const, rom}?
and did you notice that in formal params,
where rom is needed,
this const syntax is not very applicable ?

. the reason for being concerned with rom
is that people would like to know
whether they can safely pass a reference .
. this should be handled as it is in Ada:
it is safe unless the parameter is
specifically marked as out-mode .
. so the question then becomes,
what is an intuitive symbol for out-mode?
. ada's goto enclosure has been written about before;
and out-mode mode param's are like goto's;
because, they are transfering control to
some surprising places .
todo:
. how was it shown
where the out-mode is happening?
eg, for an array of pointers to strings,
is the array being modified (dangling pointer risk)
or are the strings being modified ?
the out-mode syntax needs to
make this distinction easy to express .

. what if the caller provides a shared link;
and, while the caller meant for the ref'
to provide the value it represented
at the time of the call,
in fact it will be changing dynamically,
because even though the caller is suspended
the caller's co.programs are still modifying the link;
therefore:
when a link represents a value
then the shared value needs a soft-locking system:
it doesn't prevent co.programs from writing
but requires the first writer
to ask the system for a lock-removal service;
in doing that,
the system sees who the lock belongs to
and copies the current value .
. if it knows the lock owner is going to be quick
it can just high-prioritize that call,
and suspend the unlocker until then .
. this is a lot efficiency glue
so the system needs to know at call time
whether an input is large eno' to link to,
since copying makes life much simpler .

4.22: mis.adda/type/const/for non-parameters:
. while const's for param's are not an issue
(see notes about rom above)
[@] adda/type/const/for shared-link parameters
const's for symbol declarations are very useful .
. I've had problems finding a const operator
(below) [@] mis.adda/uniqueness operator
but, having the need restricted to non-parameters
makes the search moot, I thought,
as const's can be initialized with a label
rather than an assignment operator;
nevertheless,
what if uninitialized, but
intending to assign later only once?
then a const symbol would enforce
only one assignment .
. just as math uses (someone!)
to mean (exactly one),
the type system could use (type!)
to mean not just (some
of the values from this type)
but instead (exactly one
of the values from this type
will be used here).

4.22: mis.adda/uniqueness operator:
. a convenient symbol for rom
is the same as for unique,
since rom maintains a unique value across times .
. notice though, that
when I chose (!) for unique
it was because math uses it for the
unique existence quantifier;
but when (!) is used alone, without (some),
math defines it as factorial;
and what does that have to do with unique?
( recall factorial:
x! = *(^i: i= 1..x) -- very multiplicative!
) . in both of these math cases,
it matches the usual english meaning:
(very *) .
. in the case of (some!),
(exactly one) is a very useful version of
(some one) because,
(mapping to exactly one)
is an essential characteristic of functions
-- one of math's foundations .
. intuitively the name could come from
feeling very responsible:
ie, if "(some one) did it
then there is a degree of anonymity,
but if exactly (!) one member is responsible
then that one member is
very much the reason for the season .