ByteLabs

This has bugged me for a while when useing TextMates ‘Filter Through Command…’ to replace all newlines in a selection. Somehow my mind always wants to use sed to do this although there are simpler ways to do it.

The following works with GNU sed but not with BSD sed on my Mac (although it should work given the documentation in the man page):

sed -n ':a;N;$!ba;s/\n//g;p' < infile

• :a put label at the first position
• N Append the next line of input to the pattern space
• $!ba branch to label a, the ! tells it to apply the command to a non-selected pattern space and the $ addresses the last line of input
• s/\n//g substitutes a newline with a space
• p writes pattern space to standard output

If you can make this work with BSD sed please let me know.

Our PASTA (Processor Automated Synthesis by iTerative Analysis Project) research group has a new website. The content is still quite incomplete but over the next few weeks we shall bring it all into shape. So stay tuned….

Searching in large projects (i.e. gcc repository) can be painfully slow with TextMate. If you encounter this problem have a look at the Ack TextMate Bunlde.

Get the standalone version of ack from here.

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]