Dynamic typing in a statically-typed language
Dynamic typing in a statically-typed language
复制标题
静态类型语言中的动态类型
DOI：
--
复制
发表时间：
1989
期刊：
影响因子：
--
通讯作者：
G. Plotkin
中科院分区：
文献类型：
--
作者：
M. Abadi;L. Cardelli;B. Pierce;G. Plotkin
与在运行时执行所有类型一致性检查的语言相比，静态型编程语言允许更早的错误检查，更好地检查纪律编程样式以及生成更有效的对象代码。但是，即使在静态类型的语言中，通常也有必要处理在编译时不知道类型的数据。为了安全地处理这种情况，我们建议添加一种型号的型号，其值是值V和类型标记t的对，其中v具有由T动态实例表示的类型。 -SAFE Typecase构造。
本文是对具有动态类型的简单语言的语法，操作语义和语义语义的探索。我们举例说明了如何在编程中使用动态类型的值。然后，我们讨论语言的操作语义，并获得合理的定理。我们介绍了该语言的典型语义的两个表述，并将其与操作语义相关联。最后，我们考虑了多态性和某些实施问题的含义。
Statically-typed programming languages allow earlier error checking, better enforcement of disciplined programming styles, and generation of more efficient object code than languages where all type-consistency checks are performed at runtime. However, even in statically-type languages, there is often the need to deal with data whose type cannot be known at compile time. To handle such situations safely, we propose to add a type Dynamic whose values are pairs of a value v and a type tag T where v has the type denoted by T. Instances of Dynamic are built with an explicit tagging construct and inspected with a type-safe typecase construct.
This paper is an exploration of the syntax, operational semantics, and denotational semantics of a simple language with the type Dynamic. We give examples of how dynamically-typed values might be used in programming. Then we discuss an operational semantics for our language and obtain a soundness theorem. We present two formulations of the denotational semantics of this language and relate them to the operational semantics. Finally, we consider the implications of polymorphism and some implementation issues.