Ur/Web & Exact Real Arithmetic in Haskell

Ur/Web - Sean Chalmers

Following on from our introduction to dependent types in AGDA, Sean is going to show us around Ur and Ur/Web, a full stack web language and web framework with an extremely very rich type-system.

Ur is a programming language in the tradition of ML and Haskell, but featuring a significantly richer type system. Ur is functional, pure, statically typed, and strict. Ur supports a powerful kind of metaprogramming based on row types.

Ur/Web is Ur plus a special standard library and associated rules for parsing and optimization. Ur/Web supports construction of dynamic web applications backed by SQL databases. The signature of the standard library is such that well-typed Ur/Web programs "don't go wrong" in a very broad sense.

Exact Real Arithmetic in Haskell - Mitchell Riley

Exact real arithmetic allows us to do computations without worrying about precision or rounding. In contrast with arbitrary precision arithmetic, we only need to specify an output precision and the details for intermediate steps are handled automatically.

In this talk we will implement exact real arithmetic in two very different ways. First, the "fast binary Cauchy" system amounts to representing each real as a function Natural -> Rational, such that each successive output is a closer approximation to the true value than the last. The second system represents each real number as a continued fraction; an infinite tower of sums and reciprocals. Both systems benefit from a functional programming style and the resulting code is very simple to understand.