ByteLabs

A nice article by Oleg Kiselyov about Existential Datatypes. Enjoy!

• http://foldl.com/
• http://foldr.com/

:-)

Under Australian copyright laws, copyright in literary works of authors, who died before 1955, has expired. These works are now within the ‘public domain’ in Australia and this is why the University of Adelaide is able to reproduce such works on the world wide web. Here go some of my favourites:

• George Orwell
• Charles Darwin
• Immanuel Kant
• Franz Kafka
• Leo Tolstoy
• Fyodor Dostoyevsky
• many more….

“Long-escalating tensions between Russia and the former Soviet republic of Georgia erupted into full-scale war Friday, leaving hundreds if not thousands of civilians dead and turning thousands more into refugees, forced to flee for their lives.” [1]

It seems Georgia is another proxy state supported by the US to expand its imperialist plans. Everyone who knows a bit of history should not be surprised by what is going on. Mass media – as usual – doesn’t give the appropriate context in order to understand the conflict. But if you are looking for the truth, you can find it.

I would like to direct your attention to Bill Van Auken’s article US-Russian tensions in Caucasus erupt into war.

Here is a map of Georgia which might be useful in combination with the article, and further background reading:

• Further escalation of tensions in the Caucasus between Russia and Georgia
• The missile defense scheme and the sharpening of US-Russian geopolitical tensions
• Russia and Georgia on the brink of armed conflict over Abkhazia
• Economy in Georgia

Again I would like to draw an interesting example from Benjamin Pierce’s book Types and Programming Languages that is originally due to Kfoury, Tiuryn, and Urzyczyn. The following Haskell program is well typed but takes a very long time to typecheck:

module Main (main) where
main =
 let f0 = \x -> (x,x)
     f1 = \y -> f0 (f0 y)
     f2 = \y -> f1 (f1 y)
     f3 = \y -> f2 (f2 y)
     f4 = \y -> f3 (f3 y)
     f5 = \y -> f4 (f4 y)
 in
 f5 (\z -> z)

{-# LANGUAGE RankNTypes #-}
module Main (main) where
-- g1: identity function
-- GHC implicitely quantifies it to: forall a. a -> a
g1 :: a -> a
g1 x = x
-- g2: Rank2Type
g2 :: (forall a. a -> a) -> (Bool, Char)
g2 f = (f True, f 'a')
-- g3: Rank3Type
g3 :: ((forall a. a -> a) -> (Bool, Char)) -> (Char, Bool)
g3 f = (\x -> (snd x, fst x)) (f g1)
-- g4: Rank4Type
g4 :: (((forall a. a -> a) -> (Bool, Char)) -> (Char, Bool)) ->
         (Bool, Char)
g4 f = (\x -> (snd x, fst x)) (f g2)

main :: IO ()
main = do
  putStrLn "Rank-2 Example:" 
  putStrLn . show . fst . g2 $ g1
  putStrLn . show . snd . g2 $ g1
  putStrLn "Rank-3 Example:" 
  putStrLn . show . fst . g3 $ g2
  putStrLn . show . snd . g3 $ g2
  putStrLn "Rank-4 Example:" 
  putStrLn . show . fst . g4 $ g3
  putStrLn . show . snd . g4 $ g3

The polymorphism of System F is often called impredicative. A definition is called impredicative if it involves a quantifier whose domain includes the very thing being defined. For example in System F, the type variable X in the type T = ∀X. X → X ranges over all types, including T itself (so that, for example, we can instantiate a term of type T at type T, yielding a function from T to T).[6]

The polymorphism found in ML is called predicative, because the range of type variables is restricted to monotypes (i.e. quantifier-free types), which do not contain quantifiers.

When talking about type reconstruction the previous definitions are important. There is a growing “[...] need for ever more expressive type system features, most of which threaten the decidability and practicality of Damas-Milner type inference. One such feature is the ability to write functions with higher-rank types—that is, functions that take polymorphic functions as their arguments.”[1]

Complete type inference is known to be undecidable for higher-rank (impredicative) type systems. This post serves as a reference for type reconstruction in the presence of polymorphism in higher-rank type systems.

[1] Practical type inference for arbitrary-rank types

[2] Haskell/Polymorphism

[3] Type Polymorphism – DocForge

[4] Type Polymorphism -Wikipedia

[5] System F – Polymorphic/Second-Order Lambda Calculus

[6] Types and Programming Languages [p.360]

If you managed to compile the latest darcs version of GHC (6.9.20080720 in my case) on Mac OS X Leopard, then there is a good chance that you ran into the following problem. I have opened a ticket with a solution proposal.

It’s not the cleanest solution but it works. Good luck!

I would like to point out the following article by Howard Zinn published a while ago on www.alternet.org. Although it has been a year since it was published the topic is still current and deserves attention.

There is new movie coming out called the American Dream. It looks very interesting and features interviews with people like Howard Zinn and Danny Glover.

The movie webpage also features a very interesting trailer and teaser as well as a quite shocking ‘Facts’ page.