安全な動的型と分散プロクラミング

抄録・要旨

For distributed programming, we introduce the notion of safe dynamics with dynamic types into MLlike functional programming language. The notion of dynamic types is here parametenzed with a set of monotypes, called a kind. The kind means an inductively defined set of monotypes. Hence, type case (dynamic type dispatch) mechanism can be naturally obtained as a recursive program over types, a la MartinLof, via an elimination rule for the inductively defined kinds. From a viewpoint of client-server programming, dynamic types under a constraint of the kinds provide a well-connected condition between a server and a client, with respect to types. Moreover, this point makes it possible to statically check dynamic types, such as ML-programs. A prototype of the system, called SDS (Safe Dynamics for Statically typed functional programming language), has been implemented by using C-language.