Does anybody have a copy of my LLParser.hs that once was available at http://antti-juhani.kaijanaho.fi/tmp/LLParser.hs? It looks like all my copies (except for an early version I used in one of my functional programming lectures) have gone the way of the dodo.
We are in the process of creating the next iteration of LambdaCube, where we finally depart from the Haskell EDSL approach and turn the language into a proper DSL. The reasons behind this move were outlined in an earlier post. However, we still use the EDSL as a testing ground while designing the type system, since GHC comes with a rich set of features available for immediate use. The topic of today’s instalment is our recent experiment to make illegal types unrepresentable through a custom kind system. This is made possible by the fact that GHC recently introduced support for promoting datatypes to kinds.
Even though the relevant DataKinds extension is over a year old (although it’s been officially supported only since GHC 7.6), we couldn’t find any example to use it for modelling a real-life domain. Our first limited impression is that this is a direction worth pursuing.
It might sound surprising that this idea was already brought up in the context of computer graphics in the Spark project. Tim Foley’s dissertation briefly discusses the type theory behind Spark (see Chapter 5 for details). The basic idea is that we can introduce a separate kind called Frequency (Spark refers to this concept as RecordType), and constrain the Exp type constructor (@ in Spark) to take a type of this kind as its first argument.
To define the new kind, all we need to do is write a plain data declaration, as opposed to the four empty data declarations we used to have:data Frequency = Obj | V | G | F
As we enable the DataKinds extension, this definition automatically creates a kind and four types of this kind. Now we can change the definition of Exp to take advantage of it:data Exp :: Frequency -> * -> * where ...
For the time being, we diverge from the Spark model. The difference is that the resulting type has kind * in our case, while in the context of Spark it would be labelled as RateQualifiedType. Unfortunately, Haskell doesn’t allow using non-* return kinds in data declarations, so we can’t test this idea with the current version. Since having a separate Exp universe is potentially useful, we might adopt the notion for the DSL proper.
We don’t have to stop here. There are a few more areas where we can sensibly constrain the possible types. For instance, primitive and fragment streams as well as framebuffers in LambdaCube have a type parameter that identifies the layer count, i.e. the number of framebuffer layers we can emit primitives to using geometry shaders. Instead of rolling a custom solution, now we can use type level naturals with support for numeric literals. Among others, the definition of stream types and images reflects the new structure:data VertexStream prim t data PrimitiveStream prim (layerCount :: Nat) (stage :: Frequency) t data FragmentStream (layerCount :: Nat) t data Image (layerCount :: Nat) t where ...
Playing with kinds led to a little surprise when we looked into the texture subsystem. We had marker types called DIM1, DIM2, and DIM3, which were used for two purposes: to denote the dimension of primitive vectors and also the shape of equilateral textures. Both structures have distinct fourth options: 4-dimension vectors and rectangle-shaped textures. While they are related – e.g. the texture shape implies the dimension of vectors used to address texels –, these are different concepts, and we consider it an abuse of the type system to let them share some cases. Now vector dimensions are represented as type-level naturals, and the TextureShape kind is used to classify the phantom types denoting the different options for texture shapes. It’s exactly like moving from an untyped language to a typed one.
But what did we achieve in the end? It looks like we could express the very same constraints with good old type classes. One crucial difference is that kinds defined as promoted data types are closed. Since LambdaCube tries to model a closed domain, we see this as an advantage. It also feels conceptually and notationally cleaner to express simple membership constraints with kinds than by shoving them in the context. However, the final decision about whether to use this approach has to wait until we have the DSL working.
This Theory Lunch, I gave an introduction to the functional logic programming language Curry. You can find a write-up of my talk on my personal blog.
Curry is a programming language that integrates functional and logic programming. Last week, Denis Firsov and I had a look at Curry, and Thursday, I gave an introductory talk about Curry in the Theory Lunch. This blog post is mostly a write-up of my talk.
Like Haskell, Curry has support for literate programming. So I wrote this blog post as a literate Curry file, which is available for download. If you want to try out the code, you have to install the Curry system KiCS2. The code uses the functional patterns language extension, which is only supported by KiCS2, as far as I know.Functional programming
The functional fragment of Curry is very similar to Haskell. The only fundamental difference is that Curry does not support type classes.
Let us do some functional programming in Curry. First, we define a type whose values denote me and some of my relatives.data Person = Paul | Joachim | Rita | Wolfgang | Veronika | Johanna | Jonathan | Jaromir
Now we define a function that yields the father of a given person if this father is covered by the Person type.father :: Person -> Person father Joachim = Paul father Rita = Joachim father Wolfgang = Joachim father Veronika = Joachim father Johanna = Wolfgang father Jonathan = Wolfgang father Jaromir = Wolfgang
Based on father, we define a function for computing grandfathers. To keep things simple, we only consider fathers of fathers to be grandfathers, not fathers of mothers.grandfather :: Person -> Person grandfather = father . father Combining functional and logic programming
Logic programming languages like Prolog are able to search for variable assignments that make a given proposition true. Curry, on the other hand, can search for variable assignments that make a certain expression defined.
For example, we can search for all persons that have a grandfather according to the above data. We just enter
grandfather person where person free
at the KiCS2 prompt. KiCS2 then outputs all assignments to the person variable for which grandfather person is defined. For each of these assignments, it additionally prints the result of the expression grandfather person.Nondeterminism
Functions in Curry can actually be non-deterministic, that is, they can return multiple results. For example, we can define a function element that returns any element of a given list. To achieve this, we use overlapping patterns in our function definition. If several equations of a function definition match a particular function application, Curry takes all of them, not only the first one, as Haskell does.element :: [el] -> el element (el : _) = el element (_ : els) = element els
Now we can enter
at the KiCS2 prompt, and the system outputs six different results.Logic programming
We have already seen how to combine functional and logic programming with Curry. Now we want to do pure logic programming. This means that we only want to search for variable assignments, but are not interested in expression results. If you are not interested in results, you typically use a result type with only a single value. Curry provides the type Success with the single value success for doing logic programming.
Let us write some example code about routes between countries. We first introduce a type of some European and American countries.data Country = Canada | Estonia | Germany | Latvia | Lithuania | Mexico | Poland | Russia | USA
Now we want to define a relation called borders that tells us which country borders which other country. We implement this relation as a function of type
Country -> Country -> Success
that has the trivial result success if the first country borders the second one, and has no result otherwise.
Note that this approach of implementing a relation is different from what we do in functional programming. In functional programming, we use Bool as the result type and signal falsity by the result False. In Curry, however, we signal falsity by the absence of a result.
Our borders relation only relates countries with those neighbouring countries whose names come later in alphabetical order. We will soon compute the symmetric closure of borders to also get the opposite relationships.borders :: Country -> Country -> Success Canada `borders` USA = success Estonia `borders` Latvia = success Estonia `borders` Russia = success Germany `borders` Poland = success Latvia `borders` Lithuania = success Latvia `borders` Russia = success Lithuania `borders` Poland = success Mexico `borders` USA = success
Now we want to define a relation isConnected that tells whether two countries can be reached from each other via a land route. Clearly, isConnected is the equivalence relation that is generated by borders. In Prolog, we would write clauses that directly express this relationship between borders and isConnected. In Curry, on the other hand, we can write a function that generates an equivalence relation from any given relation and therefore does not only work with borders.
We first define a type alias Relation for the sake of convenience.type Relation val = val -> val -> Success
Now we define what reflexive, symmetric, and transitive closures are.reflClosure :: Relation val -> Relation val reflClosure rel val1 val2 = rel val1 val2 reflClosure rel val val = success symClosure :: Relation val -> Relation val symClosure rel val1 val2 = rel val1 val2 symClosure rel val2 val1 = rel val1 val2 transClosure :: Relation val -> Relation val transClosure rel val1 val2 = rel val1 val2 transClosure rel val1 val3 = rel val1 val2 & transClosure rel val2 val3 where val2 free
The operator & used in the definition of transClosure has type
Success -> Success -> Success
and denotes conjunction.
We define the function for generating equivalence relations as a composition of the above closure operators. Note that it is crucial that the transitive closure operator is applied after the symmetric closure operator, since the symmetric closure of a transitive relation is not necessarily transitive.equivalence :: Relation val -> Relation val equivalence = reflClosure . transClosure . symClosure
The implementation of isConnected is now trivial.isConnected :: Country -> Country -> Success isConnected = equivalence borders
Now we let KiCS2 compute which countries I can reach from Estonia without a ship or plane. We do so by entering
Estonia `isConnected` country where country free
at the prompt.
We can also implement a nondeterministic function that turns a country into the countries connected to it. For this, we use a guard that is of type Success. Such a guard succeeds if it has a result at all, which can only be success, of course.connected :: Country -> Country connected country1 | country1 `isConnected` country2 = country2 where country2 free Equational constraints
Curry has a predefined operator
=:= :: val -> val -> Success
that stands for equality.
We can use this operator, for example, to define a nondeterministic function that yields the grandchildren of a given person. Again, we keep things simple by only considering relationships that solely go via fathers.grandchild :: Person -> Person grandchild person | grandfather grandkid =:= person = grandkid where grandkid free
Note that grandchild is the inverse of grandfather.Functional patterns
Functional patterns are a language extension that allows us to use ordinary functions in patterns, not just data constructors. Functional patterns are implemented by KiCS2.
Let us look at an example again. We want to define a function split that nondeterministically splits a list into two parts.1 Without functional patterns, we can implement splitting as follows.split' :: [el] -> ([el],[el]) split' list | front ++ rear =:= list = (front,rear) where front, rear free
With functional patterns, we can implement splitting in a much simpler way.split :: [el] -> ([el],[el]) split (front ++ rear) = (front,rear)
As a second example, let us define a function sublist that yields the sublists of a given list.sublist :: [el] -> [el] sublist (_ ++ sub ++ _) = sub Inverting functions
In the grandchild example, we showed how we can define the inverse of a particular function. We can go further and implement a generic function inversion operator.inverse :: (val -> val') -> (val' -> val) inverse fun val' | fun val =:= val' = val where val free
With this operator, we could also implement grandchild as inverse grandfather.
Inverting functions can make our lives a lot easier. Consider the example of parsing. A parser takes a string and returns a syntax tree. Writing a parser directly is a non-trivial task. However, generating a string from a syntax tree is just a simple functional programming exercise. So we can implement a parser in a simple way by writing a converter from syntax trees to strings and inverting it.
We show this for the language of all arithmetic expressions that can be built from addition, multiplication, and integer constants. We first define types for representing abstract syntax trees. These types resemble a grammar that takes precedence into account.type Expr = Sum data Sum = Sum Product [Product] data Product = Product Atom [Atom] data Atom = Num Int | Para Sum
Now we implement the conversion from abstract syntax trees to strings.toString :: Expr -> String toString = sumToString sumToString :: Sum -> String sumToString (Sum product products) = productToString product ++ concatMap ((" + " ++) . productToString) products productToString :: Product -> String productToString (Product atom atoms) = atomToString atom ++ concatMap ((" * " ++) . atomToString) atoms atomToString :: Atom -> String atomToString (Num num) = show num atomToString (Para sum) = "(" ++ sumToString sum ++ ")"
Implementing the parser is now extremely simple.parse :: String -> Expr parse = inverse toString
KiCS2 uses a depth-first search strategy by default. However, our parser implementation does not work with depth-first search. So we switch to breadth-first search by entering
at the KiCS2 prompt. Now we can try out the parser by entering
parse "2 * (3 + 4)" .
Note that our split function is not the same as the split function in Curry’s List module.↩
Tagged: breadth-first search, Curry, Denis Firsov, depth-first search, functional logic programming, functional pattern, functional programming, KiCS2, literate programming, logic programming, parsing, Prolog, Theory Lunch, TTÜ Küberneetika Instituut, type class
Postgresql-simple has been progressing since my last announcement of version 0.1 nearly a year ago. Since then there has been many changes by myself and contributors, some of which will break your code with or without compilation errors. So this post will attempt to highlight some of the bigger changes. Probably the most exciting recent change is the new support for PostgreSQL’s array types, largely due to work from Jason Dusek, Bas van Dijk, and myself. Here’s two examples of a table and query that makes use of this functionality:CREATE TABLE assocs ( id INT NOT NULL , link INT NOT NULL ); CREATE TABLE matrices ( id INT NOT NULL , matrix FLOAT8 ); import qualified Data.Vector as V import Database.PostgreSQL.Simple import Data.Int(Int64) getAssocs :: Connection -> IO [(Int,V.Vector Int)] getAssocs conn = do query_ conn "SELECT id, ARRAY_AGG(link) FROM assocs GROUP BY id" insertMatrix :: Connection -> Int -> V.Vector (V.Vector Double) -> IO Int64 insertMatrix conn id matrix = do execute conn "INSERT INTO matrices (id, matrix) VALUES (?,?)" (id, matrix) TypeInfo Changes
In order to properly support the FromField a => FromField (Vector a) instance, the TypeInfo system was overhauled. Previously, the only information it tracked was a mapping of type OIDs to type names, first by consulting a static table and then using a per-connection cache, finally querying the pg_type metatable. This was useful for writing FromField instances for postgresql types that do not have a stable OID, such as those provided by an extension, like the period type from Temporal Postgres or the hstore type from the contributed modules bundled with PostgreSQL. However, proper array support required more information, especially the type of the array’s elements. This information is now available in an easily extended data structure, available in the new Database.PostgreSQL.Simple.TypeInfo module. This was introduced in 0.3, 0.3.1 added support for range and composite types; however there is not yet any FromField instance that makes use of this information or deals with these types.IO at Conversion Time
Version 0.3 also stopped pre-computing the type name of every column and storing these in a vector before converting the results, by allowing a restricted set of IO actions at conversion time. This is a win, because the common case is that the typename is never consulted; for example almost all of the out-of-box FromField instances examine the type OID alone. Also, since IO information no longer has to be computed before conversion takes place, it makes it practical to consider using IO information that would rarely be used in normal circumstances, such as turning table OIDs into table names when errors are encountered. It’s possible to extend the IO actions available to FromField and FromRow instances by accessing the data constructor of the Conversion monad via the Database.PostgreSQL.Simple.Internal module.
This required changing the type of the FromField.typename operator, which will break your FromField instances that use it. It also required small changes to the FromField and FromRow interface, which has a chance of breaking some of your FromField and FromRow instances if they don’t strictly use the abstract Applicative and/or Monad interfaces. However, all of this breakage should be obvious; if your code compiles, it should work with the new interface.HStore support
Version 0.3.1 also introduced out-of-box support for hstore. The hstore type provides key-value maps from textual strings to textual strings. Conversions to/from lists and Data.Map is provided, while conversions from other Haskell types can be easily implemented via the HStoreBuilder interface (similar to my own json-builder package), and conversions to other Haskell types can easily be implemented via the conversion to lists.CREATE TABLE hstore_example ( id INT NOT NULL , map hstore ); insertHStore :: Connection -> Int -> [(Text,Text)] -> IO Int64 insertHStore conn id map = do execute conn "INSERT INTO hstore_example (id,map) VALUES (?,?)" (id, HStoreList map) retrieveHStore :: Connection -> Int -> IO (Maybe [(Text,Text)]) retrieveHStore conn id xs <- query conn "SELECT map FROM hstore_example WHERE id = ?" (Only id) case xs of  -> return Nothing (Only (HStoreList val):_) -> return (Just val) Better Error Messages
Jeff Chu and Leonid Onokhov have improved both error messages and error handling options in the latest version. Thanks to Jeff, the ResultError exception now includes the column name and associated table OID (if any) from which the column was taken from. And Leonid has contributed a new Errors module that can be used to dissect SqlError values in greater detail.Better Time Conversions
And in older news, version 0.1.4 debuted brand new time parsers and printers for the ISO-8601 syntax flavor that PostgreSQL emits, included FromField instances for LocalTime, and introduced new datatypes for dealing with PostgreSQL’s time infinities. Among other things, the new parsers correctly handle timestamps with UTC offsets of a whole number of minutes, which means (for example) that postgresql-simple now works in India. Version 0.2 removed the conversion from timestamp (without time zone) to the UTCTime and ZonedTime types, due to the inherent ambiguity that conversion represents; LocalTime is now the preferred way of handling timestamps (without time zones).