- Haskell - Haskell.org

A pecular algebraic data structure
by Jan Skibinski 05 Jun '01

05 Jun '01

I've been working with one pecular algebraic data structure, named Register, which is described in currently upgraded http://www.numeric-quest.com/haskell/QuantumComputer.html. or in gzipped version of the same document http://www.numeric-quest.com/haskell/QuantumComputer.html.gz. Section 13 of that document outlines the background for the topic of this message. But the section is just way too long to quote it in here. But to summarize it: data Register is pecular because it is indexable but not observable in a standard way, and because two different representations can describe the same state. In theory there should be well defined transformation from one representation to another. This seems to me as a good subject for some research work. Granted that there are many experts on functional data structures out there (I do not want to pressure any of you gurus, so I am not naming anyone :-)), could you please look at the write-up and help me with the following questions? + Is the Register data structure strangely unique, or does it fit somewhere into a hierarchy of known functional data structures? I would be happy to learn that the latter is the case, since I could then start looking at it at a more formal, well known and tested way. + Is a non-uniqness of representation amenable to formal treatment, such as deforestation? Jan

1 0

proof in haskell ?
by luc 04 Jun '01

04 Jun '01

chapter 12 of birds book mention mike spivey' theorem prover. are there anything available in source code about proof in haskell ? (btw , haskell is a great language ! one of the rare that try to "improve lazyness " ! (chaperter 11) thanks Luc

2 1

GHC core representation
by Andrew Tolmach 04 Jun '01

04 Jun '01

Dear Haskellers, Many months after the topic was first raised, there is finally a draft document describing a formal external syntax for GHC's "Core" intermediate language. It is available from http://www.cs.pdx.edu/~apt/ext-core.ps Those who wish to experiment seriously with the format described can download the latest "HEAD" experimental version of GHC. Using the "-fext-core" option when compiling "foo.hs" will generate a file "foo.core" (in additition to any other outputs specified). The document currently gives only an informal semantics "Core;" a much more formal semantics -- which I view as a very important thing to have in practice -- is in progress but not quite ready for public scrutiny. As this is very much a draft (you'll see the holes!), feedback is welcome, but due to the GHC-internals nature of this topic, please direct your comments to glasgow-haskell-users(a)haskell.org or to me personally at apt(a)cs.pdx.edu. I'll be out of email contact for the next month, though, so don't expect replies until July! - Andrew Tolmach

1 0

Re: A problem with the typing system.
by Marcin 'Qrczak' Kowalczyk 03 Jun '01

03 Jun '01

Sat, 02 Jun 2001 23:03:29 +1000, Sean Seefried <s350366(a)student.uq.edu.au> pisze: > zero = \s z ->z > succ x = \s z -> s x (x s z). > > I don't think it's important that I explain why I want the extra > occurrence of x there. I don't understand what the extra x means, so I can only explain what errors mean. I don't know what do you want to archieve. > Occurs check: cannot construct the infinite type: > t = (t -> t3 -> t2) -> t2 -> t1 The type of 's' is requested to take as its first argument 'x', which is a function which takes as its first argument 's' again. So the type of 's' would have to appear as a proper part of itself. > data Church = Ch (forall a.(a -> a -> a) -> a -> a) I would expect data Church = Ch (forall a. (a -> a) -> a) but perhaps it has something to do with your extra 'x'... > succ x = Ch(\s z -> s x (unCh x s z) > > which gives the strange typing error: > > Inferred type is less polymorphic than expected > Quantified type variable `a' is unified with `Church' The constructor Ch has type (forall a. (a -> a -> a) -> a -> a) -> Church and must be applied to a value which is polymorphic itself, i.e. which could be assigned the type '(a -> a -> a) -> a -> a' for any 'a', without knowing anything about the particular choice of 'a'. The type allows a user of the resulting Church value to choose any type for 'a' and use this argument on this type - that's why it must work for all of them. But \s z -> s x (unCh x s z) doesn't have sufficiently general type: 'x' has type Church (because 'unCh' is applied to 'x'), so 's' takes only Church as argument, so what should happen if the user instantiates it with something other than Church? > Is this sort of typing possible within Haskell. I don't know how it's supposed to behave with the extra 'x', so I can't tell what type it could have. -- __("< Marcin Kowalczyk * qrczak(a)knm.org.pl http://qrczak.ids.net.pl/ \__/ ^^ SYGNATURA ZASTÊPCZA QRCZAK

1 0

A problem with the typing system.
by Sean Seefried 02 Jun '01

02 Jun '01

Dear Haskell users, I am playing around with a variation of the Church numerals and it is giving me grief. Usually the definitions for Church numerals appear as follows. zero = \s z -> z succ x = \s z -> s (x s z) But what I would like to do is define them this way. zero = \s z ->z succ x = \s z -> s x (x s z). I don't think it's important that I explain why I want the extra occurrence of x there. Just typing this in hugs or ghci gives problems. In ghci the error message is Occurs check: cannot construct the infinite type: t = (t -> t3 -> t2) -> t2 -> t1 Expected type: t Inferred type: (t -> t3 -> t2) -> t2 -> t1 In the first argument of `x', namely `s' In the second argument of `s', namely `(x s z)' I know about rank-2 polymorphic types. (I don't really understand it but I have used them). I attempted to create a type with the following declaration. data Church = Ch (forall a.(a -> a -> a) -> a -> a) I declared an unCh unCh (Ch a) = a I then declared succ as succ x = Ch(\s z -> s x (unCh x s z) which gives the strange typing error: Inferred type is less polymorphic than expected Quantified type variable `a' is unified with `Church' Signature type: forall a. (a -> a -> a) -> a -> a Type to generalise: (Church -> Church -> Church) -> Church -> Church When checking an expression type signature In the first argument of `Ch', namely `(\ s z -> s x (unCh x s z))' in the definition of function `succ': Ch (\ s z -> s x (unCh x s z)) Doesn't the "type to generalise" fit within the framework of forall a.(a->a->a) ->a ->a. Why should it matter if something is _less_ polymorphic than expected. This is something I do not understand. Now, if I modify the definition to succ = \s z -> s x (unCh x s z) I can at least load the file. succ zero gives me _no_ typing errors. However succ (succ zero) gives me a typing error again. (And I know why) Because the type of succ zero is "(Church -> Church -> Church) -> Church -> Church" and not just simply "Church". (that is what the constructor Ch is supposed to do but it complains of the typing being less polymorphic than expected). Is this sort of typing possible within Haskell. I realise that it is sort of an infinite data type but in my opinion these sorts of things should be able to be typed. Thanks in advance. Sean Seefried.

1 0

fromInteger
by Saswat Anand 01 Jun '01

01 Jun '01

Hi, I can't understand how the arithmatic operators like (+),(-) are defined and fromInteger works in that context. Type Fun a = Int -> a fun :: Fun Int fun = (+1) instance (Num a) => Num (Fun a) where ......... (fun + 2) 10 and (2 + fun) 10 works fine. But how does it know it has to use fromInteger? But If I want these, (Just 2 + fun) 10 and (fun + Just 2) 10 to work, then is there a way to tell which conversion function to use? Thanks, Saswat

1 0

Re: Haskell 98 Report
by Marcin 'Qrczak' Kowalczyk 01 Jun '01

01 Jun '01

31 May 2001 16:10:43 -0600, Alastair David Reid <reid(a)cs.utah.edu> pisze: > and > > if foo has type > > foo :: (Ord a) => ty > > then fooBy has type > > fooBy :: (a -> a -> Bool) -> ty It's (a -> a -> Ordering) -> ty, with the default value being compare. -- __("< Marcin Kowalczyk * qrczak(a)knm.org.pl http://qrczak.ids.net.pl/ \__/ ^^ SYGNATURA ZASTÊPCZA QRCZAK

1 0

Re: fromInteger
by Marcin 'Qrczak' Kowalczyk 01 Jun '01

01 Jun '01

Fri, 1 Jun 2001 15:25:24 -0700, Saswat Anand <iscp9157(a)nus.edu.sg> pisze: > I can't understand how the arithmatic operators like (+),(-) are = > defined and fromInteger works in that context. They are all in class Num. fromInteger is automatically inserted before all integer literals, e.g. '42' is equivalent to 'fromInteger (42::Integer)' and has type 'Num a => a', i.e. the context can provide any numeric type and 42 will have that type by using the appropriate fromInteger. > Type Fun a = Int -> a > > fun:: Fun Int > fun = (+1) > > instance (Num a) => Num (Fun a) where > ......... > > (fun + 2) 10 and (2 + fun) 10 works fine. But how does it know it > has to use fromInteger? (+):: Num a => a -> a -> a >From this type it follows that both arguments of '+' must have the same type (and that this type must be Num). The first argument of '+' in 'fun + 2', i.e. 'fun', has a fully determined type: 'Fun Int'. It follows that the second argument of '+', i.e. '2', must be 'Fun Int' too. It's an integral literal, so it can have any Num type. Unifying 'Num a => a' with 'Fun Int' succeeds and gives an answer what 'a' is here: it's 'Fun Int', and it's ok because it's Num. > But If I want these, > (Just 2 + fun) 10 and (fun + Just 2) 10 > to work, then is there a way to tell which conversion function > to use? No: 'Just 2' has type 'Num a => Maybe a', 'fun' has type 'Fun Int', i.e. 'Int -> Int'. In no way 'Maybe something' can be the same type as 'arg -> result'. -- __("< Marcin Kowalczyk * qrczak(a)knm.org.pl http://qrczak.ids.net.pl/ \__/ ^^ SYGNATURA ZASTÊPCZA QRCZAK

1 0

Socket Behaviour
by Steinitz, Dominic J 01 Jun '01

01 Jun '01

Apologies if you have received this request for help already. Can anyone tell me why the following code doesn't work as expected? Both the server and client hang. [dom@lhrtba8fd85 simptest]$ server 20000 & [1] 2694 [dom@lhrtba8fd85 simptest]$ client lhrtba8fd85 20000 client: interrupted [1]+ Broken pipe server 20000 [dom@lhrtba8fd85 simptest]$ more log.txt Starting logging Hello world [dom@lhrtba8fd85 simptest]$ So it looks like the hPutStrLn to the server's socket never completes. What's stopping it? On the client side, "Hello world" gets sent but the hGetLine never completes. I guess because the server for some reason can't send. Dominic. module Main(main) where import System import IO import Socket main :: IO () main = do prog <- getProgName args <- getArgs if (length args /= 2) then do putStrLn ("Use: " ++ prog ++ " <host> <port>") exitWith (ExitFailure (-1)) else return () let host = args !! 0 port = read (args !! 1) :: Int in client host (PortNumber (mkPortNumber port)) client :: Hostname -> PortID -> IO () client host port = do sh <- connectTo host port hPutStr sh "Hello world" hFlush sh x <- hGetLine sh putStrLn x module Main (main) where import System import IO import Socket main :: IO () main = do prog <- getProgName args <- getArgs if (length args /= 1) then do putStrLn ("Use: " ++ prog ++ " <port>") exitWith (ExitFailure (-1)) else return () let port = read (args !! 0) :: Int in server (PortNumber (mkPortNumber port)) -- The server function creates a socket to listen on the port and -- loops to log messages. server :: PortID -> IO () server port = do ofh <- openFile "log.txt" WriteMode hPutStrLn ofh "Starting logging" hFlush ofh socket <- listenOn port (sh,host,portid) <- accept socket let loop = do b <- getBuffer sh 16 case b of Full msg -> do hPutStrLn ofh msg hFlush ofh loop Partial msg -> do hPutStrLn ofh msg hFlush ofh hPutStrLn sh "Finishing Logging" hFlush sh hPutStrLn ofh "Finishing logging" hClose ofh in loop data Buffer = Full String | Partial String getBuffer :: Handle -> Int -> IO Buffer getBuffer h n = if (n <= 0) then return (Full "") else do x <- try (hGetChar h) case x of Right c -> do xs <- getBuffer h (n-1) case xs of Full cs -> return (Full (c:cs)) Partial cs -> return (Partial (c:cs)) Left e -> if isEOFError e then return (Partial "") else ioError e ------------------------------------------------------------------------------------------------- 21st century air travel http://www.britishairways.com

1 0

Re: Problem
by Bruno Barbier 01 Jun '01

01 Jun '01

For hugs related questions, you should write at hugs-users(a)haskell.org See also http://haskell.org/mailman/listinfo/ for a list of haskell related mailing lists. For your problem, (works fine with linux, but I guess it's the same for Windows) I do :s to get the search paths and I get | Search path : -P{Hugs}/lib:{Hugs}/lib/hugs:{Hugs}/lib/exts then I type, :s -P{Hugs}/lib:{Hugs}/lib/hugs:{Hugs}/lib/exts:mypath1:mypath2 to add the paths 'mypath1' and 'mypath2' into the search paths; i.e. absolute paths separated by ':' (for Windows, you should probably use ';') Shirley Widyaningsih <coldblue(a)freemail.com.au> writes: > Content-type: text/plain > > > > At 01 Jun 2001 11:18:00 +0200, > Bruno Barbier (barbier(a)comte.univ-fcomte.fr) wrote: > > > > When hugs is not able to find a file, it says this. > > In the interpreter, type ':?' for help, then you can change the > > current > > path or update the paths where hugs looks for files. > > > > > > > > Can you teach me how to change the current path or updates the paths? > when i go to interpreter-> option, this below are appear. > Current settings: +fewuiA -stgl.qQkR -h250000 -p"%s> " -r$$ -c40 > Search path : -P{Hugs}\lib;{Hugs}\lib\hugs;{Hugs}\lib\exts;{Hugs} \lib\win32 > Editor setting : -EC:\WINDOWS\notepad.exe > Preprocessor : -F > > For the information, my hugs directory is in C:\Program Files\HUGS98 > Thank You > > > Sincerely, > > > Shirley > > --------------------------------------------- > WANT A NEW JOB? THEN LET THE JOB FIND YOU > > Visit www.ecruit.com.au and register your > profile. Then the headhunters can find you. > > --------------------------------------------- > Get your own free email account at > http://www.freemail.com.au/ now part of the > Webuser.com.au independent portal. Visit at > http://www.webuser.com.au > --------------------------------------------- -- Bruno Barbier Laboratoire d'Informatique de Besancon, Universite de Franche-Comte, France Phone/Fax : (33) 381.662.087 / (33) 381.666.450 Mailto : barbier(a)lifc.univ-fcomte.fr

1 0