Re: [lojban] More on lojban programatic semantics: Strong typing and inferencing of types

[Brook Conner <nellardo@concentric.net>]

la xorxes. cusku di'e
> la brukcr cusku di'e
> 
> >So, for example, you can use "poi" to annotate sumti with type
> >information, or simply an appropriate selbri for "declaring" variables:
> >
> >ko jarco la stokuot. poi mekso -- show the "stock-quote", which is a
> >mathematical expression
> 
> For annotation {noi} is better than {poi}.
> {la stokout poi mekso} would be used to restrict the reference to
> {la stokuot} which is a mekso, as opposed to any other {la stokuot}
> which is something else.

Hmmm. You raise an interesting trade-off. Since noi is "incidental", it
implies that there isn't another "la stokuot." somewhere that is
actually a different kind of "la stokuot." However, most PLs have
scoping rules that allow multiple things of the same name - the scoping
makes sure the referent of the name is always unambiguous. 

On the other hand, "poi" implies that the characteristic named is an
*essential* aspect of the thing named - this is much closer to the
meaning of a type in a PL.

> >la stokuot. mekso -- "stock-quote" is a mathematical expr.
> >
> >la stokuot. namcu -- "stock-quote" is a number.
> 
> I think a mekso cannot be a namcu, it's supposed to be an
> unevaluated expression, but I may be wrong. The mekso part
> of the language has never really been worked out.

Ehm, I think a namcu is a valid mekso, but I wasn't (yet) talking about
type hierarchy - just giving multiple examples. These bridi were meant
to be examples of declarations.
 
> >la stokuot. saclu -- "stock-quote" is a rational number
> 
> Again, for {saclu} I think it is only the symbolic representation,
> not the number that is at stake. You would be saying for example
> that {la stokout} is the name of the string of symbols 0.75,
> not the number 0.75=3/4

My understanding was that naclu (and the other similar gismu) followed a
sumti pattern of "x1 is <some kind of number> of value x2". So naclu
means that x1 is a rational, whose value is given by x2. So in the
example above, I would be saying that "la stokuot." is an *unspecified*
rational number. X2 is the value. So you could "initialize" a variable
at the same time by including x2.
 
> >The diversity of "number" gismu that include units has a nice side
> >effect of reducing the kinds of goofs that crashed  the recent Mars
> >mission: if it's "minli", then it is miles. If it is "mitre", then it is
> >meters.
> 
> I'm not sure what you mean here. I think it is the other way
> around, because the units are included in the gismu, the numbers
> (se minli, se mitre) are actually all adimensional.

A numerical value in x2 is adimensional, but the things in x1 *are*
dimensioned, because the gismu asserts that this is so. Further
,something in x2 could be dimensioned if it was identified earlier as
being in a dimension. In this case, either the dimensions have to agree,
or there has to be a reasonable conversion. So:

la numbr. namcu li pe --- "Number" is a number, whose value is 1

la distens. minli la numbr.  -- "Distance" is in miles, the value 1

la triplen. mitre la distens. -- Either an error (la distens. is miles,
la triplen. is meters) or conversion of values automatically takes place.

la fatsos. grake la distens. -- Definitely an error - "Fatsos" is in
grams the value "Distance" _ but distance has been specified to be in
miles, and there's no way to convert miles to grams.

> It is an interesting topic. Colin Fine posted some interesting
> stuff about this kind of thing a couple of years ago.

Cool. I'll have to dig in the archives.

co'o mi'e brukcr.