- Haskell-Cafe - Haskell.org

Re: [Haskell] Lemmas about type functions
by Ryan Ingram 16 Feb '08

16 Feb '08

[moved to haskell-cafe] Hmm, there's a problem here. Since type functions are open, it's not actually true that (forall ts. Cat ts () = ts), because someone could add, for example type instance Cat [a] () = [(a,a)] which makes the lemma no longer true. What you are doing in cat_nil is not proving that Cat ts () = ts, but rather that the form of ts is a particular form which makes that theorem hold, in particular, for all types ts of the form ts = (t1, (t2, ..., (tN, ()) ... )) Cat ts () = ts So for your lemma to hold, you need a new judgement "Valid ts": class Valid ts where cat_nil :: Equiv (Cat ts ()) ts -- other lemmas here instance Valid () where cat_nil = Equiv instance Valid x => Valid (a, x) where cat_nil = case (cat_nil :: Equiv (Cat x ()) x) of Equiv -> Equiv coerce :: forall f ts. Valid ts => f (Cat ts ()) -> f ts coerce x = case (cat_nil :: Equiv (Cat ts ()) ts) of Equiv -> x Also, I'm not sure if GHC can currently optimize away cat_nil; it's clear by construction that cat_nil is total, but if the compiler can't detect that it needs to run and make sure it returns Equiv and not _|_. Otherwise you get an unsound result: (given the type instance above) instance Valid [a] where cat_nil = cat_nil Oleg has pointed out this problem with GADTs as type witnesses here: http://okmij.org/ftp/Haskell/GADT-problem.hs -- ryan On 2/15/08, Ryan Ingram <ryani.spam(a)gmail.com> wrote: > I am pretty sure that this doesn't exist, but it's quite interesting. > I've submitted a feature request here: > > http://hackage.haskell.org/trac/ghc/ticket/2101 > > On 2/15/08, Louis-Julien Guillemette <guillelj(a)iro.umontreal.ca> wrote: > > Hi all, > > > > I've been using GHC's type families somewhat extensively in my > > type-preserving compiler (BTW, they work great), and quite often I > > come across the need to prove lemmas about those functions. As far as > > I understand there's currently no way to handle such lemmas purely at > > the type level, and I have to encode them as term-level functions. > > > > I wonder if I'm missing something, or otherwise if there are plans to > > provide some way to do this kind of type-level reasoning. > > > > Here's a simple example. > > > > I encode (de Bruijn) type contexts as lists of types of this form: > > > > (t0, (t1, (... , ()...))) > > > > I sometimes concatenate type contexts, and need a lemma stating that > > appending an empty context leaves it unchanged (ts ++ [] == ts). > > > > type family Cat ts0 ts > > type instance Cat () ts' = ts' > > type instance Cat (s, ts) ts' = (s, Cat ts ts') > > > > That is, I need to coerce: > > > > Exp (Cat ts ()) > > > > into: > > > > Exp ts > > > > The way I presently do it is through a term-level function that > > produces a witness that the two types are equivalent, like this: > > > > data Equiv s t where > > Equiv :: (s ~ t) => Equiv s t > > > > cat_nil :: EnvRep ts -> Equiv (Cat ts ()) ts > > cat_nil R0 = Equiv > > cat_nil (Rs _ ts_r) = case cat_nil ts_r of Equiv -> Equiv > > > > coerce :: EnvRep ts -> Exp (Cat ts ()) -> Exp ts > > coerce ts_r e = case cat_nil ts_r of Equiv -> e > > > > > > Louis > > > > _______________________________________________ > > Haskell mailing list > > Haskell(a)haskell.org > > http://www.haskell.org/mailman/listinfo/haskell > > >

1 0

set terminology
by PR Stanley 15 Feb '08

15 Feb '08

Hi domain, source --- are the two different things? I'm sure I read somewhere that the source \subseteq domain in mappings. The same was said about range and target -- target \subseteq range. Any ideas? Thanks, Paul

2 2

ANN: two new packages: carray, fft
by Jed Brown 15 Feb '08

15 Feb '08

Hopefully these are mature enough to be generally useful. I would appreciate any comments regarding the interface. The FFTW API is not particularly nice for building a pure interface on. Some of the transforms could be made slightly faster at the expense of a much nastier interface, but unless someone needs the extra few percent, or is pushing the memory limits on their machine, I'm not inclined to expose the underlying nastiness. * carray A C-compatible array library. Provides both an immutable and mutable (in the IO monad) interface. Includes utilities for multi-dimensional arrays, slicing and norms. Memory is 16-byte aligned by default to enable use of SIMD instructions. http://hackage.haskell.org/cgi-bin/hackage-scripts/package/carray * fft Bindings to the FFTW library. Provides high performance discrete fourier transforms in arbitrary dimensions. Include transforms of complex data, real data, and real to real transforms. http://hackage.haskell.org/cgi-bin/hackage-scripts/package/fft Jed

3 5

Re: [Haskell-cafe] fast integer base-2 log function?
by Thorkil Naur 15 Feb '08

15 Feb '08

Hello, If the standard libraries provide such a function, I haven't found it. I must admit that I haven't studied your code in detail. I usually do as follows for integer logarithms, shamelessly stolen from the Haskell report: > -- Integer log base (c.f. Haskell report 14.4): > > imLog :: Integer->Integer->Integer > imLog b x > = if x < b then > 0 > else > let > l = 2 * imLog (b*b) x > doDiv x l = if x < b then l else doDiv (x`div`b) (l+1) > in > doDiv (x`div`(b^l)) l Best regards Thorkil On Monday 11 February 2008 07:15, Uwe Hollerbach wrote: > Hello, haskellers, > > Is there a fast integer base-2 log function anywhere in the standard > libraries? I wandered through the index, but didn't find anything that > looked right. I need something that's more robust than logBase, it > needs to handle numbers with a few to many thousands of digits. I > found a thread from a couple of years ago that suggested there was no > such routine, and that simply doing "length (show n)" might be the > best. That seems kind of... less than elegant. I've come up with a > routine, shown below, that seems reasonably fast (a few seconds of CPU > time for a million-bit number, likely adequate for my purposes), but > it seems that something with privileged access to the innards of an > Integer ought to be even much faster -- it's just a simple walk along > a list (array?) after all. Any pointers? Thanks! > > Uwe > > > powi :: Integer -> Integer -> Integer > > powi b e | e == 0 = 1 > > | e < 0 = error "negative exponent in powi" > > | even e = powi (b*b) (e `quot` 2) > > | otherwise = b * (powi b (e - 1)) > > > ilog2 :: Integer -> Integer > > ilog2 n | n < 0 = ilog2 (- n) > > | n < 2 = 1 > > | otherwise = up n (1 :: Integer) > > where up n a = if n < (powi 2 a) > > then bin (quot a 2) a > > else up n (2*a) > > bin lo hi = if (hi - lo) <= 1 > > then hi > > else let av = quot (lo + hi) 2 > > in if n < (powi 2 av) > > then bin lo av > > else bin av hi > > (This was all properly aligned when I cut'n'pasted; proportional fonts > might be messing it up here.) > _______________________________________________ > Haskell-Cafe mailing list > Haskell-Cafe(a)haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe >

4 5

fast integer base-2 log function?
by Uwe Hollerbach 15 Feb '08

15 Feb '08

Hello, haskellers, Is there a fast integer base-2 log function anywhere in the standard libraries? I wandered through the index, but didn't find anything that looked right. I need something that's more robust than logBase, it needs to handle numbers with a few to many thousands of digits. I found a thread from a couple of years ago that suggested there was no such routine, and that simply doing "length (show n)" might be the best. That seems kind of... less than elegant. I've come up with a routine, shown below, that seems reasonably fast (a few seconds of CPU time for a million-bit number, likely adequate for my purposes), but it seems that something with privileged access to the innards of an Integer ought to be even much faster -- it's just a simple walk along a list (array?) after all. Any pointers? Thanks! Uwe > powi :: Integer -> Integer -> Integer > powi b e | e == 0 = 1 > | e < 0 = error "negative exponent in powi" > | even e = powi (b*b) (e `quot` 2) > | otherwise = b * (powi b (e - 1)) > ilog2 :: Integer -> Integer > ilog2 n | n < 0 = ilog2 (- n) > | n < 2 = 1 > | otherwise = up n (1 :: Integer) > where up n a = if n < (powi 2 a) > then bin (quot a 2) a > else up n (2*a) > bin lo hi = if (hi - lo) <= 1 > then hi > else let av = quot (lo + hi) 2 > in if n < (powi 2 av) > then bin lo av > else bin av hi (This was all properly aligned when I cut'n'pasted; proportional fonts might be messing it up here.)

3 2

Proper exception handling
by Thomas DuBuisson 15 Feb '08

15 Feb '08

Cafe, Fact 1: ghc{,i} does not crash when executing this code. Fact 2: I do not want this to crash. Question: Is there some theoretical window between the 'catchDyn' exception handling and the recursive call to 'catchThatDamnError' that could result in an unhandled exception? (of type 'DynError', of coarse) I suppose I am looking for an answer to this question from a language standpoint as well as a compiler pov. As an aside: I see at least one way to be certain of the safty by wrapping the call to forkIO in 'catchDyn', reforking if an exception is caught, and passing the new ThreadId to throwConstantly via shared mutable state - I'd like to avoid all this if my current example is safe. Thomas > import Control.Exception (catchDyn, throwDynTo) > import Control.Concurrent (forkIO, threadDelay) > import Control.Monad (forever) > import Data.Dynamic > > main = do > tid <- forkIO catchThatDamnError > forever $ throwConstantly tid > > catchThatDamnError = catchDyn start (\DynError -> catchThatDamnError) > > start = do > threadDelay 5000 > start > > throwConstantly tid = do > throwDynTo tid DynError > > data DynError = DynError deriving (Eq, Ord, Show, Typeable)

4 3

Re: [Haskell-cafe] Mutable arrays
by Jeff φ 15 Feb '08

15 Feb '08

On Feb 5, 2008 4:58 PM, Chaddaï Fouché <chaddai.fouche(a)gmail.com> wrote: > 2008/2/5, Jeff φ <jeff1.61803(a)gmail.com>: > > This is interesting. I've been programming in Concurrent Clean for a > while. > > Instead of monads, Clean supports unique types for mutable arrays and > IO. > > In Clean, I can write code that iterates through a mutable array by > > converting it to a lazy list. This is convenient because I can use all > the > > nice list processing functions that are available. > > > > You could absolutely write something like that in Haskell, but as some > have pointed out, this is probably _not a Good Idea_, even though it > works in your particular case, the array could be modified between the > time you get the lazy list and the time you actually read it... And > there's no way to insure it's not happening in Haskell, and I strongly > doubt there is in Concurrent Clean, could you confirm ? > Concurrent Clean can handle this in a safe way. Here's a code snippet for normalize_2D_ary from ArrayTest.icl: uToList_2D :: *(a u:(b c)) -> (.[c],*(a u:(b c))) | Array a (b c) & Array b c map_in_place_2d_arr :: (a -> a) *(b *(c a)) -> *(b *(c a)) | Array b (c a) & Array c a normalize_2D_ary :: *(a *(b c)) -> *(a *(b c)) | Array a (b c) & Array b c & / c & Ord c normalize_2D_ary ary = let (lst,ary2) = uToList_2D ary max_elem = foldl1 max lst in map_in_place_2d_arr (\ x -> x / max_elem) ary2 uToList_2D takes a unique array, ary, and returns a tuple containing a list of the array elements and a "new" array, ary2. uToList_2D does not modify ary, but Clean's type system forces any function that accesses a unique array to thread the array through and return a "new" array. Under the hood the "new" array actually uses the same memory storage as the original array. So, it is effecient. Threading the array serializes access insuring the array won't be modified until the list is complete. The type system will generate an error if I wrote code that breaks referential transparency. Array and IO Monads can be implemented in Clean on top of the uniqueness type system. The do-notation could be added to the language. However, the comments I've read so far lead me to believe the code I've shown cannot be implemented in Haskell using a lazy list without resorting to unsafe functions. I'm beginning to suspect the uniqueness type system of Clean is more general and flexible than Haskell's monads.

11 25

Re: [Haskell] Mailing List Archive: Search Broken?
by Janis Voigtlaender 15 Feb '08

15 Feb '08

Don Stewart wrote: > voigt: > >>Hi, >> >>it seems that something is wrong with the search on >> >> http://www.mail-archive.com/haskell@haskell.org/ >> >>Only messages from Nov and Dec 2007 are found, no matter what search >>phrases and date ranges are given. >> >>Worked yesterday and delivered search results over the whole history of >>the archive. >> >>Same for haskell-cafe. >> >>Anyone knows what is going on? > > > I always use gmane, via: > > http://news.gmane.org/search.php?match=haskell The problem with this is that when searching through gmane, and selecting a single message with a hit, one gets only to see that message without its context thread. At least I could not find out a way to switch from the found message to the thread in which it occurred. The search facility on www.mail-archive.com is much nicer in that respect, but as mentioned, as of yesterday seems to have forgotten about all messages prior to November 2007, and from 2008. Too bad... Ciao, Janis. -- Dr. Janis Voigtlaender http://wwwtcs.inf.tu-dresden.de/~voigt/ mailto:voigt@tcs.inf.tu-dresden.de

3 5

Re: [Haskell-cafe] ANN: ctemplate, SSL server support in HsOpenSSL, network-minihttp, binary parsing, network-dns
by Donn Cave 15 Feb '08

15 Feb '08

On Feb 14, 2008, at 4:44 PM, Adam Langley wrote: > HsOpenSSL now has rudimentary support for writing SSL servers[5] > (clients coming soon). In terms of blocking IO, this /should/ work the > way you would hope (i.e. like a Haskell function w.r.t. forkIO). Coincidentally, night before last I downloaded the openssl source and started trying to think about an SSL library. The thing is, I have always wished for an SSL library that doesn't do I/O, but just transforms data and leaves the I/O to you. I guess that's going to be a good deal more complicated, and in many cases not worth it at all - so there would need to be an SSLIO layer above it - but clinging to some vague reactive-object ideals I imagine that this `pure' SSL core could fit into some kinds of dispatching frameworks where the usual thing would be awkward. Anyway, I'll write again in a few years if I get around to doing anything about it. Donn Cave, donn(a)avvanta.com

1 0

a general question on Arrows
by Steve Lihn 15 Feb '08

15 Feb '08

In John Hughes' paper [1], Programming with Arrows, p. 20, "The truly interesting arrow types are those which do not correspond to a monad, because it is here that arrows give us real extra generality. Since we know that stream functions cannot be represented as a monad, then they are one of these "interesting" arrow types. So are the arrows used for functional reactive programming, for building GUIs, and the arrows for discrete event simulation we present in Section 5. And since these arrows cannot be represented by a monad, we know that they cannot support a sensible definition of app either." He described a few things that "cannot" be represented as a monad, they are: 1. Stream 2. FRP 3. GUI (request/response?) 4. Event Driven System (like circuits, robots?) My first question is: Are they "absolutely" outside of the realm of function + monad, therefore, arrows are indispensable? Or it is simply because the haskell program would be very cumbersome without arrows in these areas? (I mean without utilizing FFI to rescue.) The second question is: Other than the 4 areas above, are there more? Just want to get a sense of how useful arrows are. Not really a theoretical question. Thanks, Steve [1] http://www.cs.chalmers.se/~rjmh/afp-arrows.pdf

2 3