Re: Type regimes - terms and themes (Was: Naive, possibly silly question [LONG] )

From: JXStern (JXSternChangeX2R_at_gte.net)
Date: 11/08/03 

Date: Sat, 08 Nov 2003 16:19:45 GMT

On Sat, 8 Nov 2003 13:02:17 -0000, "S Perryman" <q@q.com> wrote:
>I have tried to define some terms in the spirit of paper by Luca
>Cardelli (praise be upon him) cited by Isaac Gouy.

Surely this kind of thing has been done already for some theory of
computation books? I believe there is also work involving logic, set
theory, and foundation of mathematics that is supposed to be
equivalent to type systems. OTOH, I don't have any specific
references for you, but I'll kibitz your definitions. (I have not
looked at the article you cite, to know which terms are his - reciting
the URL might be nice here).

>D1. Type Extent
>
>The set of types that are known to exist in a system.

The word "extent" seems a bit strained, but I see you want to use
"system" for something else. "Universe" might fit.

>D2. Type System
>
>The component that manages the type extent for a system.

Noting that this may exist only at compile time for a language like C?

>D2.1 Static Type System
>
>A system whose type extent is fixed (neither the type extent, nor the
>existing members of the type extent, can be changed) .
>
>D2.2 Dynamic Type System
>
>A system whose type extent can be changed when required.

Maybe it's better to assign static/dynamic to individual types, as a
language may have some of each?

>D3. Property
>
>Some aspect of a program component to which type is relevant.
>For example: variables, operation argument/result parameters.
>
>D3.1 Typed property
>
>A property that is associated with an exact type definition.
>
>D3.1 Untyped property
>
>A property that is not associated with any type definition.
>The type of any untyped property within a system is assumed to be the
>type extent for that system.

This needs a lot of work. Don't you mean by "property" a variable (or
constant) either with a direct value or as a reference to a value?
And would not a property necessarily associate with a complex type (ie
object)? And don't you want to say something about instance/class
scope?

Property does not "associate" with an "exact" type "definition".
Property is perhaps "bound" (?!), statically or dynamically, to "a"
type (more like to an instance(s) of a type, only degeneratively to a
class/type), or has as its value an entity which is typed -- or not.
An untyped property (if this is even a well-formed concept) is void,
not universal.

>D4. Typing
>
>The process of assigning type information to a component (or property)
>in a system.
>
>
>D4.1 Explicit Typing
>
>Type information is explicitly assigned to a component or property.
>For example: programming language syntax rules.
>
>D4.2 Implicit Typing
>
>Type information is implicitly assigned to a component or property.
>For example : type inference schemes.

I don't know about this implicit typing, I've seen some mentions of it
on the group but haven't paid attention. Sounds more like coercion to
me that a type-system issue as such. There may be type *propagation*
issues.

>D5. Type Checking
>
>The process of using the type system to ensure that components are
>using types in the manner expected by the type definitions.
>
>D5.1 Static Type Checking
>
>Type checking that is peformed before a program component can execute.
>
>
>D5.2 Dynamic Type Checking
>
>Type checking that is peformed during the execution of a program
>component.

You never defined "type definition", and I'm not sure that the
anthropomorphism "expected" is appropriate. I'm not sure the type
system is used, but rather is the agent, of checking. The whole thing
can probably be thought of better as testing invariants involving sets
of types, at compile or run time.

Static checking is performed before a program component *does*
execute, but not necessarily before it *can* execute -- one can run
something like lint over a text optionally.

Joshua Stern