Re: [Haskell-cafe] Signature for non-empty filter
On Wed, 6 Feb 2008, Jonathan Cast wrote: On 6 Feb 2008, at 1:54 PM, Matthew Pocock wrote: On Wednesday 06 February 2008, Henning Thielemann wrote: If the type checker does not terminate because the checked function does not terminate on the example input, then the function does not pass the type check and as a compromise this would be ok. Can't fault this logic. The problem is that you may have to wait quite a long time to discover this non-termination. I would second this --- letting the compiler go only to discover that it's been running for the last 3 hours because it's diverging seems like a wasted 3 hours. There is the same problem with unit testing: Tests that eat too much time have to be rewritten. Same here: If the automatic proof takes too long - choose a simpler example input (if possible). But Dan's point definitely applies here - there is no need to automatically prove every instance, if there is a possibility to do a proof manually. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Signature for non-empty filter
On Thu, 7 Feb 2008, Neil Mitchell wrote: Hi I think what you want to say now is not just (filter f l) is type correct when there is some argument on which f returns true but (filter f l) is type correct when there is some *element of l* on which f returns true or in Haskell: filterNonEmpty f x = assert (not $ null res) res where res = filter f x If you give that definition to the Catch tool (http://www-users.cs.york.ac.uk/~ndm/catch/) it will try and prove each call is safe. For certain examples, Catch will do the job very well - for example if your filter is something structural like isJust or null. Indeed, if Catch or ESC or similar tools can handle such specifications it would be great. However I suspect that the translation you gave is different from what I wanted. I consider a function buggy, if it implements 'const' considerably more complicated than just saying 'const'. :-) That is, I only want to reject a function if it _always_ returns the empty list. Your 'filterNonEmpty' is rejected whenever _some_ arguments yield the empty list. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re[4]: [Haskell-cafe] Signature for non-empty filter
Hello Henning, Thursday, February 7, 2008, 12:29:02 AM, you wrote: it's impossible to check for *arbitrary* function call whether it will be terminated. seems that you don't have formal CS education? :) so one can develop set of functions that are guaranteed to be terminated or guaranteed to be non-trivial. but it's impossible to check for arbitrary function whether it's trivial and even whether it will terminate for particular data If the type checker does not terminate because the checked function does not terminate on the example input, then the function does not pass the type check and as a compromise this would be ok. how you can check that some code doesn't terminate? ;) it may be just a bit too slow. we again return to my original point - we can check for *some* representations of trivial functions values, but we can't *ensure* that some computation is non-trivial -- Best regards, Bulatmailto:[EMAIL PROTECTED] ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re[2]: [Haskell-cafe] Mutable arrays
Hello Jeff, Thursday, February 7, 2008, 1:31:59 AM, you wrote: I noticed that GHC implements mutable arrays in the IO monad. This seems odd to me. Arrays aren't related to IO. IO monad isn't only about I/O but about imperative stuff in general. there is also special monad limited to mutable vars and arrays, namely ST. read also this: http://haskell.org/haskellwiki/Modern_array_libraries http://haskell.org/haskellwiki/IO_inside -- Best regards, Bulatmailto:[EMAIL PROTECTED] ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Signature for non-empty filter
Hi
Indeed, if Catch or ESC or similar tools can handle such specifications it
would be great. However I suspect that the translation you gave is
different from what I wanted. I consider a function buggy, if it
implements 'const' considerably more complicated than just saying 'const'.
:-) That is, I only want to reject a function if it _always_ returns the
empty list. Your 'filterNonEmpty' is rejected whenever _some_ arguments
yield the empty list.
Yes, but someone redefined your problem as the above one, which I can
solve :-) For your original problem, Catch is entirely unsuitable.
ESC/Haskell would be my preferred method of solving this within
Haskell, but I'm not sure if it has existentials or not. I could
imagine writing something like:
filter :: {f: exists x. f x == True} - {True} - {True}
filter :: (a - Bool) - [a] - [a]
Thanks
Neil
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Implementing fixed-sized vectors (using datatype algebra?)
Am Donnerstag, 7. Februar 2008 02:47 schrieb Alfonso Acosta: The other library I use for type-level programming is HList. It has type-level booleans already so you might what to take a look at it if you're not already familiar with it. Thanks I'll have a look at it. I have to admit that I don’t like the names HBool, HTrue and HFalse. What do they mean? Heterogenous booleans? Heterogenous truth? Why it’s “Bool” instead of “Boolean” and therefore not conforming to the Prelude convention? Heterogenous lists are not directly about type level computation. A HList type is usually inhabited. On the other hand, types which denote type level naturals or type-level booleans are empty data types. So type level booleans should go into some type level programming library like the one Alfonso and I want to create. HList should then use these booleans. This is at least my opinion. Best wishes, Wolfgang ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Draft chapters of Real World Haskell now publicly available
Hello Peter, an answer to an “old” e-mail (from January 25). Sorry for not answering earlier. Am Freitag, 25. Januar 2008 00:23 schrieben Sie: Wolfgang Jeltsch wrote: Indeed. A functional approach to GUIs is nice but at the moment we don’t have anything that is suitable for solving real world problems (although this is being worked on). Could you elaborate a bit on that? What are the current obstacles to be solved? Performance problems and lack of widgets are the two things that come to my mind immediately. Maybe also lack of a good way of doing dynamic user interfaces (user interfaces with a changing set/order of widgets). When I looked at Yampa, I didn't really see a problem with making a GUI or interactive application based on it (besides maybe performance and space/time leaks, the latter IMO being a general problem in Haskell that just occurs quicker in reactive programming). I think, performance is a big problem. To me it seems that Yampa-based GUIs maybe have a performance penalty of more than just a constant factor. Please have a look at the sections “Implementation and efficiency” and “Signals” under http://haskell.org/haskellwiki/Talk:Grapefruit. […] The main problem I could see is that Yampa is not really event driven in the imperative sense; I mean in an ideal event based system, the hardware triggers an interrupt when some sensor changes, and this then triggers other software events; only the code that is related to handling the event that occurred is executed. But the event that is handled could potentially not be needed for the current output (which could be considered as a programming bug...) Not necessarily a bug. There are events which don’t result in changes of the GUI, for example, mouse clicks into empty areas. […] Best wishes, Wolfgang ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] problem with collection (container) class
Am Donnerstag, 7. Februar 2008 08:58 schrieb Leandro Demarco Vedelago:
but when I try to load it in WinHugs I get the following error message:
- Instance is more general than a dependency allows
*** Instance : Container Abb a b
*** For class: Container a b c
*** Under dependency : a - b
and as I have stated above my knowledge about dependencies is almost null,
not to say null, so I don´t even have an idea where the error is.
Maybe ghci's error message is more helpful:
[EMAIL PROTECTED]:~/Documents/haskell/move ghci Leandro
GHCi, version 6.8.2: http://www.haskell.org/ghc/ :? for help
Loading package base ... linking ... done.
[1 of 1] Compiling Leandro ( Leandro.hs, interpreted )
Leandro.hs:16:19:
`Abb' is not applied to enough type arguments
Expected kind `*', but `Abb' has kind `* - * - *'
In the instance declaration for `Container Abb a b'
Failed, modules loaded: none.
There are a couple of other things, mainly that you have the wrong type for
'add' and you need an Ord constraint for 'search'.
This works:
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{- # LANGUAGE FlexibleInstances # -}
module Leandro where
data Abb a b = Branch a b (Abb a b) (Abb a b) | Leaf
data ListAssoc a b = Node a b (ListAssoc a b) | Empty
class Container c a b |c - a, c - b where
empty :: c
add :: c - a - b - c
search :: c - a - Maybe b
del :: c - a - c
toListPair :: c - [(a,b)]
instance (Ord a) = Container (Abb a b) a b where
empty = Leaf
add Leaf x y = Branch x y Leaf Leaf
add arb@(Branch ni nd ri rd) x y
|x == ni = arb
|x ni = Branch ni nd ri (add rd x y)
|otherwise = Branch ni nd (add ri x y) rd
search Leaf x = Nothing
search (Branch ni nd ri rd) x
|x == ni = Just nd
|x ni = search rd x
|x ni = search ri x
Note: The FlexibleInstances Language pragma is required by GHC 6.8.1 and
6.8.2, but not by GHC 6.6.1 or hugs, I think that's a bug in 6.8.*
A suggestion that I've received was to change the type of Abb for
data Abb (a,b) = Branch a b (Abb (a,b)) (Abb (a,b)) | Leaf
and declare container class with just two parameters like I found in all
pages I visited. I have not tried this yet, as I still have hope that what
I intend to do is possible.
Well if you have any suggestions I'd appreciate you send it to me and sorry
for bothering you and my english, but i'm spanish-speaker.
Cheers,
Daniel
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Best practice for embedding files in a GHC-compiled tool?
On Feb 7, 2008, at 12:27 AM, [EMAIL PROTECTED] wrote: Are you assuming that the various users have GHC/Hugs installed? You know about scripting through the 'runhaskell' binary, right? I do, and I've used this. I don't want to do that here. Let me say this again: I am making no assumptions whatsoever about various users, other than platform. Haskell is not a niche language, with the right compile options, it CAN be used in this way. Here's the extreme case: When one is installing Mac OS X, one has access to a command line via a terminal application, but the operating system is otherwise very stripped down. Nevertheless, if one customizes an install DVD by adding a single command-line tool, one can execute that tool in this environment. I'd rather use Haskell than C for such applications. With C, we can introduce one file to an alien environment, and it will run. I've linked GHC Haskell programs that can be used in this way. Such programs can be used by anyone on a given platform. Assuming that GHC/Hugs is installed divides the potential audience by a large factor. Under this extreme hypothesis, how do I embed a compressed tar file into a single file command line tool written in Haskell and compiled by GHC? Thanks, Dave ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re[2]: [Haskell-cafe] Signature for non-empty filter
Hello Dan, Thursday, February 7, 2008, 4:04:03 AM, you wrote: I.e., it's not necessary to restrict the class of functions you consider if you're willing to give up on full automation. So I disagree with the only if below. ok, read this as computer can ensure..., because it was exactly the original question - can computer check that any given function in turing-complete language is non-trivial? this means that answer to original question - one can ensure that argument for filter is non-terminating function only if these functions are written using some special notation which doesn't allow to write arbitrary turing-complete algorithms -- Best regards, Bulatmailto:[EMAIL PROTECTED] ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re[2]: [Haskell-cafe] Mutable arrays
Hello Jeff, Thursday, February 7, 2008, 4:17:27 AM, you wrote: logical place for mutable arrays. However, I don't understand the motivation for implementing it in IO. Were mutable arrays added to IO because it would be difficult to write code that does both IO and manipulates arrays otherwise? yes. you can't perform separate ST actions in IO monad, you may call only entire computations with pure results - the same as you can do from pure code IO monad implements idea of sequencing actions and it is used ro import any actions written in other languages (C/C++ in most cases). ST monad is just the same internally but it was directive limited to only two types of actions - with variables and mutable arrays. this, together with some type tricks ensures that its results are referentially-transparent and therefore may be called from pure code -- Best regards, Bulatmailto:[EMAIL PROTECTED] ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re[2]: [Haskell-cafe] Signature for non-empty filter
On Thu, 7 Feb 2008, Bulat Ziganshin wrote: Thursday, February 7, 2008, 4:04:03 AM, you wrote: I.e., it's not necessary to restrict the class of functions you consider if you're willing to give up on full automation. So I disagree with the only if below. ok, read this as computer can ensure..., because it was exactly the original question - can computer check that any given function in turing-complete language is non-trivial? My original question according to http://www.haskell.org/pipermail/haskell-cafe/2008-February/039161.html was Is Haskell's type system including extensions strong enough for describing a function, that does not always return a trivial value? ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] background question about IO monad
On 6 Feb 2008, at 11:32 PM, Uwe Hollerbach wrote: All right, after a bit of dinner and some time to mess about, here's another attempt to check my understanding: here is a simplified version of the lisp-time example: module Main where import System.Time pure_fn :: Integer - String pure_fn n = calendarTimeToString (toUTCTime (TOD n 0)) wicked_fn :: IO String wicked_fn = getClockTime = return . pure_fn . toI where toI (TOD n _) = n make_wicked :: String - IO String make_wicked str = return str -- use of pure_fn -- main = putStrLn (pure_fn 123000) -- use of wicked_fn -- main = wicked_fn = putStrLn -- use of make_wicked main = (make_wicked (pure_fn 1234567890)) = putStrLn If I use the first of the three main alternatives, I'm calling a pure function directly: it takes an integer, 123..., and produces a string. If I pass the same integer to the pure function, I'll get the same value, every time. This string is passed to putStrLn, an IO action, in order that I may gaze upon it, but the string itself is not thereby stuck in the IO monad. If I use the second of the three main alternatives, I'm calling an IO action: wicked_fn, which returns the current time formatted as UTC. In principle, every time I call wicked_fn, I could get a different answer. Because it's an IO action, I can't just pass it to putStrLn in the same way I passed in the previous pure_fn value, but instead I have to use the bind operator =. If I use the third of the main alternatives, I am starting with a pure function: it's that number formatted as UTC (it happens to come to Fri Feb 13 of next year), but then I pass it through the make_wicked function, which transmogrifies it into the IO monad. Therefore, as in the above, I have to use = in order to get it to work; putStrLn (make_wicked (pure_fn 123...)) doesn't work. deep breath OK, after all that, my original question, in terms of this example: the IO monad is one-way is equivalent to saying there is no haskell function that I could write that would take (make_wicked (pure_fn 123456)) and make it into something that could be used in the same way and the same places as just plain (pure_fn 123456) ? And, coming back to my scheme interpreter, this is at least somewhat irrelevant, because, since I am in a REPL of my own devising, I'm firmly in IO-monad-land, now and forever. Right. jcc ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Haskell maximum stack depth
Hi But the point is that *both* heapGobbler and neilGobbler are likely to be slower and chew through at least twice as much heap as stackGobbler, which would be the implementation of choice for both simplicity and performance if it wasn't for this stack management problem. Sure? That sounds like the thing that people can conjecture, but benchmarks can prove. And I'd claim that neilGobbler is the simplest function by a large margin. Thanks Neil ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Haskell maximum stack depth
Adrian Hey wrote: AFAICT neilGobbler isn't even entirely safe as an implementation of an eager take. There's nothing the Haskell standard to stop it being transformed into.. neilGobbler :: Int - [x] - [x] neilGobbler n xs = length (take n xs) `seq` take n xs Whoops, I see stackGobbler has the same problem.. -- Strict version of take stackGobbler :: Int - [x] - [x] stackGobbler 0 _ = [] stackGobbler _ [] = [] stackGobbler n (x:xs) = let xs' = stackGobbler (n-1) xs in xs' `seq` (x:xs') I guess this is an example of the Haskell standard needing to be tightened up a bit, but that is another story.. Regards -- Adrian Hey ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] :i and :t give different types
ryani.spam: It looks like there is a bug with unparsing of bang-constructors in ghci: On 2/7/08, Don Stewart [EMAIL PROTECTED] wrote: data Stream a = forall s. Unlifted s = Stream !(s - Step a s) -- ^ a stepper function !s-- ^ an initial state Prelude Data.Stream :info Stream data Stream a where Stream :: forall a s. (Data.Stream.Unlifted s) = !s - Step a s - !s - Stream a This last line should start with !(s - Step a s) instead of !s - Step a s. If that was fixed, everything looks correct. Ah, yes, missing parens! Well spotted. So a pretty printer wibble in GHC? -- Don ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] :i and :t give different types
It looks like there is a bug with unparsing of bang-constructors in ghci: On 2/7/08, Don Stewart [EMAIL PROTECTED] wrote: data Stream a = forall s. Unlifted s = Stream !(s - Step a s) -- ^ a stepper function !s-- ^ an initial state Prelude Data.Stream :info Stream data Stream a where Stream :: forall a s. (Data.Stream.Unlifted s) = !s - Step a s - !s - Stream a This last line should start with !(s - Step a s) instead of !s - Step a s. If that was fixed, everything looks correct. -- ryan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Mutable arrays
Ok, I've done some testing on different array accessing strategies, and at this point I believe that, as Stefan previously suggested, using an Oleg-inspired fold for access offers the best performance. My first non-unsafe idea was to try: import Data.Array.MArray import Data.Array.IO import Data.Int (Int32) import Data.List (foldl') -- |Create an array. Change the type signature to experiment with different array types. makeAry :: IO (IOUArray Integer Float) makeAry = newListArray (1,100) [1..] getElemsLazy :: (MArray a e m, Ix i) = a i e - m [e] getElemsLazy myAry = getBounds myAry = mapM (readArray myAry) . range this works on a 1 million element Int32 array (IOArray or IOUArray): myElems -getElemsLazy myAry let myMax = foldl' max 0 myElems But with a 10-million element array, I get a stack overflow. I next tried the foldA functions Stefan posted, but had some problems with them. I think that the array elements need to be instances of Bounded and Fractional, and I don't know of a suitable type. Anyway, his code is a little too compact for me to understand without further study, so I moved on. Next I created my own fold operators. These are fairly directly copied from an email Oleg posted to the haskell mailing list: leftFoldA' myArray self iteratee seed = do elem - readArray myArray $ fst seed case iteratee seed elem of Left seed - return seed Right seed - self iteratee seed leftFoldA :: (MArray a e m, Ix a1) = a a1 e - ((a1, b) - e - Either t (a1, b)) - a1, b) - m t leftFoldA array iteratee seed = let g = (leftFoldA' array) g in g iteratee seed leftFoldModA' myArray self iteratee seed = do elem - readArray myArray $ fst seed result - iteratee seed elem case result of Left seed - return seed Right seed - self iteratee seed leftFoldMA :: (MArray a e m, Ix a1) = a a1 e - ((a1, b) - e - m (Either t (a1, b))) - a1, b) - m t leftFoldMA array iteratee seed = let g = (leftFoldModA' array) g in g iteratee seed the two functions to use are leftFoldA and leftFoldMA. The difference, show in the type signature, is that the iteratee in leftFoldA is pure while the iteratee in leftFoldMA operates in the monad. So if you're going to modify the array, for example, you need to use the leftFoldMA version. These folds let me define: findMax myAry = do (lowB, highB) - getBounds myAry let maxReader (ix, acc) c = let ix' = ix + 1 acc' = max c acc in acc' `seq` (if ix' highB then Left else Right) (ix', acc') (_, myMax) - leftFoldA myAry maxReader (lowB, 0) return myMax normalizeArray myAry = do myMax - findMax myAry (lowB, highB) - getBounds myAry let normMod = 1/myMax let normalizer (ix, _) c = do let ix' = ix + 1 curVal - readArray myAry ix writeArray myAry ix (curVal * normMod) return $ (if ix' highB then Left else Right) (ix', ()) leftFoldMA myAry normalizer (lowB, ()) -- |show all elements from lowB to highB -- this only works with IO arrays, since the readArray and print happen in the same monad. -- you could possibly make it work with ST arrays if you use a monad transformer, but you'd have -- to change leftFoldMA as well. showElems myAry lowB highB = do let showFunc (ix, _) c = do let ix' = ix + 1 readArray myAry ix = print return $ (if ix' highB then Left else Right) (ix', ()) leftFoldMA myAry showFunc (lowB, ()) There are probably better ways to define the folds, but I hope these are pretty easy to follow. If I was doing a lot of different operations, I'd probably define functions like makeIteratee highB func = (\(ix, acc) c - let ix' = ix + 1 acc' = func c acc in acc' `seq` (if ix' highB then Left else Right) (ix', acc')) so that findMax becomes: findMax2 myAry = do (lowB, highB) - getBounds myAry (_, myMax) - leftFoldA myAry (makeIteratee highB max) (lowB, 0) return myMax instead of having to define a bunch of iteratees in let clauses. Now, running the program main :: IO () main = do myAry - makeAry (lowB, highB) - getBounds myAry normalizeArray myAry showElems myAry 1 10 showElems myAry 90 100 return () takes about 5 seconds, with no optimizations. It takes less than a second with -O2. Much better. It does take longer with boxed arrays, but that's to be expected. No unsafe functions, either. The only sketchy bit is using seq in the iteratees (e.g. maxReader in findMax) to force the accumulator. I say sketchy not because it's unsafe or unreliable, but it would be nice if it was unnecessary. Notes: I used GHC 6.8.1 on WinXP, 3.2GHZ P4, 1.5GB RAM. All of my original tests were done without any optimizations, which is why I didn't include timing information for the earlier stuff. The getElemsLazy function is
Re: [Haskell-cafe] :i and :t give different types
chad.scherrer: Hello haskell-cafe, In ghci, I tried to get info for Data.Stream.Stream: $ ghci GHCi, version 6.8.2: http://www.haskell.org/ghc/ :? for help Loading package base ... linking ... done. Prelude :m Data.Stream Prelude Data.Stream :i Stream data Stream a where Stream :: forall a s. (Data.Stream.Unlifted s) = !s - Step a s - !s - Stream a -- Defined in Data.Stream That's fine, and is the correct type. data Stream a = forall s. Unlifted s = Stream !(s - Step a s) -- ^ a stepper function !s-- ^ an initial state instance Functor Stream -- Defined in Data.Stream This didn't seem right to me, so I asked tried this: Prelude Data.Stream :t Stream Stream :: (Data.Stream.Unlifted s) = (s - Step a s) - s - Stream a So that's the type of the Stream constructor, which introduces a new existentially typed Stream (the 'a'). What's going on here? forall a s. (Data.Stream.Unlifted s) = !s - Step a s - !s - Stream a and (Data.Stream.Unlifted s) = (s - Step a s) - s - Stream a One is the type, one is the constructor for the type. are completely different, right? And really, neither one makes much sense to me. I would have expected forall s. (Data.Stream.Unlifted s) = (s - Step a s) - s - Stream a For the constructor? This all looks right, as far as I can tell: $ ghci -fglasgow-exts Prelude :m + Data.Stream Info about the data type: Prelude Data.Stream :info Stream data Stream a where Stream :: forall a s. (Data.Stream.Unlifted s) = !s - Step a s - !s - Stream a -- Defined in Data.Stream instance Functor Stream -- Defined in Data.Stream The type of the constructor Prelude Data.Stream :t Stream Stream :: forall s a. (Data.Stream.Unlifted s) = (s - Step a s) - s - Stream a The kind of the type: Prelude Data.Stream :k Stream Stream :: * - * -- Don ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] :i and :t give different types
Hello haskell-cafe, In ghci, I tried to get info for Data.Stream.Stream: $ ghci GHCi, version 6.8.2: http://www.haskell.org/ghc/ :? for help Loading package base ... linking ... done. Prelude :m Data.Stream Prelude Data.Stream :i Stream data Stream a where Stream :: forall a s. (Data.Stream.Unlifted s) = !s - Step a s - !s - Stream a -- Defined in Data.Stream instance Functor Stream -- Defined in Data.Stream This didn't seem right to me, so I asked tried this: Prelude Data.Stream :t Stream Stream :: (Data.Stream.Unlifted s) = (s - Step a s) - s - Stream a What's going on here? forall a s. (Data.Stream.Unlifted s) = !s - Step a s - !s - Stream a and (Data.Stream.Unlifted s) = (s - Step a s) - s - Stream a are completely different, right? And really, neither one makes much sense to me. I would have expected forall s. (Data.Stream.Unlifted s) = (s - Step a s) - s - Stream a -- Chad ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Implementing fixed-sized vectors (using datatype algebra?)
On Feb 7, 2008 9:01 PM, Dan Weston [EMAIL PROTECTED] wrote:
This may be a GHC bug, but even though in the module
Data.TypeLevel.Num.Reps has the header
{-# LANGUAGE EmptyDataDecls, TypeOperators #-}
I still get an error with both ghc and ghci version 6.8.2 unless I throw
in the -XTypeOperators flag.
If you are using type operators in a module you have to supply the
flag, independently of what flags are supplied in other modules.
The same applies for other extensions which modify the _syntax_ of the
language (e.g. Template Haskell etc ...)
So, it's not a bug.
As a side note, even if the TypeOperators flag is supplied GHC 6.8.2
fires an error with the following declaration:
instance (Compare x y CEQ) = x :==: y -- GHC fires a Malformed
instance header error
whereas using an equivalent prefix definition works just fine
instance (Compare x y CEQ) = (:==:) x y
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Implementing fixed-sized vectors (using datatype algebra?)
I know that naming is arbitrary, but...
Digits in types seems ugly to me. In this case, it is also redundant.
Everyone but FORTRAN programmers counts from 0, not 1. Nat and Pos seem
clear. Nat0 could even mean Nat \ {0}, the opposite of what is proposed,
so confusion is even increased with Nat0.
Dan
Alfonso Acosta wrote:
On Feb 7, 2008 4:16 PM, Wolfgang Jeltsch [EMAIL PROTECTED] wrote:
Nat means all natural numbers except zero while Nat0 means all natural
numbers (including zero). Since in computer science, natural numbers
usually cover zero, we should use Pos instead of Nat and Nat instead of Nat0.
Sounds sensible, actually Nat and Nat0 is confusing. However I would
rather use Pos and Nat0 to make explicit that naturals include zero .
Depending on the definition of naturals they might or might not
include zero. http://en.wikipedia.org/wiki/Natural_number
You seem to write 12 as 1 :+ 2 instead of () :+ 1 :+ 2. But I think, the
latter representation should probably be prefered. With it, :+ always has a
number as its left argument and a digit as its right. Without the () :+ we
get ugly exceptional cases.
You can see this, for example, in the instance
declarations for Compare. With the second representation, we could reduce
the number of instances dramatically. We would define a comparison of digits
(verbose) and than a comparison of numbers based on the digit comparison (not
verbose).
Even if () would be preferred from the programmers point of view (I'm
not sure how much we could reduce the number of instances though), it
makes the representation less attractive on the user-side. Anyone
using the library would find it annoying and would wonder why is it
neccessary.
Unless we find a way to use () only internally (we should use a
one-character type to make it shorter to type) I think we should stick
to current representation.
:+ is already used as the constructor for complex numbers. We should probably
use some different operator.
Right. I didn't think about that, thanks.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Mutable arrays
2008/2/7, Jeff φ [EMAIL PROTECTED]: I played with your foldl1MArray' last night. I noticed it can be reduced to . . . foldl1MArray' :: (MArray a e m, Ix i) = (e - e - e) - a i e - m e foldl1MArray' f a = do (l,u) - getBounds a foldl1' (liftM2 f) (map (readArray a) (range (l,u))) Unfortunately, my new version consumes a lot of stack and heap space. Why is this so inefficient? Is there a simple change that will make it efficient? This code don't compute the results incrementally, it can't because foldl1' is not aware of the monad, it only construct a huge action in m which is then run. foldM advantage is that it can run incrementally. Which is not to say my code was the best possible (far from it), already the following would have been better : foldlA f a arr = getBounds arr = foldM (\a-a `seq` liftM $ f a) a . map (readArray arr) . range foldl1A f arr = getBounds arr = readArray arr . fst = flip (foldlA f) arr -- Jedaï ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Implementing fixed-sized vectors (using datatype algebra?)
This may be a GHC bug, but even though in the module
Data.TypeLevel.Num.Reps has the header
{-# LANGUAGE EmptyDataDecls, TypeOperators #-}
I still get an error with both ghc and ghci version 6.8.2 unless I throw
in the -XTypeOperators flag.
cat Go.hs
import Data.TypeLevel.Num.Reps
main = return (undefined :: D2 :+ D1) print Done
ghc --make Go.hs
[1 of 1] Compiling Main ( Go.hs, Go.o )
Go.hs:3:31:
Illegal operator `:+' in type `D2 :+ D1'
(Use -XTypeOperators to allow operators in types)
ghc --make -XTypeOperators Go.hs
[1 of 1] Compiling Main ( Go.hs, Go.o )
Linking Go ...
ghc --version
The Glorious Glasgow Haskell Compilation System, version 6.8.2
Dan
Alfonso Acosta wrote:
Don't expect anything astonishing yet, but an initial version of the
library can be found at
http:/code.haskell.org/type-level
To make reviewing easier I have put the haddock-generated documentation at
http://code.haskell.org/~fons/type-level/doc/
Some remarks:
* Only Positive and Natural numerals in decimal representation are
supported. It would be cool to add support for Integers though.
* The code is based on Oleg's implimentation of type-level binaries
http://okmij.org/ftp/Computation/resource-aware-prog/BinaryNumber.hs
* exponentiation/log and GCD is not implemented yet
* multiplication is not relational and thus division is broken. I
tried porting Oleg's multiplication algorithm without success.
* Aliases (in binary, octal decimal and hexadecimal form) for
type-level values and their value-level reflection functions are
generated with TH.
That implies:
* Long compilation time depending on your system
* Although errors will always be reported in decimal form, the end
user can input values using other bases (only for values in the range
of generated aliases of course)
* It would be cool to have real support for other bases apart from decimals
* It would imply having unlimited size of input for other bases
(right now if we want to input a value out of the alises limit,
decimal reprentation is mandatory)
* However, is it feasible? How could it be done without needing to
implement the operations for each base? WOuld it be possible to
overload the type-level operators so that they worked with different
representations and mixed representation arguments?
* Booleans are not implemented (Wolfgang?)
I would be happy to hear any suggestions, get code reviews and/or contributions.
Cheers,
Fons
On Feb 7, 2008 11:17 AM, Wolfgang Jeltsch [EMAIL PROTECTED] wrote:
Am Donnerstag, 7. Februar 2008 02:47 schrieb Alfonso Acosta:
The other library I use for type-level programming is HList. It has
type-level booleans already so you might what to take a look at it if
you're not already familiar with it.
Thanks I'll have a look at it.
I have to admit that I don't like the names HBool, HTrue and HFalse. What do
they mean? Heterogenous booleans? Heterogenous truth? Why it's Bool
instead of Boolean and therefore not conforming to the Prelude convention?
Heterogenous lists are not directly about type level computation. A HList
type is usually inhabited. On the other hand, types which denote type level
naturals or type-level booleans are empty data types. So type level booleans
should go into some type level programming library like the one Alfonso and I
want to create. HList should then use these booleans. This is at least my
opinion.
Best wishes,
Wolfgang
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] FP and Quality
ICFP 2007 introduced a new category of paper called an Experience Report, which is not required to add to the body of research knowledge, but rather report on the effectiveness of functional tools and methods in full-scale projects. You can read the official description in the call for papers: http://www.icfpconference.org/icfp2008/cfp/cfp.html The ICFP 2007 schedule lists all the experience reports here: http://www.informatik.uni-bonn.de/~ralf/schedule.html You can get the PDFs for the experience report (and talk slides) we wrote describing our use of FP at Linspire here: http://seereason.com/publications/ Cliff On Feb 4, 2008 2:20 PM, PR Stanley [EMAIL PROTECTED] wrote: Hi folks I'm thinking of writing a little essay arguing the case for the advantages of FP for producing quality software. Can the list recommend any papers/articles which I can use as sources of my argument? I have access to the IEEE database too although earlier I couldn't find anything on the subject. Thanks, Paul ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Haskell maximum stack depth
Neil Mitchell wrote: Hi But the point is that *both* heapGobbler and neilGobbler are likely to be slower and chew through at least twice as much heap as stackGobbler, which would be the implementation of choice for both simplicity and performance if it wasn't for this stack management problem. Sure? Yes, though testing stackGobbler with a large enough data set could be problematic for the very reason we've been discsussing. But let's say your hypothesis was correct. If so then presumably *all* Haskell programs could give better performance than they currently do if we nuked the stack completely and have ghc generate CPS style code. This too would be fine with me. The problem with the current situation is that we have perfectly sound and correct programs that crash quite unnecessarily (and even if they don't get quite that far, can still cause considerable per thread memory wastage if what SPJ says is true). Why their authors choose to use a stack greedy implementation and whether that was by design or a mistake really *isn't* the point. As I said before (this is the third time I think), the fact that these programs use a lot of stack at all is just a peculiarity of *ghc* implementation, so it really is a ghc responsibility to do a decent job of stack management IMO. It's not a programmer responsibility to code in such a way that minimal stack is used (with ghc). That sounds like the thing that people can conjecture, but benchmarks can prove. And I'd claim that neilGobbler is the simplest function by a large margin. AFAICT neilGobbler isn't even entirely safe as an implementation of an eager take. There's nothing the Haskell standard to stop it being transformed into.. neilGobbler :: Int - [x] - [x] neilGobbler n xs = length (take n xs) `seq` take n xs Regards -- Adrian Hey ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Haskell maximum stack depth
Neil Mitchell wrote: Hi I have already partially scanned the list looking for the first element that satisfies some condition, using a tail recursive search. If such an element is found I want to split the list at that point. span/break? I really can't believe the memory overhead of span is that terrible, you are only duplicating the (:)'s and its only one traversal. As an aside, my version of this function would be: neilGobbler :: Int - [x] - [x] neilGobbler n xs = length res `seq` res where res = take n xs My guess is it will use O(1) stack and burn O(n) heap (in addition that actually used by the result), so assymptotic complexity wise same as heapGobbler, but probably higher constant factors with ghc due to lazy building of take thunks and subsequent reduction and indirection costs. Sure? Guessing constant factors related to strictness and laziness is incredibly hard! My guess based on gut feeling is that the program will take less time, and use half the memory. But given my initial comment, that guess is not very reliable. But the point is that *both* heapGobbler and neilGobbler are likely to be slower and chew through at least twice as much heap as stackGobbler, which would be the implementation of choice for both simplicity and performance if it wasn't for this stack management problem. Regards -- Adrian Hey ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] question concerning ANSI void *
Hello,
Ok .. I am writing a Haskell function that will call down into the ANSI
C library .. blah :: - Ptr Word8 - The underlying C function
that blah is calling has a void * so I am using Ptr Word 8 to model
the void *. I propose to have the callers of function blah to populate a
data structure something like Ptr Buz where data Buz = { } and
then do a recast :: Ptr Word 8 - Ptr Buz when invoking function blah.
Does this seem reasonable? Is there a better way?
Thanks, Vasili
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Two Lectureships in Nottingham
Dear all, We are advertising two new Lectureships (Assistant Professorships) in Computer Science at the University of Nottingham in England. Applications in the area of functional programming are particularly welcome. Further details are available from: http://jobs.nottingham.ac.uk/vacancies.aspx?cat=160#j2797 The closing date for applications is 22nd Feburary 2008 Best wishes, Graham Hutton +-+ | Dr Graham Hutton Email : [EMAIL PROTECTED] | | School of Computer Science | | University of Nottingham Web : www.cs.nott.ac.uk/~gmh | | Jubilee Campus, Wollaton Road | | Nottingham NG8 1BB, UK Phone : +44 (0)115 951 4220| +-+ This message has been checked for viruses but the contents of an attachment may still contain software viruses, which could damage your computer system: you are advised to perform your own checks. Email communications with the University of Nottingham may be monitored as permitted by UK legislation. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Mutable arrays
On Feb 2, 2008 12:11 PM, Chaddaï Fouché [EMAIL PROTECTED] wrote: To address this I propose this function : foldl1MArray' :: (MArray a e m, Ix i) = (e - e - e) - a i e - m e foldl1MArray' f a = do (l,u) - getBounds a firstElem - readArray a l foldM (\a mb - a `seq` mb = return . f a) firstElem (map (readArray a) (range (l,u))) I played with your foldl1MArray' last night. I noticed it can be reduced to . . . foldl1MArray' :: (MArray a e m, Ix i) = (e - e - e) - a i e - m e foldl1MArray' f a = do (l,u) - getBounds a foldl1' (liftM2 f) (map (readArray a) (range (l,u))) Unfortunately, my new version consumes a lot of stack and heap space. Why is this so inefficient? Is there a simple change that will make it efficient? ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] User groups meeting all over the world
The community might be interested to know that there are (at least) 7 Haskell/FP user groups meeting across the world in the next two weeks! FringeDCWashington DC/USAFebruary 9 PDXFunc Portland/USA February 11 Fun in the afternoonLondon/UKFebruary 12 BayFP San Francisco/USAFebruary 13 Saint-Petersburg Haskell User Group Saint-Petersburg/Russia. February 16 NYFP NetworkNew York/USA February 19 NWFPIG: Seattle FP GroupSeattle/USA February 20 The Austin (Texas) group met a couple of weeks ago. This is a great development -- a year ago I don't think we had *any* groups meeting regularly. Consider dropping in to one, if there's a meetting near you, or starting your own group! All groups we know about are listed here: http://www.haskell.org/haskellwiki/User_groups -- Don ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Implementing fixed-sized vectors (using datatype algebra?)
On Feb 7, 2008 4:16 PM, Wolfgang Jeltsch [EMAIL PROTECTED] wrote: Nat means all natural numbers except zero while Nat0 means all natural numbers (including zero). Since in computer science, natural numbers usually cover zero, we should use Pos instead of Nat and Nat instead of Nat0. Sounds sensible, actually Nat and Nat0 is confusing. However I would rather use Pos and Nat0 to make explicit that naturals include zero . Depending on the definition of naturals they might or might not include zero. http://en.wikipedia.org/wiki/Natural_number You seem to write 12 as 1 :+ 2 instead of () :+ 1 :+ 2. But I think, the latter representation should probably be prefered. With it, :+ always has a number as its left argument and a digit as its right. Without the () :+ we get ugly exceptional cases. You can see this, for example, in the instance declarations for Compare. With the second representation, we could reduce the number of instances dramatically. We would define a comparison of digits (verbose) and than a comparison of numbers based on the digit comparison (not verbose). Even if () would be preferred from the programmers point of view (I'm not sure how much we could reduce the number of instances though), it makes the representation less attractive on the user-side. Anyone using the library would find it annoying and would wonder why is it neccessary. Unless we find a way to use () only internally (we should use a one-character type to make it shorter to type) I think we should stick to current representation. :+ is already used as the constructor for complex numbers. We should probably use some different operator. Right. I didn't think about that, thanks. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] background question about IO monad
On 2/6/08, Uwe Hollerbach [EMAIL PROTECTED] wrote:
And, coming back to my scheme interpreter, this is at least somewhat
irrelevant, because, since I am in a REPL of my own devising, I'm
firmly in IO-monad-land, now and forever.
This is not entirely true; a REPL can be pure.
Consider the following simple stack-based-calculator; all the IO
happens within interact, the REPL itself is pure:
import System.IO
main = hSetBuffering stdout NoBuffering interact replMain
replMain s = Stack calculator\n ++ repl [] s
repl :: [Int] - String - String
repl _ [] =
repl _ ('q':_) =
repl s ('\n':xs) = show s ++ \n ++ repl s xs
repl s xs@(x:_) | x = '0' x = '9' =
let (v, xs') = head $ reads xs in repl (v:s) xs'
repl s (c:xs) | c `elem` validCommands = case command c s of
Just s' - repl s' xs
Nothing - stack underflow\n ++ repl s xs
repl s (_:xs) = repl s xs -- ignore unrecognized characters
validCommands = .d+c
command :: Char - [Int] - Maybe [Int]
command '.' (x:xs) = Just xs
command 'd' (x:xs) = Just $ x:x:xs
command '+' (x:y:xs) = Just $ (x+y):xs
command 'c' _ = Just []
command _ _ = Nothing
You can go further than interact if you want to abstract away the
impurity in your system and take input from some outside process which
has a limited set of impure operations. Take a look here for an
example using Prompt (which has seen some discussion here on
haskell-cafe): http://paste.lisp.org/display/53766
In that example, guess n is an action in the pure Prompt monad;
different interpretation functions allow this monad to interact with
an AI (in a semi-pure setting; it outputs strings), or with a real
player via the full IO interface. A similar mechanism could be used
for the scheme REPL to make it as pure as possible, with
getClockTime being replaced by prompt GetClockTime to interact
with the outside world.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] User groups meeting all over the world
I will only consider events where they serve free tea and sandwiches, plus if there's a landing pad for the chopper nearby. :-) At 23:11 07/02/2008, you wrote: The community might be interested to know that there are (at least) 7 Haskell/FP user groups meeting across the world in the next two weeks! FringeDCWashington DC/USAFebruary 9 PDXFunc Portland/USA February 11 Fun in the afternoonLondon/UKFebruary 12 BayFP San Francisco/USAFebruary 13 Saint-Petersburg Haskell User Group Saint-Petersburg/Russia. February 16 NYFP NetworkNew York/USA February 19 NWFPIG: Seattle FP GroupSeattle/USA February 20 The Austin (Texas) group met a couple of weeks ago. This is a great development -- a year ago I don't think we had *any* groups meeting regularly. Consider dropping in to one, if there's a meetting near you, or starting your own group! All groups we know about are listed here: http://www.haskell.org/haskellwiki/User_groups -- Don ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Signature for non-empty filter
Hi Bulat, Once again, let's be careful about what check arbitrary functions for termination/non-trivialness means. If you mean, decide via an algorithm whether a function is terminating on all inputs, then yes, you need to restrict the class of functions. If you mean prove in some logic that a function is terminating on all inputs, then there is no reason to restrict the class of functions. (Think of it this way: the truth of propositions in that logic may not be decidable, so the existence of a proof of termination in that logic does not imply an algorithm for deciding termination.) ACL2 and Twelf are practical systems built around this second kind of reasoning. In these systems, you write down partial functions (in a functional notation in ACL2, in a logic programming notation in Twelf) and then prove that they are terminating, and therefore total. Both systems permit the definition of all computable functions on the natural numbers (worst comes to worst, you can write an interpreter for the untyped lambda-calculus). So in neither system is it *decidable* whether a function is terminating. However, both provide helpful tools for proving that individual functions are terminating, and in both systems you can help these tools along yourself when the automated reasoning doesn't do the job. Many dependently typed programming languages have this flavor, in that you can prove propositions that are not decidable. Propositions are represented by types, and proofs by programs, so the truth of a proposition comes down to the existence of a term of a particular type. There is no reason that type inhabitation (and therefore all propositions) needs to be decidable. So it is perfeclty possible to have a dependent type system where you give filter the type for all satisfiable f where f ranges over all computable functions of the appropriate type, even though this proposition is not decidable. -Dan On Feb07, Bulat Ziganshin wrote: Hello Henning, Thursday, February 7, 2008, 4:27:30 PM, you wrote: ok, read this as computer can ensure..., because it was exactly the original question - can computer check that any given function in turing-complete language is non-trivial? My original question according to http://www.haskell.org/pipermail/haskell-cafe/2008-February/039161.html was Is Haskell's type system including extensions strong enough for describing a function, that does not always return a trivial value? where Haskell is *turing-complete* *computer* language this allows to answer to your question that you need to use special, non-turing language if you want to check arbitrary functions for non-trivialness. one example of such language: data Func = ConstTrue | ConstFalse and dependent-typed languages provides you (afaiu) much richer facilities to describe functions for which you still may prove something useful so, if you term function includes the Func type, the answer is yes, but if you mean usual haskell functions, the answer is no ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Implementing fixed-sized vectors (using datatype algebra?)
On Feb 7, 2008 8:38 PM, Dan Weston [EMAIL PROTECTED] wrote:
I know that naming is arbitrary, but...
Digits in types seems ugly to me. In this case, it is also redundant.
Everyone but FORTRAN programmers counts from 0, not 1. Nat and Pos seem
clear. Nat0 could even mean Nat \ {0}, the opposite of what is proposed,
so confusion is even increased with Nat0.
Ok, fair enough. I changed the names of Positives and Naturals (which
do include 0) for Pos and Nat.
The change (together with a connective rename from :+ to :* ) is
already pushed in the darcs repository.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Implementing fixed-sized vectors (using datatype algebra?)
On 8 Feb 2008, at 8:38 am, Dan Weston wrote:
I know that naming is arbitrary, but...
Digits in types seems ugly to me. In this case, it is also
redundant. Everyone but FORTRAN programmers counts from 0, not 1.
Nat and Pos seem clear. Nat0 could even mean Nat \ {0}, the
opposite of what is proposed, so confusion is even increased with
Nat0.
For what it's worth, the Ada names for the types
{x in Z | x = 0}
and {x in Z | x 0}
are Natural and Positive respectively. Natural is useful for
counting stuff;
Positive is useful mainly because Ada practice is to index from 1.
In Z, |N is used for natural numbers, which are defined to include 0.
In modern set theory, both the cardinal and the ordinal numbers start
with
0, not with 1.
All things considered, I would be very upset indeed if a type called
Nat
or Natural or something like that did not include 0.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] User groups meeting all over the world
On 2/7/08 3:21 PM, PR Stanley wrote: I will only consider events where they serve free tea and sandwiches, plus if there's a landing pad for the chopper nearby. :-) BayFP's next one _might_ be at a place rhyming with Loogle[1], so that'd be organic tea and I'm certain there's a landing pad HTH, Keith 1. We're still working on the location ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: modeling ANSI C structs in Haskell?
Galchin Vasili wrote: I am reading through the FFI doc. Any suggestions on enabling Haskell programmers to model ANSI C structs that will be passed down to C run-time? If you have a C function that needs to be passed a struct, then there are three scenarios: (a) A common situation is that your C struct is opaque (or at least meant to be used opaquely). You'll have explicit allocate+construct functions as well as deallocate+destruct functions in your C library. This means that you don't care at all how to marshall the struct, you don't even (need to) know how it looks like. All you work with is pointers (i.e. Ptr a, or Ptr X where X is an empty data type). You can use ForeignPtr to automatically call the Library provided destructor when the GC finds that the pointer is no longer accessible in your program (from the Haskell side). (b) In case the C function expects a pointer to a user allocated struct, your type X will probably be a Haskell record, and you want to make X an instance of class Storable. You can allocate and deallocate the C struct by using one of the functions provided by Foreign.Marshal.Alloc. (c) Most uncommon (though not not unheard of): the function gets the struct passed by value. This means you can't write the FFI code completely in Haskell because Haskell FFI can only work with C primitive types (numbers, pointers, etc). You need to write a little C wrapper to convert pass-by-value to pass-by-reference. Then see case (b). HTH Ben ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] :i and :t give different types
On 7 Feb 2008, at 12:30 PM, Chad Scherrer wrote: On Feb 7, 2008 11:57 AM, Don Stewart [EMAIL PROTECTED] wrote: Ah, yes, missing parens! Well spotted. So a pretty printer wibble in GHC? -- Don Yeah, that was my first concern, but then I noticed the quantification was different, so I'm still working through that one. The quantification isn't different, just differently presented. In Haskell 98, there are never explicit foralls and any type is implicitly quantified over its free variables at the top level. So, in GHC a type without explicit foralls is quantified over its free variables at the top level. So the two types are in fact equal. It was confusing, since I assumed the implementations of :i and :t shared a lot of code. Apparently not :) jcc ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] background question about IO monad
Thanks, I'm going to have to study this a bit...
Uwe
On 2/7/08, Ryan Ingram [EMAIL PROTECTED] wrote:
On 2/6/08, Uwe Hollerbach [EMAIL PROTECTED] wrote:
And, coming back to my scheme interpreter, this is at least somewhat
irrelevant, because, since I am in a REPL of my own devising, I'm
firmly in IO-monad-land, now and forever.
This is not entirely true; a REPL can be pure.
Consider the following simple stack-based-calculator; all the IO
happens within interact, the REPL itself is pure:
import System.IO
main = hSetBuffering stdout NoBuffering interact replMain
replMain s = Stack calculator\n ++ repl [] s
repl :: [Int] - String - String
repl _ [] =
repl _ ('q':_) =
repl s ('\n':xs) = show s ++ \n ++ repl s xs
repl s xs@(x:_) | x = '0' x = '9' =
let (v, xs') = head $ reads xs in repl (v:s) xs'
repl s (c:xs) | c `elem` validCommands = case command c s of
Just s' - repl s' xs
Nothing - stack underflow\n ++ repl s xs
repl s (_:xs) = repl s xs -- ignore unrecognized characters
validCommands = .d+c
command :: Char - [Int] - Maybe [Int]
command '.' (x:xs) = Just xs
command 'd' (x:xs) = Just $ x:x:xs
command '+' (x:y:xs) = Just $ (x+y):xs
command 'c' _ = Just []
command _ _ = Nothing
You can go further than interact if you want to abstract away the
impurity in your system and take input from some outside process which
has a limited set of impure operations. Take a look here for an
example using Prompt (which has seen some discussion here on
haskell-cafe): http://paste.lisp.org/display/53766
In that example, guess n is an action in the pure Prompt monad;
different interpretation functions allow this monad to interact with
an AI (in a semi-pure setting; it outputs strings), or with a real
player via the full IO interface. A similar mechanism could be used
for the scheme REPL to make it as pure as possible, with
getClockTime being replaced by prompt GetClockTime to interact
with the outside world.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] I love purity, but it's killing me.
As I pointed out a few days ago in another thread, you can benefit from using Observable sharing [1] Be warned that Observable sharing is a non-conservative extension of Haskell and it breaks referential transparency. [1] http://www.cs.chalmers.se/~koen/pubs/entry-asian99-lava.html On Feb 8, 2008 7:33 AM, Tom Hawkins [EMAIL PROTECTED] wrote: I've been programming with Haskell for a few years and love it. One of my favorite applications of Haskell is using for domain specific languages. However, after designing a handful of DSLs, I continue to hit what appears to be a fundamental hurdle -- or at least I have yet to find an adequate solution. My DSLs invariably define a datatype to capture expressions; something like this: data Expression = Add Expression Expression | Sub Expression Expression | Variable String | Constant Int deriving Eq Using the datatype Expression, it is easy to mass a collections of functions to help assemble complex expressions, which leads to very concise programs in the DSL. The problem comes when I want to generate efficient code from an Expression (ie. to C or some other target language). The method I use invovles converting the tree of subexpressions into an acyclic graphic to eliminate common subexpressions. The nodes are then topologically ordered and assigned an instruction, or statement for each node. For example: let a = Add (Constant 10) (Variable i1) b = Sub (Variable i2) (Constant 2) c = Add a b would compile to a C program that may look like this: a = 10 + i1; b = i2 - 2; c = a + b; The process of converting an expression tree to a graph uses either Eq or Ord (either derived or a custom instance) to search and build a set of unique nodes to be ordered for execution. In this case a, then b, then c. The problem is expressions often have shared, equivalent subnodes, which dramatically grows the size of the tree. For example: let d = Add c c e = Add d d-- e now as 16 leaf nodes. As these trees grow in size, the equality comparison in graph construction quickly becomes the bottleneck for DSL compilation. What's worse, the phase transition from tractable to intractable is very sharp. In one of my DSL programs, I made a seemingly small change, and compilation time went from milliseconds to not-in-a-million-years. Prior to Haskell, I wrote a few DSLs in OCaml. I didn't have this problem in OCaml because each let expression was mutable, and I could use the physical equality operator to perform fast comparisons. Unfortunately, I have grown to love Haskell's type system and its lack of side effects, and could never go back. Is there anything that can be done to dramatically speed up comparisons, or is there a better approach I can take to extract common subexpressions? I should point out I have an opportunity to get Haskell on a real industrial application. But if I can't solve this problem, I may have to resort to far less eloquent languages. :-( Thanks for any and all help. -Tom ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] I love purity, but it's killing me.
I've been programming with Haskell for a few years and love it. One of my favorite applications of Haskell is using for domain specific languages. However, after designing a handful of DSLs, I continue to hit what appears to be a fundamental hurdle -- or at least I have yet to find an adequate solution. My DSLs invariably define a datatype to capture expressions; something like this: data Expression = Add Expression Expression | Sub Expression Expression | Variable String | Constant Int deriving Eq Using the datatype Expression, it is easy to mass a collections of functions to help assemble complex expressions, which leads to very concise programs in the DSL. The problem comes when I want to generate efficient code from an Expression (ie. to C or some other target language). The method I use invovles converting the tree of subexpressions into an acyclic graphic to eliminate common subexpressions. The nodes are then topologically ordered and assigned an instruction, or statement for each node. For example: let a = Add (Constant 10) (Variable i1) b = Sub (Variable i2) (Constant 2) c = Add a b would compile to a C program that may look like this: a = 10 + i1; b = i2 - 2; c = a + b; The process of converting an expression tree to a graph uses either Eq or Ord (either derived or a custom instance) to search and build a set of unique nodes to be ordered for execution. In this case a, then b, then c. The problem is expressions often have shared, equivalent subnodes, which dramatically grows the size of the tree. For example: let d = Add c c e = Add d d-- e now as 16 leaf nodes. As these trees grow in size, the equality comparison in graph construction quickly becomes the bottleneck for DSL compilation. What's worse, the phase transition from tractable to intractable is very sharp. In one of my DSL programs, I made a seemingly small change, and compilation time went from milliseconds to not-in-a-million-years. Prior to Haskell, I wrote a few DSLs in OCaml. I didn't have this problem in OCaml because each let expression was mutable, and I could use the physical equality operator to perform fast comparisons. Unfortunately, I have grown to love Haskell's type system and its lack of side effects, and could never go back. Is there anything that can be done to dramatically speed up comparisons, or is there a better approach I can take to extract common subexpressions? I should point out I have an opportunity to get Haskell on a real industrial application. But if I can't solve this problem, I may have to resort to far less eloquent languages. :-( Thanks for any and all help. -Tom ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] I love purity, but it's killing me.
I know of a few of ways to express sharing in a pure language: 1) Observable sharing, which, in general, is unsafe. http://www.cs.chalmers.se/~koen/pubs/entry-asian99-lava.html 2) Using Template Haskell http://www.dcs.gla.ac.uk/publications/PAPERS/7524/EmbedHDLinTH.ps 3) Matthew Naylor has done some work on expressible sharing, which has advantages over both methods above. I don't have any reference though... 4) Use a monad (but I'm sure this is what you're trying to avoid). / Emil On 2008-02-08 07:33, Tom Hawkins wrote: I've been programming with Haskell for a few years and love it. One of my favorite applications of Haskell is using for domain specific languages. However, after designing a handful of DSLs, I continue to hit what appears to be a fundamental hurdle -- or at least I have yet to find an adequate solution. My DSLs invariably define a datatype to capture expressions; something like this: data Expression = Add Expression Expression | Sub Expression Expression | Variable String | Constant Int deriving Eq Using the datatype Expression, it is easy to mass a collections of functions to help assemble complex expressions, which leads to very concise programs in the DSL. The problem comes when I want to generate efficient code from an Expression (ie. to C or some other target language). The method I use invovles converting the tree of subexpressions into an acyclic graphic to eliminate common subexpressions. The nodes are then topologically ordered and assigned an instruction, or statement for each node. For example: let a = Add (Constant 10) (Variable i1) b = Sub (Variable i2) (Constant 2) c = Add a b would compile to a C program that may look like this: a = 10 + i1; b = i2 - 2; c = a + b; The process of converting an expression tree to a graph uses either Eq or Ord (either derived or a custom instance) to search and build a set of unique nodes to be ordered for execution. In this case a, then b, then c. The problem is expressions often have shared, equivalent subnodes, which dramatically grows the size of the tree. For example: let d = Add c c e = Add d d-- e now as 16 leaf nodes. As these trees grow in size, the equality comparison in graph construction quickly becomes the bottleneck for DSL compilation. What's worse, the phase transition from tractable to intractable is very sharp. In one of my DSL programs, I made a seemingly small change, and compilation time went from milliseconds to not-in-a-million-years. Prior to Haskell, I wrote a few DSLs in OCaml. I didn't have this problem in OCaml because each let expression was mutable, and I could use the physical equality operator to perform fast comparisons. Unfortunately, I have grown to love Haskell's type system and its lack of side effects, and could never go back. Is there anything that can be done to dramatically speed up comparisons, or is there a better approach I can take to extract common subexpressions? I should point out I have an opportunity to get Haskell on a real industrial application. But if I can't solve this problem, I may have to resort to far less eloquent languages. :-( Thanks for any and all help. -Tom ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
