Type industry muggle ...

## Getting started with PureScript 0.7.1.0

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...
* 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!

## 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]


## 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.

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.

## 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 *).

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.

## 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

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.

## Indentation aware parsing for Haskell-like blocks

Use indentparser (unless prefer libraries staring with “uu” prefix). It is the only choice on hackage compatible with Parsec, and it’s pretty good – follows the style of Parsec library and defined as general as it needs to be and its basic framework just looks right. There are other two indentation aware parsers on hackage but one seems obsolete and the other is not as beautiful as this one.

However, there is one small problem. You need to build your own combinator using some of their token parsers. The library provided combinator “braceBlock” almost works but not what you want (I think it is a bug rather than a feature.). The braceBlock combinator lets you parse both

item
item
item

and

{ item; item; item;
item; item
}

but not this one below

{ item; item; item;
item; item }

which is what you do want to parse as a block.

So, what you need to do is to define something like this

blockOfmany p = braces (semiSep p) <|> blockOf (many p)

and to a parser for a do block can be defined as follows

doP = keyword “do” >> blockOfmany commadP

where keyword and commandP should be properly built up using their indentation aware token parsers and combinators.

## Untyped de Bruijn lambda term evaluator using datatype promotion in GHC

{-# LANGUAGE GADTs, DataKinds, PolyKinds, KindSignatures, TypeOperators,
RankNTypes, FlexibleInstances
#-}

data V a = Vfun (V a -> V a) | Vinv a -- user should never use Vinv

type Val = V ([String] -> String)

showV :: V ([String] -> String) -> [String] -> String
showV (Vfun f) (x:xs) = "(\\"++x++"."++showV (f (Vinv $const x)) xs++")" showV (Vinv g) xs = g xs showVal v = showV v$ map return "xyz"++[c:show n | c<-cycle "xyz", n<-[0..]]

instance Show Val where show = showVal

data Nat = Z | S Nat

data Fin :: Nat -> * where
FZ :: Fin (S n)
FS :: Fin n -> Fin (S n)

data Lam :: Nat -> * where
Var :: Fin n -> Lam n
App :: Lam n -> Lam n -> Lam n
Abs :: Lam (S n) -> Lam n

apV (Vfun f) = f

eval :: (Fin n -> Val) -> Lam n -> Val
eval env (Var fn)    = env fn
eval env (App e1 e2) = apV (eval env e1) (eval env e2)
eval env (Abs e)     = Vfun (\x -> eval (ext env x) e)

ext :: (Fin n -> V a) -> V a -> Fin (S n) -> V a
ext env x FZ     = x
ext env x (FS n) = env n

empty :: f Z -> V a
empty _ = error "empty"

*Main> eval (ext empty (Vfun id)) (Abs $Var (FS FZ))(\x.(\y.y))*Main> eval empty (Abs$ Var (FS FZ))<interactive>:182:13:    Couldn't match expected type 'Z' with actual type S n0'    Expected type: Lam 'Z      Actual type: Lam (S n0)    In the second argument of eval', namely (Abs $Var (FS FZ))' In the expression: eval empty (Abs$ Var (FS FZ))`

This works! It statically checks the size of the environment. Great!

## Tried out synatstic for Haskell editing in Vim

Syntastic is a fantastic syntax checker for Vim editor.

http://www.vim.org/scripts/script.php?script_id=2736

I learned about this recently, and tried this out for my favoraite language Haskell. And, I have also learned that Vim now has a resonable way of managing Vim packages using pathogen. I followed the instructions on the following blog for installing pathogen:

http://tammersaleh.com/posts/the-modern-vim-config-with-pathogen

When you install syntastic using pathogen, which is the recommended way, things will just work (at least in linux).

Syntastic supports Haskell using ghc-mod package, which of course requires ghc installed. Major linux distros are likey to have a distro packge for ghc-mod and ghc. I use the Debian unstable, which has ghc-mod and ghc packages by distro.

When you try out sytastic for Haskell, standard haskell scripts of hs suffix will work but the lierate haskell scripts of lhs suffix will not. The solution for this is to simply make a symbolic link of lhaskell.vim from haskell.vim in the syntax_checker directory as follows:

kyagrd@kyahp:~/.vim/bundle/syntastic/syntax_checkers$ls -al *haskell*.vim -rw-r–r– 1 kyagrd kyagrd 1694 4월 21 15:14 haskell.vim lrwxrwxrwx 1 kyagrd kyagrd 11 4월 21 16:24 lhaskell.vim -> haskell.vim Then, I got syntastic working for literate haskell scripts as well. Tips that I use. ## Korean syllable decomposition using Haskelll text-icu package provides bindings for the ICU library. The library author notes that there can be some memory overheads of copying Haskell memory area (Text) to a fixed memory area for FFI to ICU library. text-icu provides automatic buffer mangement. So, you don’t need to mess around with Ptr and raw heap memory allocation, but there is a usually expected overhead. kyagrd@kyahp:~/cscs/text-icu-ko$ ghci -XOverloadedStrings
GHCi, version 7.4.1: http://www.haskell.org/ghc/  :? for help
Prelude Data.Text.ICU> :m + Data.Text.ICU.Normalize
Prelude Data.Text.ICU Data.Text.ICU.Normalize>

By NFKD (compatibility decomposition) and NFKC (compatibility composition), Hangul chosung jamo can be equated with Hangul compatibility jamo, as follows:

…> (normalize NFD “나”,normalize NFD “ㄴㅏ”)
(“\4354\4449”,“\12596\12623”)
…> (normalize NFKD “나”,normalize NFKD “ㄴㅏ”)
(“\4354\4449”,“\4354\4449”)
…> normalize NFKD “나” == normalize NFKD “ㄴㅏ”
True

However, Unicode standard does not seem to provide some relation between jongsung jamo and compatibility jamo (hence, cannot expect ICU library to have such faclility).

…> (“난”,“ㄴㅏㄴ”)
(“\45212”,“\12596\12623\12596”)
…> (normalize NFD “난”,normalize NFD “ㄴㅏㄴ”)
(“\4354\4449\4523”,“\12596\12623\12596”)
…> (normalize NFKD “난”,normalize NFKD “ㄴㅏㄴ”)
(“\4354\4449\4523”,“\4354\4449\4354”)
…> normalize NFKD “난” == normalize NFKD “ㄴㅏㄴ”
False

So, in order to define an operator like “난” =:= “ㄴㅏㄴ” to be True, one needs to implement by themselves refering to the Hangule related unicode codepage.

References:

#langdev channel at Ozinger IRC network

UTF8 한글 문자열을 첫가끝 낱자(자소)로 분해하기