ByteLabs

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

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

:-)

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!

After loads of refactoring work a new version of HBURG has been released. If you have cabal install you can easily get it by executing the following commands:

 $ cabal update
 $ cabal install hburg

Of course you can also use the instructions provided here.

Notable changes:

• Completely refactored back-end
• Automated integration tests via Test.hs. Execute tests by running:

 $ runghc Test.hs clean configure build test

• The example Java compiler that demonstrates HBURGs usage has also been revised and updated. See HBURGs homepage for more information on the example compiler.

I am actively working on a C# back-end so you can use HBURG to generate a code generator for a compiler written in C#. This should come in handy for the advanced compiler course at the SSW.

Time Machine associates backups with the MAC address of your computer. Thus if you migrate your Time Machine backup to a new Mac Computer, you can’t resume backups where you left off. The following article should help to remedy the problem.

My dad discovered the following patent claim. Compare this with my diploma thesis. Does that ring a bell ;-)

My diploma thesis has been published as book.

Amongst many other bookstores I found these quite cool:

• Buecher.de has a nice page about it.

• Amazon.com and Amazon.de has it as well.