Type industry muggle ...

| Posted by Ki Yung Ahn

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: pakcs@curry-language.org)
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

| Posted by Ki Yung Ahn

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.

| Posted by Ki Yung Ahn

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

| Posted by Ki Yung Ahn

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.

| Posted by Ki Yung Ahn

I only had 10 posts?!

| Posted by Ki Yung Ahn

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.

| Posted by Ki Yung Ahn

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.

| Posted by Ki Yung Ahn

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.

| Posted by Ki Yung Ahn

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.

| Posted by Ki Yung Ahn

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