Leading on from the slides by Peyton Jones, this lecture sets out how constructor classes and higher-order functions can help to treat effectful computation within a pure functional language; or potentially contain its influence within an imperative one.
Lecture 8: Monads and I/O
15 October 2010
Comments Off on Lecture 8: Monads and I/O |
Lecture log | Tagged: Haskell, metaprogramming, monads, type classes, types, types and effects |
Permalink
Posted by Ian Stark
Lecture 20: Type-Checking for SQLizability
18 March 2010Review of what LINQ can do in C# to lower the impedance mismatch between general-purpose programming languages and database query languages. Advantages and limitations on this; in particular the possibility of runtime failure, limits of abstraction, and the role of reflection.
One possible route to improving this: introduction of a type and effect system to track behaviour that cannot be represented in SQL. This allows arbitrary use of parametrization and higher-order functions, while providing compile-time guarantees of on-database execution. Outline of proof via a strongly-normalizing rewrite system. Several examples of how this more deeply embeds querying into a functional language, allowing modular construction of code and opening up queries to conventional compiler rewriting as well as SQL database-specific optimisations.
This lecture is based on the work of Ezra Cooper, in particular the following paper:
- Ezra Cooper. The script-writer’s dream: How to write great SQL in your own language, and be sure it will succeed. In Database Programming Languages: Proceedings of the 12th International Symposium DBPL 2009, Lecture Notes in Computer Science 5708, pages 36–51. Springer-Verlag, 2009.
You can follow his research blog for more on this.
Homework
Please fill out and submit an anonymous feedback questionnaire. Thank you.
Comments Off on Lecture 20: Type-Checking for SQLizability |
Lecture log | Tagged: Links, metaprogramming, sql, types, types and effects |
Permalink
Posted by Ian Stark