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 :)

I only had 10 posts?!

I only had 10 posts?!

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.

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. If you don’t want navigate through this cool online LaTeX editor, you can simply download PDF here. 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.

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.

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.

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.

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

During the poster session in ICFP’12 several people asked me about whether further information is available. So, here I posted a PDF of my poster and a draft paper submitted to a conference (now accepted and published in TLCA’13

Poster in ACM SRC hosted by ICFP 2012


Draft of our TLCA’13 paper

available online at http://citeseerx.ist.psu.edu/viewdoc/summary?doi=

BibTeX for citation:

booktitle={Typed Lambda Calculi and Applications},
series={Lecture Notes in Computer Science},
editor={Hasegawa, Masahito},
title={System Fi: a higher-order-polymorphic lambda calculus with erasable term indices},
publisher={Springer Berlin Heidelberg},
keywords={term-indexed data types; generalized algebraic data types;
 higher-order polymorphism; type-constructor polymorphism;
 higher- kinded types; impredicative encoding;
 strong normalization; logical consistency},
author={Ahn, KiYung and Sheard, Tim and Fiore, Marcelo and Pitts, Andrew M.},

Presentation material for selected posters



I also have a reference implementation of a Church-style Fi with both beta-conversion and eta-conversion (doesn’t have a parser though, just Haskell syntax tree, normalizer, and type checker)


{-# 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))
*Main> eval empty (Abs $ Var (FS FZ))

    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!

Syntastic is a fantastic syntax checker for Vim editor.


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:


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.

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
Loading package ghc-prim … linking … done.
Loading package integer-gmp … linking … done.
Loading package base … linking … done.
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 “ㄴㅏ”)
…> (normalize NFKD “나”,normalize NFKD “ㄴㅏ”)
…> normalize NFKD “나” == normalize NFKD “ㄴㅏ”

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

…> (“난”,”ㄴㅏㄴ”)
…> (normalize NFD “난”,normalize NFD “ㄴㅏㄴ”)
…> (normalize NFKD “난”,normalize NFKD “ㄴㅏㄴ”)
…> normalize NFKD “난” == normalize NFKD “ㄴㅏㄴ”

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


#langdev channel at Ozinger IRC network

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