Type Industry muggle ...

안기영 安基榮 Ahn, Ki Yung

[kyagrd]

Moving to Logdown

Got really annoyed at Markdown parsing errors in Tumblr's web editor.

So moving my blog to http://kyagrd.logdown.com/

Bye Tumblr.

[kyagrd]

n-Queens using MiniZinc

MiniZinc is a high level Constraint Programming (CP) language (or a frontend for constraint programming solvers). Being distributed with its own IDE, it is a most friendly enviornment to have a taste on what constraint programming is. Here is the n-Queens problem, which is like a hello world for CP, in MiniZinc.

include "globals.mzn"; int: n; % fixed integer parameter % (xs[y],y), is a coordiate for a queen array[1..n] of var 1..n: xs; % constraint for the n queens problem on nxn borard constraint alldifferent(xs); constraint forall (i,j in 1..n where i<j) ( j-i != abs(xs[i]-xs[j]) ); solve satisfy; % find satisfying solution output ["Solution:\n", "xs = \(xs) \n", "To pretty-print the chessboard config, use ghci to run:\n", "let xs = \(xs) in putStrLn $ concat $ Data.List.intersperse \"\\n\" [ [if i==k then 'Q' else '#' | k <- ys ] | i<-[1..length xs] ]"];

Note that fixed parameters, which should be initialized before runnning the solver, are declared witout the var keyword and the variables that are to be searched for solutions are declared with the var keyword. This var is in fact part of the type.

And in the IDE it looks like this.

Since we have not initizlied the fixed paramenter n, the IDE will prompt for its value when you run it with Ctrl-R.

The output looks like this for n = 8.

Solution: xs = [3, 6, 4, 2, 8, 5, 7, 1] To pretty-print the chessboard config, use ghci to run: let xs = [3, 6, 4, 2, 8, 5, 7, 1] in putStrLn $ concat $ Data.List.intersperse "\n" [ [if i==k then 'Q' else '#' | k <- ys ] | i<-[1..length xs] ]

Try to pretty-print the result in 2D chessboard configuration using your favorite programming langauge, which is in my case Haskell.

Seems like MiniZinc got a correct solution :)

You actually have to use an external mechanism to print this last step because you cannot use var types where normal types are required. var int is differet from int. The output command only prints strings not var strings. Var is like a stage annotation that contaminates the result once you use it. For instance if you try to print out something that relies on any var value MiniZinc will complain that it is var string not string. If a high level constraint programming lanaguage supported multi-staged computation we could actualy do those kind of things at the last step of printing out a result depending on the solution value.

[kyagrd]

Why Prolog does not have (open ended) set unification built-in

In recent months I have been wondering about why Prolog or other similar logic programming implementations do not generally support (open ended) set unification. There has been a lot of studies on finite set unification, which still didn't seem to make into standardized libraries or common idioms in logic programming, but there are only a few studies on open ended set unification. The reason I started to wonder about this is because I needed a map unification for describing type inference including records, for instance {x:int, y:bool} should be equivalent to {y:bool, x:int}. A simplified problem, ignoring the type annotations, is the set unification, where {x,y} and {y,x} should be considered equivalent.

More generally, in order to handle extensible records, we need open ended unification where the tail (or the rest) of the set is a variable. For example consider unifying a set containing at least x denoted by {x|S1} and a set containing at least y denoted by {y|S2}. We intuitively know that the most general unification for the query ?- {x|S1} = {y|S2}. is S1 = {x|S}, S2 = {y|S} where the substitution for S1 and S2 shares the same tail S. This idea of open ended set unification has already been explored and published by Frieder Stolzenburg (1996). I was able to write this down in Prolog at https://github.com/kyagrd/ExtensibleRecordsWithSetMembLP (see setunify_naive.pl and setunify.pl in the repository) and it seems to work well in Prolog implementations. Therefore, in a way, this is a solved problem. However, this kind of open ended set unification is not wired into Prolog or other logic programming implementations as a primitive built-in unification operation.

So, why haven't open ended sets been wired in as primitive values that could be unified in logic programming paradigm? The short answer to might be that it is hard to come up with an efficient internal representation of open ended sets, especially for nested open ended sets, for instance set of sets. We can deal with unification of open ended list of open ended list (here again open ended mean that the tail could be an uninstantiated logic variable), simply by applying the recursive definition of structural unification and get the most general unifier as the first answer when executing it as a logic program. However, when we are dealing with set of sets, this becomes a bit irritating. Consider the following unification:

?- { {x|S1} | SS1 } = { {y|S2} | SS2 }.

What is the most general unifier of this unification? We can think of two candidates.

First, try the top level open ended set unification without taking consideration that the elements are open ended sets: SS1 = { {y|S2} | SS }, SS2 = { {x|S1} | SS }

Second, considering that elements are open ended sets try unifying the known elements and if that unification of elements succeeds then unify its tail: S1 = {y|S}, S2 = {x|S}, SS1 = SS2

Both are unifiers. Although the latter looks more compact, the former is actually a more "general" unifier in the traditional sense because it represents more possibilities. When we instantiate S1 and S2 in the former as the latter unifier, we effectively get the latter. That is, further instantiating the former unification by S1 = {y|S}, S2 = {x|S}, it is equivalent to the latter because duplication is ignored in sets. Still, when we are in a situation where we eventually want the latter answer, the internal representation of sets could be far from compact by following the algorithm that generates the former. So, there are may be more things to consider to implement such set unification more efficiently when we start supporting unifications of open ended sets in addition to the usual structural unification in a general purpose logic programming system. And from my experience of writing down the algorithms for set unification it is quite difficult to predict whether the algorithm will behave as the former or the latter (or even differently from either of them).

Fortunately, for the problem of type inference involving extensible records, we do not need to consider this set-of-set situation, because the field names of a record are always atomic labels (e.g., x and y in the examples above), not a set, not even a compound structure. But this problem is interesting in itself, and logic programming enthusiasts might want to solve it. Since my current priority is expressing type inference involving record types, I only need one level of set unification on the labels and then the type annotation of that label could be another record and so on. That is, there could be a pattern of alternating structural unification and set unification (which is map unification essentially) but not the set-of-set unification when handling types of records. So, I don't think I can take an initiative to solving this set-of-set unification problem considering efficient implementation right now but happy to discuss who might have an initiative to push forward on this particular problem.

I still need a generic unification opeator for both structural values and set values for type inferenece specifications because type systems with records would have both record types and non-record types (e.g., basic types, function types, ...). In the implementation (internally hacking logic programming implementation based on micorKanren), the tricky part is tying the knot to provide a generic unification operator that could apply for both structural values and set values. The implementation should starting from a structural recursion, and adding a hook that calls open ended set unification when it meets a set constructor. However, the set operations are also defined in terms of a unification operator, so carelessly tying the knot could easily run into an infinite loop. I think I am getting close to tying the knot. I was able to implement set-of-set unification by tying the knot at the membership constraint so that set unification could call set unification for its elements if needed. I havn't gotten to the last step of tying the knot at the structural equality to invoke set unification when it meets the set constructor.

[kyagrd]

Getting started with PureScript 0.7.1.0

Some Triva about PureScript

PureScript is a purely functional language specifically targeting JavaScript as its backend. If you have tasted Haskell and lamenting about the current untyped mess in scripting languages, especially regarding web-programming, probabiy your only choice out there is PureScript.

PureScript is the only language with a sane approch to staticaly support duck typing on records by using Row Polymorphism.

In addition, PureScript supports Extensible Effects with the same mechanism, using Row Polymorphism. Monads are labeled with effects (e.g. console for console I/O) in PureScript. This greatly reduces the problem of excessive transformer stack-up when composing Haskell monadic libraries simply for combining effects in obvious ways.

Short note for new PureScript users (like me)

This is a short note for those who want to try PureScript, who are already familliar with GHC and cabal. PureScript is relatively well documented, but for newbies it could be confusing because updated documents for the recent version 0.7.1.0 are scatterred around several URLs and the e-book and several other documents on the web is written based on the older version.

Installing PureScript is easy if you have installed cabal for installing PureScript and npm for installing JavaScript packages, especially for installing pulp (package dependency manangment/sandboxing for PureScript). Since purescript is implemented in Haskell, I felt it most natural to use cabal because I am GHC user. But you don't have to have GHC and cabal installed in fact. There are also binary distribtions directly downlodable or via other binary packge managers from the PureScript homepage; see http://www.purescript.org/download/ for more informtion. I'll just stick to cabal in this document.

You can install PureScript in any system cabal runs.

cabal install purescript

For npm and pulp,

You'd do somthing like this on Mac OS X

brew install npm npm install -g pulp

and on Debian-based linux systems

sudo apt-get install npm npm install pulp

Most users of Mac OS X would have Admin rights so it is most reasonlable to install pulp globalally in the system. The PureScript binary files should be installed in ~/.cabal/bin and you should have already added ~/.cabal/bin to your PATH already if you are a sensible GHC user. Since you've installed pulp globally with -g option, it should also be in your PATH. Note that installing pulp can take a while, especially when you have freshly installed npm, because it installs all its dependencies.

Altough you can sudo install -g pulp on linux systems, if you are in sudo group, it is usually not recommended in linux systems. So, just install it locally and set up some additional path in bashrc or whatever shell configuration file you use. In some linux distros, such as Debian, the executable filename for the "node.js" is named as nodejs rather than node in most other systems. So, you'd have to make a symbolic link in one of your PATH anyway. The pulp package mananager for PureScript also tries to find node. Anyway this is what I did in Debian after installing pulp locally. The npm pacakge manager for JavaScript on Debian installs user packages into ~/npm_modules directory and its binary/executable files are symlinked into ~/npm_modules/.bin directory.

kyagrd@debair:~$ ls -al node_modules/ total 16 drwxr-xr-x 4 kyagrd kyagrd 4096 Aug 2 22:30 . drwxr-xr-x 33 kyagrd kyagrd 4096 Aug 3 00:01 .. drwxr-xr-x 2 kyagrd kyagrd 4096 Aug 3 00:00 .bin drwxr-xr-x 4 kyagrd kyagrd 4096 Aug 2 22:29 pulp kyagrd@debair:~$ ls -al node_modules/.bin total 8 drwxr-xr-x 2 kyagrd kyagrd 4096 Aug 3 00:00 . drwxr-xr-x 4 kyagrd kyagrd 4096 Aug 2 22:30 .. lrwxrwxrwx 1 kyagrd kyagrd 15 Aug 3 00:00 node -> /usr/bin/nodejs lrwxrwxrwx 1 kyagrd kyagrd 16 Aug 2 22:30 pulp -> ../pulp/index.js

So, this is a good place to stick in the renamed symlink for "node.js". (If you don't like it here you can put it in anywhere else say ~/bin and add it to your PATH.)

kyagrd@debair:~$ ln -s /usr/bin/nodejs ~/node_modules/.bin/node kyagrd@debair:~$ ls -al node_modules/.bin total 8 drwxr-xr-x 2 kyagrd kyagrd 4096 Aug 3 00:00 . drwxr-xr-x 4 kyagrd kyagrd 4096 Aug 2 22:30 .. lrwxrwxrwx 1 kyagrd kyagrd 15 Aug 3 00:00 node -> /usr/bin/nodejs lrwxrwxrwx 1 kyagrd kyagrd 16 Aug 2 22:30 pulp -> ../pulp/index.js

Now we're done with all the tedious stuff and have fun.

kyagrd@debair:~$ mkdir pursproj kyagrd@debair:~$ cd pursproj/ kyagrd@debair:~/pursproj$ pulp init * Generating project skeleton in /home/kyagrd/pursproj bower cached git://github.com/purescript/purescript-console.git#0.1.0 bower validate 0.1.0 against git://github.com/purescript/purescript-console.git#^0.1.0 bower cached git://github.com/purescript/purescript-eff.git#0.1.0 bower validate 0.1.0 against git://github.com/purescript/purescript-eff.git#^0.1.0 bower cached git://github.com/purescript/purescript-prelude.git#0.1.1 bower validate 0.1.1 against git://github.com/purescript/purescript-prelude.git#^0.1.0 bower install purescript-console#0.1.0 bower install purescript-eff#0.1.0 bower install purescript-prelude#0.1.1 purescript-console#0.1.0 bower_components/purescript-console └── purescript-eff#0.1.0 purescript-eff#0.1.0 bower_components/purescript-eff └── purescript-prelude#0.1.1 purescript-prelude#0.1.1 bower_components/purescript-prelude

The pulp init command creates a template PureScript project for you. To see other command of pulp, you can pulp --help.

Usage: /home/kyagrd/node_modules/.bin/pulp [options] [command-options] Global options: --bower-file -b Read this bower.json file instead of autodetecting it. --help -h Show this help message. --monochrome Don't colourise log output. --then Run a shell command after the operation finishes. Useful with `--watch`. --version -v Show current pulp version --watch -w Watch source directories and re-run command if something changes. Commands: browserify Produce a deployable bundle using Browserify. build Build the project. dep Invoke Bower for package management. docs Generate project documentation. init Generate an example PureScript project. psci Launch a PureScript REPL configured for the project. run Compile and run the project. test Run project tests. Use `/home/kyagrd/node_modules/.bin/pulp --help` to learn about command specific options.

We can try run and test commands

kyagrd@debair:~/pursproj$ pulp run * Building project in /home/kyagrd/pursproj * Build successful. Hello sailor! kyagrd@debair:~/pursproj$ cat src/Main.purs module Main where import Control.Monad.Eff.Console main = do log "Hello sailor!" kyagrd@debair:~/pursproj$ pulp test * Building project in /home/kyagrd/pursproj * Build successful. Running tests... You should add some tests. * Tests OK. kyagrd@debair:~/pursproj$ cat test/Main.purs module Test.Main where import Control.Monad.Eff.Console main = do log "You should add some tests." kyagrd@debair:~/pursproj$

The run and test command invokes build command before running or testing if the project has not been built yet.

One last thing is about editing the "bower.json" file. The pulp package manager for PureScript uses bower (a local sandboxing package manager for javascirpt packages and also used for purescript cuase purescript package seems to be desinged to be compatible with javascript package versioning/dpenecy convention) to locally sandbox all its dependencies in the bower_compnents directory. I think for beginners like me, the only thing to edit is the dependency section.

kyagrd@debair:~/pursproj$ ls bower.json bower_components output src test kyagrd@debair:~/pursproj$ cat bower.json { "name": "pursproj", "version": "1.0.0", "moduleType": [ "node" ], "ignore": [ "**/.*", "node_modules", "bower_components", "output" ], "dependencies": { "purescript-console": "^0.1.0" } }

The dependices section of the default "bower.json" created by invoking pulp init only contains the purescript-console package. As you need to use more library packages, you can list them in the dependencies section. There is a list of most commonly used basic packages (of course including purescript-console) combined as a sort of meta-package called purescript-base. We can edit the depenecy section, instead of purescript-console change it to purescript-base. Because purescript-base depends on purescript-console, it is redundent to specify purescript-console when there is purescript-base. The current version of purescript-base is 0.1.0, which happens to be same as the version of purescript-console.

So, change it like this and then install all its depending packages using pulp dep install (which invokes bower install). It sure does install more packages than before.

kyagrd@debair:~/pursproj$ vi bower.json ### edit with text editor kyagrd@debair:~/pursproj$ cat bower.json { "name": "pursproj", "version": "1.0.0", "moduleType": [ "node" ], "ignore": [ "**/.*", "node_modules", "bower_components", "output" ], "dependencies": { "purescript-base": "^0.1.0" } } kyagrd@debair:~/pursproj$ pulp dep install bower cached git://github.com/purescript-contrib/purescript-base.git#0.1.0 bower validate 0.1.0 against git://github.com/purescript-contrib/purescript-base.git#^0.1.0 bower cached git://github.com/purescript/purescript-arrays.git#0.4.1 bower validate 0.4.1 against git://github.com/purescript/purescript-arrays.git#^0.4.0 bower cached git://github.com/purescript/purescript-control.git#0.3.0 bower validate 0.3.0 against git://github.com/purescript/purescript-control.git#^0.3.0 bower cached git://github.com/purescript/purescript-either.git#0.2.0 bower validate 0.2.0 against git://github.com/purescript/purescript-either.git#^0.2.0 bower cached git://github.com/purescript/purescript-enums.git#0.5.0 bower validate 0.5.0 against git://github.com/purescript/purescript-enums.git#^0.5.0 bower cached git://github.com/purescript/purescript-foldable-traversable.git#0.4.0 bower validate 0.4.0 against git://github.com/purescript/purescript-foldable-traversable.git#^0.4.0 bower cached git://github.com/paf31/purescript-lists.git#0.7.0 bower validate 0.7.0 against git://github.com/paf31/purescript-lists.git#^0.7.0 bower cached git://github.com/purescript/purescript-math.git#0.2.0 bower validate 0.2.0 against git://github.com/purescript/purescript-math.git#^0.2.0 bower cached git://github.com/purescript/purescript-maybe.git#0.3.3 bower validate 0.3.3 against git://github.com/purescript/purescript-maybe.git#^0.3.0 bower cached git://github.com/purescript/purescript-monoid.git#0.3.0 bower validate 0.3.0 against git://github.com/purescript/purescript-monoid.git#^0.3.0 bower cached git://github.com/purescript/purescript-strings.git#0.5.5 bower validate 0.5.5 against git://github.com/purescript/purescript-strings.git#^0.5.0 bower cached git://github.com/purescript/purescript-tuples.git#0.4.0 bower validate 0.4.0 against git://github.com/purescript/purescript-tuples.git#^0.4.0 bower cached git://github.com/paf31/purescript-unfoldable.git#0.4.0 bower validate 0.4.0 against git://github.com/paf31/purescript-unfoldable.git#^0.4.0 bower cached git://github.com/purescript/purescript-integers.git#0.2.1 bower validate 0.2.1 against git://github.com/purescript/purescript-integers.git#^0.2.0 bower cached git://github.com/purescript/purescript-st.git#0.1.0 bower validate 0.1.0 against git://github.com/purescript/purescript-st.git#^0.1.0 bower cached git://github.com/purescript-contrib/purescript-bifunctors.git#0.4.0 bower validate 0.4.0 against git://github.com/purescript-contrib/purescript-bifunctors.git#^0.4.0 bower cached git://github.com/purescript/purescript-lazy.git#0.4.0 bower validate 0.4.0 against git://github.com/purescript/purescript-lazy.git#^0.4.0 bower cached git://github.com/purescript/purescript-invariant.git#0.3.0 bower validate 0.3.0 against git://github.com/purescript/purescript-invariant.git#^0.3.0 bower install purescript-base#0.1.0 bower install purescript-arrays#0.4.1 bower install purescript-either#0.2.0 bower install purescript-control#0.3.0 bower install purescript-enums#0.5.0 bower install purescript-foldable-traversable#0.4.0 bower install purescript-lists#0.7.0 bower install purescript-math#0.2.0 bower install purescript-maybe#0.3.3 bower install purescript-monoid#0.3.0 bower install purescript-strings#0.5.5 bower install purescript-tuples#0.4.0 bower install purescript-unfoldable#0.4.0 bower install purescript-st#0.1.0 bower install purescript-integers#0.2.1 bower install purescript-bifunctors#0.4.0 bower install purescript-lazy#0.4.0 bower install purescript-invariant#0.3.0 purescript-base#0.1.0 bower_components/purescript-base ├── purescript-arrays#0.4.1 ├── purescript-console#0.1.0 ├── purescript-control#0.3.0 ├── purescript-either#0.2.0 ├── purescript-enums#0.5.0 ├── purescript-foldable-traversable#0.4.0 ├── purescript-integers#0.2.1 ├── purescript-lists#0.7.0 ├── purescript-math#0.2.0 ├── purescript-maybe#0.3.3 ├── purescript-monoid#0.3.0 ├── purescript-strings#0.5.5 ├── purescript-tuples#0.4.0 └── purescript-unfoldable#0.4.0 purescript-arrays#0.4.1 bower_components/purescript-arrays ├── purescript-foldable-traversable#0.4.0 ├── purescript-st#0.1.0 └── purescript-tuples#0.4.0 purescript-either#0.2.0 bower_components/purescript-either └── purescript-foldable-traversable#0.4.0 purescript-control#0.3.0 bower_components/purescript-control └── purescript-prelude#0.1.1 purescript-enums#0.5.0 bower_components/purescript-enums ├── purescript-either#0.2.0 ├── purescript-strings#0.5.5 └── purescript-unfoldable#0.4.0 purescript-foldable-traversable#0.4.0 bower_components/purescript-foldable-traversable ├── purescript-bifunctors#0.4.0 └── purescript-maybe#0.3.3 purescript-lists#0.7.0 bower_components/purescript-lists ├── purescript-foldable-traversable#0.4.0 ├── purescript-lazy#0.4.0 └── purescript-unfoldable#0.4.0 purescript-math#0.2.0 bower_components/purescript-math purescript-maybe#0.3.3 bower_components/purescript-maybe └── purescript-monoid#0.3.0 purescript-monoid#0.3.0 bower_components/purescript-monoid ├── purescript-control#0.3.0 └── purescript-invariant#0.3.0 purescript-strings#0.5.5 bower_components/purescript-strings └── purescript-maybe#0.3.3 purescript-tuples#0.4.0 bower_components/purescript-tuples └── purescript-foldable-traversable#0.4.0 purescript-unfoldable#0.4.0 bower_components/purescript-unfoldable ├── purescript-arrays#0.4.1 └── purescript-tuples#0.4.0 purescript-st#0.1.0 bower_components/purescript-st └── purescript-eff#0.1.0 purescript-integers#0.2.1 bower_components/purescript-integers ├── purescript-math#0.2.0 └── purescript-maybe#0.3.3 purescript-bifunctors#0.4.0 bower_components/purescript-bifunctors └── purescript-control#0.3.0 purescript-lazy#0.4.0 bower_components/purescript-lazy └── purescript-monoid#0.3.0 purescript-invariant#0.3.0 bower_components/purescript-invariant └── purescript-prelude#0.1.1

There are several tutorial examples online. Many of them should be doable by editing the src/Main.purs file. Ones that actually runs on browsers would need to use pulp browserify, which outputs single file that contains self contained javascript code. We can do it for this template project too (you need to check developer console for the output though).

kyagrd@debair:~/pursproj$ pulp browserify > index.js * Browserifying project in /home/kyagrd/pursproj * Building project in /home/kyagrd/pursproj * Build successful. * Browserifying... kyagrd@debair:~/pursproj$ cat > index.html <html> <head> <title>Example purescript app</title> <meta charset="UTF-8"> </head> <body> Check the console <script type="text/javascript" src="index.js"></script> </body> </html> kyagrd@debair:~/pursproj$ ls bower.json bower_components index.html index.js output src test

Load "index.html" in a browser that supports a deveolper console like Firefox. Every time you load "index.html" you can see the console log printing "hello sailor!", just as it did when we pulp run on the command line console.

Happy PureScript-ing!

[kyagrd]

An example of higher-kinded polymorphism not involving type classes

We almost always explain higher-kinded polyomrphism (a.k.a. type constructor polymorphism) in Haskell with an example involving type classes such as Monad. It is natural to involve type classes because type classes were the motivation to support type constructor polymoprhism in Haskell. However, it is good to have an example that highlights the advantage of having higher-kinded polymorphism, because type constructor variables are not only useful for defining type classes. Here is an example I used in my recent draft of a paper to describe what type constructor polymorphism is and how they are useful.

data Tree c a = Leaf a | Node (c (Tree c a)) newtype Pair a = Pair (a,a) type BTree a = Tree Pair a type RTree a = Tree [] a

The ability to abstract over type constructors empowers us to define more generic data structures, such as Tree, that can be instantiated to well-knwon data structures, such as BTree (binary tree) or RTree (rose tree). The Tree datatype is parametrized by c :: * -> *, which determines the branching structure at the nodes, and a :: *, which determines the type of elemenets hanging on the leaves. By instantiating the type construcor variable c, we get concrete tree data structures, which we would define sparately as follows without type constructor polymophism, but only with type polymorphism:

data BTree a = BLeaf a | BNode (BTree a, BTree a) data RTree a = RLeaf a | RNode [RTree a]

[kyagrd]

HM+HigherKindedPoly+KindPoly in 25 lines of hacky Prolog

Previously, I posted about 7-liner Hindley--Milner type inference written in Prolog.

http://kyagrd.tumblr.com/post/120536318024/hindley-milner-in-7-lines-of-hacky-prolog

Today I've managed to extend it to support higher-kinded polymorphism (a.k.a. type constructor polymorphsim) and kind polymorphism (of couse, both rank 1).

https://gist.github.com/kyagrd/0ba0761263bc60a60432

It is only 25 lines, but I left out pattern matching expressoins because there could be several differnt design choices (e.g. nested pattern support). As long as we are dealing with regular datatypes only, type inference for pattern matching shouldn't be fundamentally complicated.

One trick I had to come up with is delaying the kind sanity check for function type introduction. If you just call on kind/3 inside type(..., A->B, ...), either one or both of A and B may contain variables that would later be further speciallized and we don't have enough information for kind checking.

[kyagrd]

Hindley--Milner in 7 lines of hacky Prolog

While ago, I wrote a 8-liner Curry program of STLC type inference. (6 lines excluding datatype declearation)

http://www-ps.informatik.uni-kiel.de/smap/smap.cgi?browser/31 http://kyagrd.tumblr.com/post/103510371489/stlc-type-inference-in-8-lines-of-curry

There is a 7 liner Prolog for Hindley--Milner! (I didn't write this but stumbled across while web searching)

http://lpaste.net/65035

This 7-liner is not pure Prolog 'cuase it uses copy_term/2 to implement instantiation of polymorphic types.

I wonder how much this would scale up. I think it should work up to type constructor polymorphism for regular ADTs in functional languages, and may also be able to add top-level rank-1 kind polymorphism on top of that. But it might get messy once you start to throw in non-regular datatypes and even worse when GADTs come along.

[kyagrd]

Some quick thoughts on a restriceted form of kind polymophism

It is well known that adding unrestricted kind polymorphism to the higher-order polymorphic lambda calculus, a.k.a. System $ F_\omega $, leads to logically inconsistent paradoxes. For those in dependently typed theorem proving community, this is non of their concern, since dependently typed proof assistants are usually based on predicative calculus with stratified universes. However, there is an alternative approach that has not been well explored yet.

Consider taking an alternative approach of starting from a more traditional functional language based on impredicative polymorphism and turning that into a theorem proving system. For instance consider a certain subset of Haskell with GHC extensions such as RankNTypes and ImpredicativeTypes (after all, core of GHC is an extension of $ F_\omega $ ), and trying to carve out a logically consistent language. This is exactly the motivation of my Ph.D. thesis, and its resulting artifact is the Nax language. To make the long story short, we should be able to have a logically consistent subset of say Haskell with GHC extension including GADTs and PolyKind. The benefit of such design is that we can reuse all the facilities that have already been built around functional languages like Haskell, which has far more sophisticated and well-optimized compilers than most theorem proving systems.

If we take this route, we should figure out a safe way to extend impredicative polymorphism with a restricted form of kind polymorphism. I believe that extending $ F_\omega $ with Rank 1 polymorphic kind bindings for finite number of globally defined type constructor variables is safe. That is, the resulting calculus with this extension is logically consistent. Proof of logical consistency of this extended calculus should be quite straightforward by mapping the extended calculus back into $ F_\omega$ by inlining.

Here is the syntax of the extended calculus: $$ \sigma ::= \kappa \mid \forall \chi.\kappa $$ $$ \kappa ::= \chi \mid * \mid \kappa \to \kappa' $$ $$ A, B, F, G ::= X \mid A \to B \mid \lambda X^{\kappa}.F \mid F~G \mid \forall X^{\kappa}.B $$ $$ \Sigma ::= \cdot \mid T^\sigma,\Sigma $$ $$ \Gamma ::= \cdot \mid X^{\kappa} \mid x:A $$ $$ t, r, s ::= x \mid \lambda x.t \mid r~s $$

A type constructor name $T$ is no different than a type variable $X$. It is just a notional convention to emphasize that the variable stands for a globally defined name for a type constructor. From a list of globally defined type constructors $ T_1 = F_1, T_2 = F_2, \ldots, T_n = F_n $ a global context $\Sigma$ can be obtained such that $ \Sigma = T_1^{\sigma_1}, T_2^{\sigma_2}, \ldots, T_n^{\sigma_n} $ Each $\sigma_i$ is a polymorphic kind of $F_i$. For instance, the polymorphic kind scheme of $F_1 = \lambda X^{\chi}.X$ is $\sigma_1 = \forall \chi.\chi \to \chi$.

For simplicity, let us consider just one global definition where $T_1 = F_1$. Assuming $F_1$ is well kinded, we get $\Sigma = T_1^{\sigma_1]}$. In the derivation tree of a typing judgment $ T_1^{\sigma_1};\Gamma \vdash t : A $, we inline each occurrence of $T_1$ with an instantiation of its definition $F_1$, instantiating all the free kind variables in $F_1$ appropriately for each occurrence. For instance, if we had $F_1 = \lambda X^{\chi}.X$, we might instantiate it to $ \lambda X^{*}.X$, $ \lambda X^{ * \to * }.X$, or any appropriate instantiation of $\chi$ as needed. Once we have inlined every occurrence of $T_1$, the global context $\Sigma$ becomes irrelevant. Therefore, we can simply ignore $\Sigma$, and the resulting derivation tree is exactly the derivation tree for a typing judgment in $ F_\omega $.

Generalizing the inlining for $n$ definitions is not so hard. The only additional thing to consider is that the previously defined type constructor names can be used in the latter definitions. Consider $ T_1 = F_1, T_2 = F_2, \ldots, T_n = F_n $. The first name $T_1$ can appear in any of $F_2, \ldots, F_n$. So, inlining should be performed in a cascading manner starting from $T_1$, inlining inside $\Sigma$ as well as other parts of the derivation tree.

Next step is to generalize this idea for System $F_i$ which extends System $ F_\omega $ with erasable type indices. Here, this will get more complicated because type variables and term-index variables can appear in kinds as well as kind variables.

[kyagrd]

STLC type inference in 8 lines of Curry

The beauty of functional logic programming where unification is natively supported. I'm curious how this would scale up to HM.

data Ty = Iota | Arr Ty Ty data Tm = Var String | App Tm Tm | Lam String Tm infer ctx (Var x) = case lookup x ctx of Just t -> t Nothing -> error (x ++ " undefined") infer ctx (App e1 e2) | infer ctx e2 `Arr` t =:= infer ctx e1 = t where t free infer ctx (Lam x e) = t `Arr` infer ((x,t):ctx) e where t free

This actually runs in PAKCS well as below. There are some strange warnings from the prolog side, which I have no idea what they are about. And, I don't really handle errors so messages when unification fails are not good of course.

______ __ _ _ ______ _______ | __ | / \ | | / / | ____| | _____| Portland Aachen Kiel | | | | / /\ \ | |_/ / | | | |_____ Curry System | |__| | / /__\ \ | _ | | | |_____ | | ____| / ______ \ | | \ \ | |____ _____| | Version 1.11.4 (4) |_| /_/ \_\ |_| \_\ |______| |_______| Curry2Prolog(swi 6.6) Compiler Environment (Version of 2014-11-22) (RWTH Aachen, CAU Kiel, Portland State University) Type ":h" for help (contact: [email protected]) Prelude> :l a [1 of 2] Skipping Prelude ( /home/kyagrd/cscs/pakcs/lib/Prelude.curry, /home/kyagrd/csc s/pakcs/lib/.curry/Prelude.fcy ) [2 of 2] Compiling a ( a.curry, .curry/a.fcy ) > :define x=Var "x" > :define y=Var "y" > :define z=Var "z" > infer [] (Lam "x" x) Arr _a _a > infer [] (Lam "x" (Lam "y" (Lam "z" (App (App x z) (App y z))))) Warning: /tmp/pl_pakcs_file_18510_8/.curry/pakcs/PAKCS_Main_Exp.pl:23: Redefined static procedure PAKCS_Main_Exp.pakcsMainGoal/3 Previously defined at /tmp/pl_pakcs_file_18510_7/.curry/pakcs/PAKCS_Main_Exp.pl:23 Warning: /tmp/pl_pakcs_file_18510_8/.curry/pakcs/PAKCS_Main_Exp.pl:24: Redefined static procedure blocked_PAKCS_Main_Exp.pakcsMainGoal/3 Previously defined at /tmp/pl_pakcs_file_18510_7/.curry/pakcs/PAKCS_Main_Exp.pl:24 Arr (Arr _a (Arr _b _c)) (Arr (Arr _a _b) (Arr _a _c)) > infer [] (Lam "x" (App x x )) Warning: /tmp/pl_pakcs_file_18510_10/.curry/pakcs/PAKCS_Main_Exp.pl:23: Redefined static procedure PAKCS_Main_Exp.pakcsMainGoal/3 Previously defined at /tmp/pl_pakcs_file_18510_8/.curry/pakcs/PAKCS_Main_Exp.pl:23 Warning: /tmp/pl_pakcs_file_18510_10/.curry/pakcs/PAKCS_Main_Exp.pl:24: Redefined static procedure blocked_PAKCS_Main_Exp.pakcsMainGoal/3 Previously defined at /tmp/pl_pakcs_file_18510_8/.curry/pakcs/PAKCS_Main_Exp.pl:24 *** No value found!

Src also availiable at http://www-ps.informatik.uni-kiel.de/smap/smap.cgi?browser/31

[kyagrd]

The Nax language (dissertation and slides)

I made the draft of my dissertation and the slides used for the thesis defense available online.

P.S. In addtion, I'm also providing a single space version of my dissertaion. Our school's thesis format is double line space, but I find sinle line spacing (in fact 1.2 space) is more readable.

[kyagrd]

Test to see how FB->Twitter link would work

Tumbr forwards both to FB and Twitter, now since I set up FB->Twitter, I think Tiwtter is going to have an echo ...

That's what I thought but apparently, there is no echo on twitter. Either Tumblr or FB is smart enough :)

[kyagrd]

I only had 10 posts?!

[kyagrd]

Got a MacBook Air, played with it for a week

Since I am planning to graduate this year, I thought it is a good time to finally get a laptop from Apple when I still have a student discount. Another purpose of it was using Keynote to make presentations effectively. Mac OS X is the only sensible desktop environment that supports GUI engine that can handle vector graphics properly. One can grab a figure, formula, table, etc. from a PDF and just paste into a presentation slide and scale it without worrying about blurring. This is really great for LaTeX users because one just reuse the contents from a paper, don't have to recreate snippets re-formatted for slides. I had old mac mini that looked like a white bento-box from about 2007, made few slides with it and was very satisfied. Now, I it got too slow for new software and cannot even upgrade it, so I got a brand new machine, 11'' MacBook Air with 256GB SSD. The minimum amount of128GB is about $100 less, but I really need to use Linux (either via virtual machine or dual boot), so more storage was inevitable. There are packaging systems OS X ports of software mainly targeted for Linux, but I was never satisfied with it, unfortunately. I heard that there a better option came up recently called homebrew, but still, I can't get used to the keybindings using command rather than control and all those things :(

I like the hardware, of course. Fine looking aluminum, high-quality display (11'' didn't feel that small), and Apple's touch pad is no comparison to other laptops. It's first time using SSD sotrate, and it seemed to work faster than HDD. So, even though it does not have high-computing power in the CPU, it wouldn't feel that slow compared to machines with higher-end CPU's with HDD. I don't have serious graphic/video/audio tasks, so it's fine for me. When using a virtual machine, SSD definitely wins. And it uses less battery as well.

The Keynote for iCloud is great as well. You can edit the contents of your (or others' shared to you for editing) presentation online, even in non-Mac machines; although it works best with Safari, a lot of jobs are doable in Firefox as well (e.g., fix typos, edit text, minor layout changes, add new slides, and so on). One problem I had with iCloud Keynote is that it does not properly scale vector image, just stretches out and makes it blur. So, if you use vector graphic source images like eps or pdf format, don't try to present it through web-browser but stick to Keynote for presentation.

Other than Keynote and web-browsing, I tend to work inside Debian linux running on virtualbox. Since I don't need much of graphic acceleration, I'm currently happy with visualized Linux environment; I think SSD makes it feel less that it is a virtual machine than running guest OS on HDD.

[kyagrd]

Mendler-style recursion schemes for mixed-variant datatypes

A draft of a new paper on Menlder-style recursion schemes (in consideration to submit to TYPES'14 post-proceedings) is available online, powered by ShareLaTeX. We'd appreciate any feedback.

This paper contains a bug fix for $mcata_1$ (or $\it\text{msf}it_{\star\to\star}$ in this paper) in "A hierarchy of Mendler-style recursion schemes", an interesting example of its use over an indexed mixed-variant datatype, and more rigorous theoretic elaboration of its $F_\omega$ embedding.

Moreover, we introduce ongoing work of two new Mendler-style recursion scheme. One of them is Mendler-style iteration over Parametric Higher-Order Abstract Syntax (PHOAS), inspired by Parametric Compositional Data Types (PCDT). We named our recursion scheme $\it\text{mphit}$, which stands for Mendler-style parametric higher-order iteration. I'll perhaps write a separate post on this.

[kyagrd]

Interactive Haskell on the web

tryhaskell.org uses a patched version of mueval library and console library, and the famouse javascript library jQuery. So, it is based on GHC, but can only run limited things, which mueval allows.

codepad.org is based on Hugs.

fpcomplete.com seems to be using GHC and its web freamwork is yesod, but not exactly sure what its implementation is based on. This is the most comprehensive authoring page that supports interactive Haskell environment on the web.

[kyagrd]

Programming with term-indexed types in Nax

Our draft (submitted for the IFL’12 post-proceeding review process) explores a language design space to support term-indexed datatypes along the lines of the lightweight approach, promoted by the implementation of GADTs in major functional programming languages (e.g., GHC, OCaml). Recently, the Haskell community has been exploring yet another language design space, datatype promotion (available in recent versions of GHC), to support term-indexed datatypes.

In this draft, we discuss similarities and differences between these two design spaces that allow term-indices in languages with two universes (star and box) and no value dependencies. We provide concrete examples written in Nax, Haskell (with datatype promotion), and Agda, to illustrate the similarities and differences.

“Nax’s term-indices vs. Haskell’s datatype promotion” corresponds to “Universe Subtyping vs. Universe Polymorphism” in Agda. Nax can have nested term indices. That is, we can use terms of already indexed types (e.g. length indexed lists, singleton types) as indices in Nax, while we cannot in Haskell’s datatype promotion (as it is now in GHC 7.6). On the other hand, Haskell’s datatype promotion allows type-level data structures containing types as elements (e.g. List *).

You can read further details in our draft below: http://nax.googlecode.com/svn/trunk/draft/IFL12/IFL12draft.pdf

P.S. In addition to supporting term indices, Nax is designed to be logically consistent in the Curry—Howard sense and to support Hindley—Milner-style type inference. These two important characteristics of Nax are out of the scope of this draft, but to be published soon and will also appear in my dissertation. 

Unfortulately, this was rejected for the post-preceeding but it will still apear in my thesis (which I'm really trying hard to finish up soon) and looking for other venues to submit a revised version.

[kyagrd]

List-like things in Conor's talk at ICFP 2012 into Haskell

In Conor's keynote talk at ICFP 2012, he uses a generic list like thing in Agda, which generalizes over regular lists, length indexed lists, and even more complicated things. It is done by indexing the data structure with relations of kind (A -> A -> *) rather than just a value. With the help of GHC's newest super hot datatype promotion and kind polymorphism this already type checks!!! (I checked this in GHC 7.4.1 but it should work in GHC 7.6.x as well.)

{-# LANGUAGE KindSignatures, GADTs, DataKinds, PolyKinds #-} -- list like thing in Conor's talk into Haskell! data List x i j where   Nil  :: List x i i   Cons :: x i j -> List x j k -> List x i k append :: List x i j -> List x j k -> List x i k append Nil         ys = ys append (Cons x xs) ys = Cons x (append xs ys) -- instantiating to a length indexed list data Nat = Z | S Nat data VecR a i j where MkVecR :: a -> VecR a ('S i) i type Vec a n = List (VecR a) n 'Z vNil :: Vec a 'Z; vNil = Nil vCons :: a -> Vec a n -> Vec a ('S n) vCons = Cons . MkVecR -- instantiating to a plain list data R a i j where MkR :: a -> R a '() '() type PlainList a = List (R a) '() '() nil :: PlainList a nil = Nil cons :: a -> PlainList a -> PlainList a cons = Cons . MkR

Additional note:

You can go on and define Inst datatype for instructions. However, in GHC 7.4.1, you cannot write the compile function that compiles expressions to instructions because Haskell does not have stratified universes. GHC 7.4.1 will give you an error that says BOX is not *. I heard that *:* will be added go GHC at one point, so, it may work in more recent versions.

{-# LANGUAGE KindSignatures, GADTs, DataKinds, PolyKinds #-} {-# LANGUAGE TypeOperators #-} data Ty = I | B data Val t where  IV :: Int -> Val I  BV :: Bool -> Val B plusV :: Val I -> Val I -> Val I plusV (IV n) (IV m) = IV (n + m) ifV :: Val B -> Val t -> Val t -> Val t ifV (BV b) v1 v2 = if b then v1 else v2 data Expr t where  VAL :: Val t -> Expr t  PLUS :: Expr I -> Expr I -> Expr I  IF :: Expr B -> Expr t -> Expr t -> Expr t eval :: Expr t -> Val t eval (VAL v) = v eval (PLUS e1 e2) = plusV (eval e1) (eval e2) eval (IF e e1 e2) = ifV (eval e) (eval e1) (eval e2) data Inst :: [Ty] -> [Ty] -> * where   PUSH  :: Val t -> Inst ts (t ': ts)   ADD   :: Inst ('I ': 'I ': ts) ('I ': ts)   IFPOP :: GList Inst ts ts' -> GList Inst ts ts' -> Inst ('B ': ts) ts' compile :: Expr t -> GList Inst ts (t ': ts) compile (VAL v) = undefined -- Cons (PUSH v) Nil                 -- I am stuck here {- GListLike.hs:32:19:  -     Couldn't match kind `BOX' against `*'  -     Kind incompatibility when matching types:  -       k0 :: BOX  -       [Ty] :: *  -     In the return type of a call of `Cons'  -     In the expression: Cons (PUSH v) Nil  -}

It turns out that this Conor's example is a very nice example that highlights the differences between GHC's datatype promotion and the Nax language approach (or System Fi, which I posted earlier). I'll try to explain the difference in the IFL 2012 post-proceeding, but in a nutshell, System Fi needs neither *:* (which causes logical inconsistency) nor stratified universes to express Conor's example of the stack-shape indexed compiler. (Or, we may say that Fi typing context split into two parts somehow encode certain uses of stratified universes) Anyway, I see no problem of writing that code in Nax.

However, we do not have polymorphism at kind level in System Fi, so we cannot express GList, but only specific instances of GList instantiated to some specific x. I do have some rough thoughts that HM-style polymorphism at kind level won't cause logical inconsistencies, but haven't worked out the details.