Datafun: A functional datalog

Written by OlivierNicole (Olivier Nicole)
Published: 2016-09-17 (last updated: 2016-09-21)

Datafun - a langauge that has been discovered / invented. Somewhere between the two.

Datafun is:

  • a simply-typed lambda-calculus
  • where types are posets & some are semilattices
  • that tracks monoticity via types
  • to let you compute fixed points
  • and know they terminate.

Tracking monotonicity

  • Two types of function: discrete or monotone
  • Two kinds of variable: discrete or monotone
  • Two typing contexts: Delta discrete, Gamma monotone.

Fixed points

Example of CYK parsing

The CYK parsing algorithm (to parse a context-free grammar) translates very easily into Datafun.


Many algorithms are concisely expressed as fixed points of monotone maps on semilattices. Tracking monotonicity is very useful.

Datafun can be seen as a generalization of Datalog because it supports other semilattices.