Polyrpc
A multi-tier functional programming language based on the polymorphic rpc calculus
- Allow to write client, server, and location-polymorphic functions
- A polyrpc programming language system including a parser, a poly rpc type checker, a slicing compiler, a poly cs type checker, and a poly cs interpter.
- A polymorphic location inference algorithm based on bidirectional typechecking.
- Syntactic sugar for location annotations (particularly for location-independent functions)
News
- A bidirectional location inference algorithm is available in the master branch. Examples are available at examples.
- Use --debug-parse to see a desugared term before the inference and --dump-typecheck to check a location inferenced term
- For experts, --debug-typecheck is available to see how the bidirectional inference is working in detail.
Download and build
$ git clone https://github.com/kwanghoon/polyrpc
$ cd polyrpc
$ stack build
Run an polyrpc interpreter
$ stack exec -- polyrpc ./examples/helloworld.rl
POLYRPC, version 0.1.0: http://github.com/kwanghoon/polyrpc/
[Reading] ./examples/helloworld.rl
[Lexing]
[Parsing]
[Type checking]
[Compiling]
[Verifying generated codes]
[Executing codes]
Hello World
[Success]
Documents
-
Research papers
- A Typed Slicing Compilation for the Polymorphic RPC Calculus, the 23rd International Symposium on Principles and Practice of Declarative Programming (PPDP), September 2021. (arXiv)
- A Polymorphic RPC calculus, Science of Computer Programming, Vol.197, Article 102499, October 2020. (arXiv)
- A Theory of RPC calculi for Client-Server Model, Journal of Functional Programming, e5, 39, pages, 2019.
-
A polymorphic location inference algorithm based on bidirectional type checking
- The surface syntax is available in surface/Surface.hs.
- Based on Jana Dunfield, Neelakantan R. Krishnaswami, Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism, ICFP2013 and its implementation of the bidirectional type checking algorithm by Olle Fredriksson.
- The algorithm is for the predicative subset of the polymorphic RPC calculus.