12/26/07

Type Inference with Rank 1 Polymorphism for Type-Directed Compilation of ML




This paper defines an extended polymorphic type system for an ML-style programming language, and develops a sound and complete type inference algorithm. Different from the conventional ML type discipline, the proposed type system allows full rank 1 polymorphism, where polymorphic types can appear in other types such as product types, disjoint union types and range types of function types.


See post below, I guess I should study this.

12/22/07

Sneak Peak: the Hi language

My language is slowly progressing, so a sneak peak at the prelude and some example programs.

After studying some Mondrian code a few years ago, I decided to call my language Hieronymus after my own favorite painter Hieronymus Bosch. However, Hi seems to be so ever more nice.

Good, the interpreter is as good as done. I rewrote it in such a manner that it should be relatively easy to implement a small runtime.

I still got some problems with the type checker and rank-1 polymorphism which I am not sure I want to solve.



namespace system (

interface num = #a where (
def plus: a -> a -> a
def min: a -> a -> a
def mul: a -> a -> a
def div: a -> a -> a
)

def +: ::num a => a -> a -> a =
\x,y -> x.plus x y

def -: ::num a => a -> a -> a =
\x,y -> x.min x y

def *: ::num a => a -> a -> a =
\x,y -> x.mul x y

def /: ::num a => a -> a -> a =
\x,y -> x.div x y

)

namespace system (

interface ord = #a where (
def compare: a -> a -> int
)

def ==: ::ord a => a -> a -> bool =
\x,y -> int_eq (x.compare x y) 0

def <: ::ord a => a -> a -> bool =
\x,y -> int_less (x.compare x y) 0

def <=: ::ord a => a -> a -> bool =
\x,y -> int_less (x.compare x y) 1

def >: ::ord a => a -> a -> bool =
\x,y -> int_less (x.compare y x) 0

def >=: ::ord a => a -> a -> bool =
\x,y -> int_less (x.compare y x) 1

)

namespace system (

type bool = [ true | false ]

def not: bool -> bool =
[ true -> false
| _ -> true ]

def and: bool -> bool -> bool =
[ true, true -> true
| _ , __ -> false ]

def or: bool -> bool -> bool =
[ false, false -> false
| _ , __ -> true ]

def eq: bool -> bool -> bool =
[ false, false -> true
| true , true -> true
| _ , __ -> false ]

instance ord bool where (
def compare: bool -> bool -> int =
[ false, false -> 0
| true, true -> 0
| false, _ -> 0-1 ]
)
)

namespace system (

// type int = [ MININT | ... | -1 | 0 | 1 | 2 | ... | MAXINT ]
type int = {system.int}

def int_monadic_min: int -> int =
\v0 -> {int_monadic_min[v0]}

def int_dyadic_min: int -> int -> int =
\v0,v1 -> {int_dyadic_min[v0,v1]}

def int_plus: int -> int -> int =
\v0,v1 -> {int_plus[v0,v1]}

def int_mul: int -> int -> int =
\v0,v1 -> {int_mul[v0,v1]}

def int_div: int -> int -> int =
\v0,v1 -> {int_div[v0,v1]}

def int_compare: int -> int -> int =
\v0,v1 -> {int_compare[v0,v1]}

def int_eq: int -> int -> bool =
\v0,v1 -> {int_eq[v0,v1]}

def int_less: int -> int -> bool =
\v0,v1 -> {int_less[v0,v1]}

def int_magic_tick: () -> bool =
\v0 -> {int_magic_tick[v0]}

instance num int where (
def plus: int -> int -> int = int_plus
def min: int -> int -> int = int_dyadic_min
def mul: int -> int -> int = int_mul
def div: int -> int -> int = int_div
)

instance ord int where (
def compare: int -> int -> int = int_compare
)
)

namespace system (

type char = {system.char}

def char_compare: char -> char -> char =
\v0,v1 -> {char_compare[v0,v1]}

def char_eq: char -> char -> bool =
\v0,v1 -> {char_eq[v0,v1]}

def char_less: char -> char -> bool =
\v0,v1 -> {char_less[v0,v1]}

def char_ascii_code: char -> int =
\v0 -> {char_ascii_code[v0]}

def char_ascii_char: int -> char =
\v0 -> {char_ascii_char[v0]}

instance ord char where (
def compare: char -> char -> int = char_compare
)
)

namespace system (

def file_read: list char -> list char =
\v0 -> {file_read[v0]}

def file_write: list char -> list char -> unit =
\v0,v1 -> {file_write[v0,v1]}

)

namespace list (

using system

type list = \a => [nil | cons a (list a)]

instance ord (list a) where (
def compare: ::ord a => int =
[ nil , nil -> 0
| nil , _ -> 0-1
| _ , nil -> 1
| cons x xx, cons y yy ->
if x == y then xx.compare xx yy
else x.compare x y ]
)

def concat: list a -> list a -> list a =
[ nil, yy -> yy
| cons x xx, yy -> cons x (concat xx yy) ]

def map: (a -> b) -> list a -> list b =
[ f, nil -> nil
| f, cons x xx -> cons (f x) (map f xx) ]

def head: list a -> list a = [ cons x xx -> x ]

def tail: list a -> list a = [ cons x xx -> xx ]
)

namespace system (

type tuple_2_t = \t0 => \t1 => [tuple_2 t0 t1]

instance ::ord t0 => ::ord t1 => ord (tuple_2 t0 t1) where (

def compare: tuple_2_t t0 t1 -> tuple_2_t t0 t1 -> int =
[ tuple_2 x0 x1, tuple_2 y0 y1 ->
let c = x0.compare x0 x1 in
if c == 0 then x1.compare x1 y1 else c ]

)

type tuple_3_t = \t0 \t1 \t2 => [tuple_3 t0 t1]
)

/* Some example programs */

using system

using list

def fac: int -> int =
[ 0 -> 1
| 1 -> 1
| n -> n * (fac (n - 1)) ]

def collatz: int -> int =
let even = [n -> (n / 2) * 2 == n] in
[ 1 -> 1
| n -> if even n
then collatz (n / 2)
else collatz (1 + (n * 3)) ]

def fibs: int -> list int =
[ 0 -> cons 1 (cons 1 nil)
| n -> let ff = fibs (n-1) in
cons (head ff + (head (tail ff))) ff]


def main: (int, list int) =
let f = [(x,y) -> y] in
let p = (let n = 3 in (n, fibs n)) in f p

12/20/07

MetaLua

MetaLua is a very interesting metaprogramming Lua dialect.


---------------------------------------------------------
-- the "-{...}" means that we're going to do compile-time
-- stuff (here, syntax extension)
---------------------------------------------------------
-{ block:
------------------------------------------------------
-- Register the additional keywords in mlp.lexer
------------------------------------------------------
mlp.lexer:add{ "let", "in" }

------------------------------------------------------
-- Extend the expression parser; code generation is
-- delegated to the function let_in_builder() below.
------------------------------------------------------
mlp.expr:add{
"let", mlp.id, "=", mlp.expr, "in", mlp.expr,
builder = let_in_builder }


------------------------------------------------------
-- This creates the code returned by the macro.
-- Notice the holes-in-quote-in-splice.
------------------------------------------------------
local function let_in_builder (x)
local variable, value, expr = unpack (x)
return +{

function (-{variable})
return -{expr}
end (-{value}) }
end

} -- back to "normal" code

a, b, c = 1, 1, -2
roots = let sqrt_delta = (b^2-4*a*c)^0.5 in
{ (sqrt_delta-b)/(2*a), (-sqrt_delta-b)/(2*a) }


12/19/07

SML# Project

SML# is a new SML dialect developed by Atsushi Ohori (among others). It extends SML with a number of constructs and uses the MLton runtime system.

From their site:

SML# supports the following practically important new features:



  • Seamless Interoperablility with C

  • Record polymorphism

  • Rank1 polymorphism


SML# is carefully designed so that



  • it is a conservative extension of Standard ML: SML# compiler compiles any program that conforms to the Definition of Standard ML.

  • it supports the Basis Library.


Currently, SML# (0.20 release version) is available in the following forms.



  • source package (that can be build on linux, solaris, cygwin)

  • Mac OS Intel/PowerPC universal binary package

  • Windows binary installer


12/18/07

Erlang and Concurrency by Pang


“After a long and careful analysis the results are clear: 11 out of 10 people can't handle threads.”

Todd Hoff


From this talk, from which there is this movie.

Ah well, who doesn't know Erlang these cheap-information days?

12/17/07

OCaml and Emily In a Walnut

I program a lot of ocaml code. Not to say that there are no nicer languages, for all it is worth, ocaml is just the closest to my personal programming style: plain typed functional programming with an occasional impure construct.

Ocaml is old by now, it is older than Java. Some tools are pretty mature, one of the tools I really want to look at is Emily, of which I didn't know so far. Actually, I am not sure I quite grok it yet. Compiled-in security policies? Ouch.

12/16/07

Just a Song



My mistake, just two songs:



And some gossip: Amy Winehouse Arrested For Interfering With Husband's Assault Case: Report

12/12/07

S has a Left Inverse

Text below is by Shin-Cheng Mu 穆信成. Can you spot a bug ;-)

S is injective

Recall the definition of S:



S : (A -> B -> C) -> (A -> B) -> A -> C
S = λ x y a -> x a (y a)

I am assuming a simple semantics of sets and functions, and by S being injective I mean that S x = S x' ⇒ x = x', which can be trivially shown below:



S x = S x'
≡ { η expansion, for all y : A -> B, a : A }
(∀ a, y : S x y a = S x' y a)
≡ { definition of S }
(∀ a, y : x a (y a) = x' a (y a))
⇒ { choose y = K b for some b }
(∀ a, b : x a (K b a) = x' a (K b a))
≡ { definition of K: K b a = b }
(∀ a, b : x a b = x' a b)
≡ { pointwise equality }
x = x'


Now that we know S is injective, there ought to exist some function S⁻¹ such that S⁻¹ ○ S = id. Nakano san claimed that a definition would be:



S⁻¹ : ((A -> B) -> A -> C) -> A -> B -> C
S⁻¹ = λ x a b -> x (K b) a

That S⁻¹ ○ S = id is easy to see:



S⁻¹ (S x) a b
= (S x) (K b) a
= x a (K b a)
= x a b

From another direction, we have only S ○ S⁻¹ ⊆ id since S is not a surjective function. How the range of S look like? Inspecting the definition of S. Since y is applied only once to a, the value of y on other input does not matter. That is, the range of S consists of only functions e such that:



e y a = e y' a for all y, y' such that y a = y' a ......(1)

We will show that S (S⁻¹ e) = e for all e satisfying (1):



S (S⁻¹ e) y a
= { definition of S }
S⁻¹ e a (y a)
= { definition of S⁻¹ }
e (K (y a)) a
= { by (1), since K (y a) a = y a }
e y a

Inverting higher-order functions?

Some endnotes. Once Nakano and I thought we discovered how to invert higher-order functions (and even derive the necessary side conditions, like the one on e above) by drawing λ expressions as trees and manipulating them. It turned out that I overlooked something obvious in the very beginning and the result was a disaster.

Wiimote Interactive Whiteboard


12/10/07

Humanitarian Scientific Achievement Award




Burnham Institute for Medical Research
Professor Yu Yamaguchi, M.D., Ph.D., was recently awarded The Humanitarian Scientific Achievement Award by the MHE Research Foundation. The focus of the foundation is to find a cure for Multiple Hereditary Exostoses, a rare genetic bone disorder. The disorder causes people to grow exostoses (bone tumors) on their bones. MHE patients can also suffer from non-skeletal medical issues including mental and neurological issues.


  1. Mild social interaction deficits (excessive shyness, adherence to routines)

  2. Heightened sensitivities to sensory stimulation (sounds, touch, taste)

  3. Difficulties to concentrate

  4. Muscle weakness (easy to get tired)

  5. Reduced levels of fear/anxiety (well, just in mice, that is)



He believes these symptoms can be explained by the deficiency of heparan sulfate in nerve and muscle cells.

Also of interest, HSV immune sog9 cells?