Michael Arntzenius
ABSTRACT
Datalog may be considered either an unusually powerful query language or a carefully limited logic programming language. Datalog is declarative, expressive, and optimizable, and has been applied successfully in a wide variety of problem domains. However, most use-cases require extending Datalog in an application-specific manner. In this paper we define Datafun, an analogue of Datalog supporting higher-order functional programming. The key idea is to track monotonicity with types.
- S. Abramsky and A. Jung. Domain theory. Handbook of logic in computer science, 3:1–168, 1994. Google Scholar
Digital Library
- P. Alvaro, N. Conway, J. M. Hellerstein, and W. R. Marczak. Consistency analysis in Bloom: a CALM and collected approach. In CIDR 2011, Fifth Biennial Conference on Innovative Data Systems Research, Asilomar, CA, USA, January 9-12, 2011, Online Proceedings, pages 249–260, 2011.Google Scholar
- S. Antoy and M. Hanus. Functional logic programming. Communications of the ACM, 53(4):74–85, Apr. 2010. ISSN 0001-0782. Google ScholarDigital Library
- M. Aref, B. ten Cate, T. J. Green, B. Kimelfeld, D. Olteanu, E. Pasalic, T. L. Veldhuizen, and G. Washburn. Design and implementation of the LogicBlox system. In Proceedings of the 2015 ACM SIGMOD International Conference on Management of Data, Melbourne, Victoria, Australia, May 31 - June 4, 2015, pages 1371–1382, 2015. Google ScholarDigital Library
- F. Bancilhon, D. Maier, Y. Sagiv, and J. D. Ullman. Magic sets and other strange ways to implement logic programs (extended abstract). In Proceedings of the Fifth ACM SIGACT-SIGMOD Symposium on Principles of Database Systems, PODS ’86, pages 1–15, New York, NY, USA, 1986. ACM. ISBN 0-89791-179-2. doi: 10.1145/6012.15399. Google ScholarDigital Library
- M. Y. Becker, C. Fournet, and A. D. Gordon. Secpal: Design and semantics of a decentralized authorization language. Journal of Computer Security, 18(4):619–665, 2010. Google ScholarDigital Library
- P. N. Benton and P. Wadler. Linear logic, monads and the lambda calculus. In Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, USA, July 27-30, 1996, pages 420– 431, 1996. Google ScholarDigital Library
- R. E. Bryant. Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Computing Surveys (CSUR), 24(3):293–318, 1992. Google ScholarDigital Library
- M. Budiu and G. Plotkin. Multilinear programming with big data. Festschrift for Luca Cardelli, September 2014.Google Scholar
- J. Cheney, S. Lindley, and P. Wadler. Query shredding: efficient relational evaluation of queries over nested multisets. In International Conference on Management of Data, SIGMOD 2014, Snowbird, UT, USA, June 22-27, 2014, pages 1027–1038, 2014. Google ScholarDigital Library
- O. de Moor, D. Sereni, M. Verbaere, E. Hajiyev, P. Avgustinov, T. Ekman, N. Ongkingco, and J. Tibble. .QL: Object-oriented queries made easy. In Generative and Transformational Techniques in Software Engineering II, International Summer School, GTTSE 2007, Braga, Portugal, July 2-7, 2007. Revised Papers, pages 78–133, 2007. Google ScholarDigital Library
- J. Dunfield and N. R. Krishnaswami. Complete and easy bidirectional typechecking for higher-rank polymorphism. In International Conference on Functional Programming (ICFP), Sept. 2013. arXiv:1306.6032{cs. PL}. M. Felleisen and R. Hieb. The revised report on the syntactic theories of sequential control and state. Theor. Comput. Sci., 103(2):235–271, Sept. 1992. ISSN 0304-3975. doi: 10.1016/0304-3975(92)90014-7. Google ScholarDigital Library
- ISBN 0-306-40060-X. H. Ganzinger and D. A. McAllester. Logical algorithms. In Logic Programming, 18th International Conference, ICLP 2002, Copenhagen, Denmark, July 29 - August 1, 2002, Proceedings, pages 209–223, 2002. Google ScholarDigital Library
- J. Gibbons, F. Henglein, R. Hinze, and N. Wu. Relational algebra by way of adjunctions. In Database Programming Languages, October 2015.Google Scholar
- R. Hickey, S. Halloway, and J. Gehtland. Datomic: The fully transactional, cloud-ready, distributed database. http://www.datomic.com. Accessed: 11 March 2016.Google Scholar
- M. Madsen, M. Yee, and O. Lhoták. From datalog to flix: a declarative language for fixed points on lattices. In C. Krintz and E. Berger, editors, Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016, Santa Barbara, CA, USA, June 13-17, 2016, pages 194–208. ACM, 2016. ISBN 978-1-4503- 4261-2. doi: 10.1145/2908080.2908096. Google ScholarDigital Library
- A. Ohori, P. Buneman, and V. Breazu-Tannen. Database programming in Machiavelli—a polymorphic language with static type inference. In Proceedings of the 1989 ACM SIGMOD International Conference on Management of Data, SIGMOD ’89, pages 46–57, New York, NY, USA, 1989. ACM. ISBN 0-89791-317-5. doi: 10.1145/67544.66931. Google ScholarDigital Library
- F. Pfenning and R. Davies. A judgmental reconstruction of modal logic. Mathematical Structures in Computer Science, 11(4):511–540, 2001. doi: 10.1017/S0960129501003322. Google ScholarDigital Library
- B. C. Pierce and D. N. Turner. Local type inference. ACM Trans. Program. Lang. Syst., 22(1):1–44, 2000. Google ScholarDigital Library
- J. C. Reynolds. Definitional interpreters for higher-order programming languages. Higher-Order and Symbolic Computation, 11(4):363–397, 1998. Google ScholarDigital Library
- M. Schäfer and O. de Moor. Type inference for datalog with complex type hierarchies. In Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Madrid, Spain, January 17-23, 2010, pages 145–156, 2010. Google ScholarDigital Library
- S. M. Shieber, Y. Schabes, and F. C. N. Pereira. Principles and implementation of deductive parsing. J. Log. Program., 24(1&2):3–36, 1995.Google Scholar
- R. J. Simmons and F. Pfenning. Linear logical approximations. In Proceedings of the 2009 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-based Program Manipulation, PEPM 2009, Savannah, GA, USA, January 19-20, 2009, pages 9–20, 2009. Google ScholarDigital Library
- Z. Somogyi, F. Henderson, and T. C. Conway. The implementation of mercury, an efficient purely declarative logic programming language. In ILPS 1994, Workshop 4: Implementation Techniques for Logic Programming Languages, Ithaca, New York, USA, November 17, 1994, 1994.Google Scholar
- J. Whaley. Context-Sensitive Pointer Analysis using Binary Decision Diagrams. PhD thesis, Stanford University, Mar. 2007. Google ScholarDigital Library
- J. Whaley, D. Avots, M. Carbin, and M. S. Lam. Using Datalog and binary decision diagrams for program analysis. In K. Yi, editor, Proceedings of the 3rd Asian Symposium on Programming Languages and Systems, volume 3780. Springer-Verlag, Nov. 2005. Google ScholarDigital Library
- L. Wong. Kleisli, a functional query system. J. Funct. Program., 10(1): 19–56, 2000. Google ScholarDigital Library
Index Terms
- Datafun: a functional Datalog
Recommendations
Fixpoints for the masses: programming with first-class Datalog constraints
Datalog is a declarative logic programming language that has been used in a variety of applications, including big-data analytics, language processing, networking and distributed systems, and program analysis.
In this paper, we propose first-class ...
From Datalog to flix: a declarative language for fixed points on lattices
PLDI '16We present Flix, a declarative programming language for specifying and solving least fixed point problems, particularly static program analyses. Flix is inspired by Datalog and extends it with lattices and monotone functions. Using Flix, implementors ...
Datafun: a functional Datalog
ICFP '16Datalog may be considered either an unusually powerful query language or a carefully limited logic programming language. Datalog is declarative, expressive, and optimizable, and has been applied successfully in a wide variety of problem domains. ...
Comments