Re: introspection in SML

Pascal Costanza <pc@[EMAIL PROTECTED]
> writes:
> Since there is no notion of 'runtime' in formal logics, why should
> those definitions be relevant for programming languages in general?
> They can only be relevant for specific programming languages.

In typed lambda calculus, type is conveyed by syntax, so the presence
or absence of a concept of runtime is irrelevant.  The ML crowd stays
with that notion of syntactic type, or what Lispers would call static
type.

> Yes. I think the misunderstanding comes from the fact that 'we'
> dynamic typers hear 'not typed' when 'you' static typers say
> 'untyped'. The term 'untyped' is very confusing in a (general)
> programming language setting.

Right, what the Lispers call "dynamic typed", the static typers would
call "tagged" (Cardelli [1] says "type-free").  What the Lispers call
"untyped" or "weakly typed" (e.g. assembly code or C++), the static
typers would call "unsound" or "unsafe" (Cardelli says "typeless").


To-may-to, to-mah-to, etc.

[1] Cardelli, Typeful Programming, section 10.
    http://citeseer.ist.psu.edu/243526.html