## Datafun: A functional datalog

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.

## Conclusion

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.