May 2007 - Haskell-Cafe

Higher order types via the Curry-Howard correspondence
by Gaal Yahas 16 May '07

16 May '07

What do higher-order types like lists mean when viewed through the Curry-Howard correspondence? I've been wondering about this for a while. The tutorials ask me to consider id :: forall a. a -> a (.) :: forall a b c. (b -> c) -> (a -> b) -> (a -> c) These represent theorems in a logical calculus, with the variables a, b, c denoting propositions. In the case of the composition function, the proposition (a -> c) may be deduced if (b -> c) and (a -> b) obtain, and so on. (I've obviously skimmed some details.) We know the function e :: a -> b diverges because there is no way to deduce b from a with no other premises; the only value that satisfies this is bottom -- and so on. But what does the following mean? map :: (a -> b) -> [a] -> [b] Since the empty list inhabits the type [b], this theorem is trivially a tautology, so let's work around and demand a non-trivial proof by using streams instead: data Stream a = SHead a (Stream a) sMap :: (a -> b) -> Stream a -> Stream b What is the object "Stream a" in logic? What inference rules may be applied to it? How is "data Stream" introduced, and what about variant constructors? -- Gaal Yahas <gaal(a)forum2.org> http://gaal.livejournal.com/

9 14

openBinaryFile
by Eric 15 May '07

15 May '07

Hello all, Does anyone have some sample code for reading and writing to binary files? E.

2 1

readline crashes in Emacs buffer on Windows
by Gleb Alexeyev 15 May '07

15 May '07

Hello Cafe! I asked about this problem on IRC channel but with little luck. The problem boils down to the following: readline crashes on any input if the calling program runs in the Emacs buffer. To reproduce this bug, load the code below into ghci using haskell-mode and run main. >import System.Console.Readline > >main = do readline "prompt" > putStrLn "You cannot see this, because I've crashed. Amen" I'm running Windows 2003 Server, GHC-6.6, Emacs 22.0.50.1.

1 0

Problem with finalizers
by Ivan Tomac 15 May '07

15 May '07

Why does the finalizer in the following code never get called unless I explicitly call finalizeForeignPtr fptr? Even adding System.Mem.performGC made no difference. The code was compiled with ghc --make -fffi -fvia-c Test.hs Ivan -------------------- Test.hs ------------------------ module Main where import Foreign.Ptr import Foreign.ForeignPtr import Foreign.Marshal.Utils import System.Mem foreign import ccall safe "ctest.h &ctest" ctestPtr :: FunPtr (Ptr Int -> IO ()) test :: Int -> IO () test i = with i test' where test' ptr = do fptr <- newForeignPtr ctestPtr ptr putStrLn "test" -- finalizeForeignPtr fptr main = do putStrLn "before test..." test 33 putStrLn "after test..." performGC --------------------- ctest.h ---------------------- #include <stdio.h> static inline void ctest( int *i ) { printf( "finalizer called with: %d\n", *i ); }

3 5

Code layout in Emacs' haskell-mode
by Christopher L Conway 15 May '07

15 May '07

I am new to Haskell---and also to languages with the off-side rule--and working my way through Hal Daume's tutorial. I'm a little confused by the support for code layout in Emacs' haskell-mode. Is it buggy, or am I doing something wrong. For example, here's the "Hello, world" example from the tutorial, with the indentation induced by pounding Tab in haskell-mode. test.hs: module Test where import IO main = do putStrLn "Hello, world" Prelude> :l test [1 of 1] Compiling Test ( test.hs, interpreted ) test.hs:12:0: parse error on input `main' In emacs, every line but the one with "where" reports "Sole indentation". With "where", I have the option of having it flush left or indented four spaces; "import" wants to be two spaces in from "where". Moving where doesn't change the error. But if I manually move import flush left (which is the way it's shown in the tutorial, BTW): module Test where import IO main = do putStrLn "Hello, world" Prelude> :l test [1 of 1] Compiling Test ( test.hs, interpreted ) Ok, modules loaded: Test. I have a similar problem with the layout of if-then-else... num.hs: module Num where import IO main = do putStrLn "Enter a number: " inp <- getLine let n = read inp if n == 0 then putStrLn "Zero" else putStrLn "NotZero" Prelude> :l num [1 of 1] Compiling Num ( num.hs, interpreted ) num.hs:11:2: parse error (possibly incorrect indentation) Again, if I hit tab on the "then" or "else" lines, emacs reports "Sole indentation". But if I manually change the indentation, it works. module Num where import IO main = do putStrLn "Enter a number: " inp <- getLine let n = read inp if n == 0 then putStrLn "Zero" else putStrLn "NotZero" Prelude> :l num [1 of 1] Compiling Num ( num.hs, interpreted ) Ok, modules loaded: Num. This is particularly weird because if-then-else doesn't always act this way: exp.hs: module Exp where my_exponent a n = if n == 0 then 1 else a * my_exponent a (n-1) Prelude> :l exp [1 of 1] Compiling Exp ( exp.hs, interpreted ) Ok, modules loaded: Exp. I suppose this might have something to do with the do-notation... Does haskell-mode support code layout? Are there conventions I need to know about to make it behave properly? I have haskell-mode version 2.1-1 installed from the Ubuntu feisty repository. Thanks, Chris

5 5

instance monad problem
by Veer Singh 15 May '07

15 May '07

Hello, I am trying to learn haskell , but i am struggling with types , its been around 7 days , it will be very kind if some explain it why this error , i think this is the only stumbling block . I am looking for the comparison on why similar code works , while other code not . I get this error on ghci : {- `a' is not applied to enough type arguments Expected kind `*', but `a' has kind `* -> *' In the type `SS a' In the type `(Monad a) => {Monad (SS a)}' In the instance declaration for `Monad (SS a)' -} Here is the very small code with comments: data SS a = SS a Int data Maybe1 a = Nothing1 | Just1 a instance Monad Maybe1 where (Just1 x) >>= f = f x --^^ this loads fine in ghci -- where as this instance (Monad a)=> Monad (SS a) where (SS x y) >>= f = f (x y) --^^ does not work , so whats the difference , both have type parameters -- something similar works like this : instance (Eq a)=>Eq (SS a) where (SS x y) == (SS b c) = (y == c) && (x == b) Thanks

3 2

Re: [Haskell-cafe] Limits of deduction
by Matthew Brecknell 15 May '07

15 May '07

Roberto Zunino: > Yes, you are right, I didn't want to involve type classes and assumed > 3::Int. A better example would be: > > polyf :: Int -> a -> Int > polyf x y = if x==0 then 0 > else if x==1 then polyf (x-1) (\z->z) > else polyf (x-2) () > > Here, passing both () and (\z->z) _does_ make inference fail. Alternatively, type inference succeeds in rejecting an illegal program [1,2]. :-) So I think we need to be a little more precise about exactly what is undecideable in this example. Yes, the explicit type signature you've given is valid, and the Hindley-Milner type inference algorithm is not able to assign that type without an explicit signature. But that doesn't make Hindley-Milner type inference undecideable. On the contrary, Hindley-Milner type inference is deliberately designed to be decideable. To achieve that, it assumes monomorphic types in certain identifiable contexts, and therefore rejects some functions for which valid types exist. So I think the point you were making is that the problem of inferring the types of all functions for which valid types exist is, in general, undecideable. Hindley-Milner inference ensures decideability by choosing a somewhat less general (but still useful) problem. For what it's worth (not much), it might be possible to invent a decideable type inference which could infer types for a slightly larger set of functions (including polyf), by automatically generalising the types of arguments which are not inspected. Of course, doing so would presuppose the decideability of the subproblem of identifying unused arguments, and achieving that would undoubtedly require certain restrictions on the subproblem definition, analogous to the ones employed by Hindley-Milner. [1] http://haskell.org/onlinereport/decls.html#sect4.1.4 [2] http://haskell.org/onlinereport/decls.html#sect4.5

1 0

Limits of deduction
by Andrew Coppin 14 May '07

14 May '07

Suppose I have you the source code to some arbitrary function that takes a list and returns another list. It is possible to determine whether the function always examins the entire input list? Or would that be equivilent to solving the Halting Problem? (Last time I checked, the Halting Problem is unsolvable.)

9 14

How to decrease ghc link time
by Georg Sauthoff 14 May '07

14 May '07

Hi, well, I work with a Haskell project which I regulary compile with ghc. I am a bit unhappy with the link time of the project (i.e. the time ghc needs to link everyting). The project consinst of ~60 Haskell and ~25 foreign files. Some parts of the project are organized like a 'cluster', i.e. the foreign part has only one function, which is used from Haskell-Code. What could I do to improve the link time? Does some concept of 'Packages' exists in Haskell, which helps with the link time? If someone does it before, does it help to link against shared foreign libraries instead of static ones (if this is possible)? Best regards Georg

2 3

CUFP
by Simon Peyton-Jones 14 May '07

14 May '07

The CUFP website is working again now. http://cufp.galois.com/ Thanks for pointing it out. Simon

1 0