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.

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

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

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

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.

During the poster session 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.

Poster in ACM SRC hosted by ICFP 2012

SystemFiPosterICFP12ACMSRC.pdf

Draft paper (still revising, just a current dump of working version)

SystemFiDraft.pdf

Presentation material for selected posters

http://prezi.com/t7zrjbfnjx8q/system-fi/

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))(\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!

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. 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 한글 문자열을 첫가끝 낱자(자소)로 분해하기