The Breeze language used in SAFE is a mostly functional language, similar in spirit to ML, except that it enforces an information flow model to support both confidentiality and integrity. Breeze will be both statically and dynamically typed in keeping with the standard security principle of defense-in-depth. Currently, the type system, which is based on the Myers-Liskov decentralized label model, is only dynamically-typed.I'm having a little bit of trouble understanding what they mean by a language being both statically and dynamically typed. Has a programming language attempted this in the past? What does this look like, concretely, in the syntax and behavior of the language?
Generally I've understood that static typing means explicit declaration of the type of the variable to the compiler, with compile-time verification of access to only fields and methods that are known to be valid for that type, while dynamic typing means that the compiler does not so restrict the access via that variable, and may not even know the intended type of the variable until runtime.
So what would it mean for a language to be both statically and dynamically typed?
static/dynamic typing and explicit/implicit typing are 'orthogonal' properties.
ReplyDeleteA language system (compiler/runtime) can support all four.
E.G. it would not be unexpected for a high quality Common Lisp implementation to support all four. I.E. in the presence of sufficient type information, some provided explicitly by the programmer through the judicious use of type declarations, some maybe inferred by the compiler, the compiler may be able to elide some dynamic type checks.
static/dynamic typing and explicit/implicit typing are 'orthogonal' properties.
ReplyDeleteA language system (compiler + runtime) might support all four. Common Lisp would be an example. In the presence of sufficient type information, some provided explicitly by the programmer through judicious use of type declarations, some inferred by the compiler (i.e. implicit), a high quality Common Lisp compiler might decide (i.e. statically) to elide some otherwise necessary dynamic type check.