웹에서의 인터랙티브 사용자 경험은 점점 일반화되고 있습니다. 클라이언트 측 프로그램은 점점 더 복잡해지고 있으며, 이벤트 처리, HTML 문서 상태 읽기, 인터페이스 업데이트 등을 다뤄야 합니다. 이 논문에서는 이러한 세 가지 측면을 선언적으로 지원하는 선언적 언어를 제안하며, 복잡한 인터페이스를 레코드, 함수, 재귀와 같은 단순한 프로그래밍 기법을 사용하여 작성할 수 있는 프로그래밍 모델을 제공합니다.
Interactive user experiences on the web are becoming the norm. Client-side programs are becoming more complicated and have to deal with event handling, reading HTML document state and updating the interface. In this paper we propose a declarative language that supports these three facets of client-side browser development declaratively and provides a programming model where complex interfaces can be written using simple programming techniques such as records, functions and recursion.
다형적 RPC 계산법(polymorphic RPC calculus)은 프로그래머가 다형적 위치(polymorphic location) 구성 요소를 이용해 간결한 다중 계층(multitier) 프로그램을 작성할 수 있도록 해준다. 하지만 지금까지는 이를 실제로 구현한 사례가 없었다. 본 논문에서는 다형적 RPC 계산법에 기반한 실험적 프로그래밍 언어를 개발한다. 우리는 클라이언트(client)와 서버(server) 부분이 분리된 다형적 클라이언트-서버(CS) 계산법을 제안한다. 기존의 비타입(untyped) CS 계산법과 달리, 우리가 제안하는 계산법은 다형적 위치를 정적으로뿐만 아니라 동적으로도 해석할 수 있다. 또한, 우리는 다형적 RPC 계산법을 이 CS 계산법으로 타입 기반 분할 컴파일(type-based slicing compilation)하는 방식을 설계하고, 타입 및 의미론적 정당성(type and semantic correctness)을 증명하였다. 아울러, 실행에 불필요한 타입 정보를 제거하고, 실행 시 위치(location)는 유지하는 기법을 제안하며, 이를 통해 다형적 CS 계산법을 비타입 CS 계산법으로 변환하고, 그에 대한 의미론적 정당성도 입증하였다.
The polymorphic RPC calculus allows programmers to write succinct multitier programs using polymorphic location constructs. However, until now it lacked an implementation. We develop an experimental programming language based on the polymorphic RPC calculus. We introduce a polymorphic Client-Server (CS) calculus with the client and server parts separated. In contrast to existing untyped CS calculi, our calculus is not only able to resolve polymorphic locations statically, but it is also able to do so dynamically. We design a type-based slicing compilation of the polymorphic RPC calculus into this CS calculus, proving type and semantic correctness. We propose a method to erase types unnecessary for execution but retaining locations at runtime by translating the polymorphic CS calculus into an untyped CS calculus, proving semantic correctness.
RPC 계산법(RPC calculus)은 클라이언트-서버 모델을 위한 위치 함수(located function)를 작성할 수 있는 다중 계층(multi-tier) 프로그래밍 언어(예: Links)의 간단한 의미론적 기반이다. 이후, 타입이 부여된 RPC 계산법(typed RPC calculus)이 설계되어, 함수의 위치 정보를 타입으로 표현하고, 이를 기반으로 한 위치 타입 기반 분할 컴파일(location type-directed slicing compilation)을 수행할 수 있게 되었다. 그러나 현재까지의 위치 사용은 단일형(monomorphic) 위치에 한정되어 있어, RPC 계산법 이론을 클라이언트-서버 모델에 실제로 적용하기 위해서는 이 한계를 극복해야 한다. 본 논문에서는 프로그래머가 다형적 위치(polymorphic location) 구문을 사용하여 간결한 다중 계층 프로그램을 작성할 수 있도록 하는 다형적 RPC 계산법(polymorphic RPC calculus)을 제안한다. 이러한 다형적 다중 계층 프로그램은 기존의 분할 컴파일 기법에 적합한 위치 상수만 포함된 프로그램으로 자동 변환될 수 있다. 우리는 다형적 RPC 계산법을 위한 타입 시스템을 정식화하고, 그 타입 안전성(type soundness)을 증명하였다. 또한, 모노모픽 변환(monomorphization translation)을 설계하고, 해당 변환에 대한 타입 및 의미론적 정당성도 함께 증명하였다.
The RPC calculus is a simple semantic foundation for multi-tier programming languages such as Links in which located functions can be written for the client-server model. Subsequently, the typed RPC calculus is designed to capture the location information of functions by types and to drive location type-directed slicing compilations. However, the use of locations is currently limited to monomorphic ones, which is one of the gaps to overcome to put into practice the theory of RPC calculi for client-server model. This paper proposes a polymorphic RPC calculus to allow programmers to write succinct multi-tier programs using polymorphic location constructs. Then the polymorphic multi-tier programs can be automatically translated into programs only containing location constants amenable to the existing slicing compilation methods. We formulate a type system for the polymorphic RPC calculus, and prove its type soundness. Also, we design a monomorphization translation together with proofs on its type and semantic correctness for the translation.
다중 계층 프로그래밍 언어(multi-tier programming languages)를 사용하면, 프로그래머는 코드가 실행될 위치(location)를 명시할 수 있어, 클라이언트와 서버 프로그램을 별도로 작성하고 이를 함께 테스트해야 하는 웹 기반 클라이언트-서버 모델에서의 개발 부담을 줄일 수 있다.
Cooper와 Wadler가 제안한 RPC 계산법(RPC calculus)은 이러한 언어들의 이론적 기반 중 하나로, 대칭적 통신(symmetric communication)을 지원하며, 프로그래머가 임의로 깊게 중첩된 클라이언트-서버 상호작용을 작성할 수 있는 특징을 가진다.
그러나 기존 연구들은 동적으로 타입이 부여된 위치(dynamically typed locations)만을 다루고 있다.
이에 우리는 위치를 타입 수준에서 추적할 수 있는(typed) 타입이 부여된 RPC 계산법(typed RPC calculus)을 제안한다. 새롭게 설계된 위치 기반 타입 시스템(located type system)은 클라이언트-서버 모델을 위한 RPC 계산법의 이론적 토대를 마련한다.
(다음에 소개할 SCP2020 및 PPDP2021에 발표된 논문들에서는, 타입이 부여된 RPC 계산법이 다형적 위치(polymorphic locations)와 타입 기반 분할 컴파일(type-based slicing compilation)을 통해 확장될 것입니다.)
With multi-tier programming languages, programmers can specify the locations of code to run in order to reduce development efforts for the web-based client-server model where programmers write client and server programs separately and test the multiple programs together. The RPC calculus, one of the foundations of those languages by Cooper and Wadler, has the feature of symmetric communication in programmer's writing arbitrarily deep nested client-server interactions. However, the existing research only considers dynamically typed locations. We propose a typed RPC calculus where locations are tracked in type-level. A new located type system paves the way for a theory of RPC calculi for the client-server model.
(In the following papers published in SCP2020 and PPDP2021, the typed RPC calculus will be enhanced with polymorphic locations and a type-based slicing compilation.)