February 2007 - Haskell-Cafe

Safe lists with GADT's
by oleg＠pobox.com 27 Feb '07

27 Feb '07

Stefan O'Rear wrote: > Personally I like the GADT approach best since it is very flexible and > convienient. I have never used a purpose-build computer proof system, > but (modulo _|_) it took me less than 10 minutes to answer > LoganCapaldo (on #haskell)'s challenge to proof that + was commutative > ( http://hpaste.org/522 ) I'm afraid it may be premature to call this a proof. Here's your code > data S x > data Z > > data Add :: * -> * -> * -> * where > AddZZ :: Add Z Z Z > AddS1 :: !(Add x y z) -> Add (S x) y (S z) > AddS2 :: !(Add x y z) -> Add x (S y) (S z) > > add_is_commutatative :: Add a b c -> Add b a c > add_is_commutatative (AddZZ) = AddZZ > add_is_commutatative (AddS1 a) = AddS2 (add_is_commutatative a) > add_is_commutatative (AddS2 a) = AddS1 (add_is_commutatative a) First of all, where is the coverage proof? Given two numbers, S (S Z) and S Z, how to find their sum using the above code? Someone needs to construct the sequence of Adds, _at run-time_! But where is the proof that the sequence of Add applications expresses all possible ways of computing the sum, and each possible sum can be represented as a sequence of Adds? One may say -- this is so trivial; to which I reply that the original question was trivial as well. If we talk about the formal _proof_, then let's do it rigorously and formally all the way. Also, we can write > main = let x = AddS1 (undefined::Add Z Z (S Z)) in print "OK" > main2 = let x = add_is_commutatative (undefined::Add Z Z (S Z)) in print "OK" and the evaluation of 'main' and main2 prints OK. Thus we need to do forcing _all_ the way. But what if we forget some forcing? Incidentally, this is exactly what happened: add_is_commutatative should have been strict. But the code above misses the strictness annotation and still it compiles and seems to work -- and gives one a reason to call it a proof despite the deficiency. I'm afraid I have little trust in the system that permits such lapses. > but (modulo _|_) That is quite an unsatisfactory disclaimer! From the CH point of view, Haskell is inconsistent as every type is populated. Showing that a function is total is precisely demonstrating that the function is the proof of its type. So, showing the absence of bottoms is precisely making the proof! The problem with GADTs and other run-time based evidence is just that: _run-time_ based evidence and pattern-matching. In a non-strict system, checking that the evidence is really present is the problem on and of itself. BTW, Omega, Dependent ML and a few other systems with GADTs are strict.

3 2

problems installing ghc 6.6 with extralibs (bad interface file)
by Thomas Hartman 27 Feb '07

27 Feb '07

I installed ghc 6.6 from source ok. But then when I tried installing it with the "extralibs" to get all the functionality that had been unbundled in 6.6, I hit a glitch. Anyone ever seen anything like this? In case it matters, this is ssh-ed in to a virtualized user mode linux session. ***************************************** thartman@linodewhyou:~/haskellInstalls$ cat install-ghc-6.6.sh if [ ! -f ghc-6.6-src.tar.bz2 ]; then wget http://www.haskell.org/ghc/dist/6.6/ghc-6.6-src.tar.bz2 fi if [ ! -f ghc-6.6-src-extralibs.tar.bz2 ]; then wget http://www.haskell.org/ghc/dist/6.6/ghc-6.6-src-extralibs.tar.bz2 fi tar -tvjf ghc-6.6-src.tar.bz2 tar -tvjf ghc-6.6-src-extralibs.tar.bz2 pushd ghc-6.6 ./configure make make install popd thartman@linodewhyou:~/haskellInstalls$ sudo ./install-ghc-6.6.sh 2>&1 | tee out.txt thartman@linodewhyou:~/haskellInstalls$ tail -n20 out.txt ------------------------------------------------------------------------ make[2]: Nothing to be done for `install'. ------------------------------------------------------------------------ == make install - --no-print-directory -r; in /home/thartman/haskellInstalls/ghc-6.6/utils/ghc-pkg ------------------------------------------------------------------------ Creating a symbolic link from ghc-pkg-6.6 to ghc-pkg in /usr/local/bin for i in ghc-pkg-6.6; do \ /usr/bin/install -c -m 755 $i /usr/local/bin; \ done /usr/local/bin/ghc -H16m -O -cpp -Wall -fno-warn-name-shadowing -fno-warn-unused-matches -i../../compat -ignore-package Cabal -Rghc-timing -c Main.hs -o Main.o -ohi Main.hi Main.hs:19:0: Bad interface file: ../../compat/Distribution/InstalledPackageInfo.hi mismatched interface file versions: expected 6060, found 6 <<ghc: 24591324 bytes, 4 GCs, 106128/106128 avg/max bytes residency (1 samples), 16M in use, 0.00 INIT (0.02 elapsed), 0.25 MUT (0.42 elapsed), 0.10 GC (0.12 elapsed) :ghc>> make[2]: *** [Main.o] Error 1 make[1]: *** [install] Error 1 make: *** [install] Error 1 ~/haskellInstalls thartman@linodewhyou:~/haskellInstalls$

2 1

Re: Re: [Haskell-cafe] Build failed - hidden package ?
by Dunric 27 Feb '07

27 Feb '07

Yes, that did the trick. Thank You. >-----Puvodni zprava----- >Od: J. Garrett Morris [mailto:trevion@gmail.com] >Komu: Dunric <dunric29a(a)atlas.cz> >Předmět: Re: [Haskell-cafe] Build failed - hidden package ? > > >Hello, > >Are you building with Cabal? In case you are, Cabal hides all >packages by default and only shows those which are mentioned in your >cabal file. To fix this, you can add 'base' to the build-depends: >list. > >If you're not using Cabal, I don't have a clue. (-; > >Good luck! > >/g > >On 2/26/07, Dunric <dunric29a(a)atlas.cz> wrote: >> Hi. >> I've got stuck with the following compilation error I probably can't fully understand: >> >> ---------------------------------------------------------------------- >> Building library... >> ... >> Using package config file: /usr/local/lib/ghc-6.6/package.conf >> wired-in package base mapped to base-2.0 >> wired-in package rts mapped to rts-1.0 >> wired-in package haskell98 mapped to haskell98-1.0 >> wired-in package template-haskell mapped to template-haskell-2.0 >> Hsc static flags: -static >> ... >> Graphics/UI/SDL/Rotozoomer.hs:15:7: >> Could not find module `Foreign.C': >> it is a member of package base, which is hidden >> >> ---------------------------------------------------------------------- >> >> What does such error mean ? >> >> Modules Foreign and Foreign.C are installed and available from the default path. >> Lines 12-15 of Rotozoomer.hs: >> ------------------------------------------ >> module Graphics.UI.SDL.Rotozoomer where >> >> import Foreign >> import Foreign.C >> ------------------------------------------ >> >> Any idea what's wrong, resp. some explanation why compilation fails ? >> >> Thanks in an advance. >> >> ------------------------------------------ >> >> www.icqsms.cz >> >> _______________________________________________ >> Haskell-Cafe mailing list >> Haskell-Cafe(a)haskell.org >> http://www.haskell.org/mailman/listinfo/haskell-cafe >> > > >-- >It is myself I have never met, whose face is pasted on the underside of my mind. ------------------------------------------ www.icqsms.cz

1 0

rebinding >>= for restricted monads
by David Roundy 27 Feb '07

27 Feb '07

Hello fellow haskellers, I am wondering if anyone has an idea whether I'd run into trouble if I rebound >>= in order to provide a more restricted monad. My idea is to define a class: class WitnessMonad wm where (>>=) :: wm w w' a -> (a -> wm w' w'' b) -> wm w w'' b (>>) :: wm w w' a -> wm w' w'' b -> wm w w'' b return :: a -> wm w w' a fail :: String -> wm w w' a which obviously just adds a couple of phantom types indicating the monad state prior to and after each operation. I actually rather like this redefined monad, as it seems like it'd be useful in lots of places (e.g. a restricted IO monad that disallows use of a file handle after it's closed). It seems to me like this would be a pretty cool kind of monad. It'd allow us to encode typechecked "properties" in a monad, and there'd be very little restriction on how tricky those properties could be. And we'd get this all using the same do syntax we all love (and the new properties are by definition sequential, so a monad is precisely what we want, only at the type level). One trouble I see is how to move an ordinary monad into the WitnessMonad class. Of course, they differ in kind, so we need to do something, but I'm not sure what, and suspect that folks with experience using monad transformers will immediately see the answer. Of course, I want to be able to use both my fancy witnessed monad and IO in the same module, and I want to be able to use do notation for both of them. I suppose we could easily define data M m w w' c = M (m c) lift = M lower (M m) = m instance WitnessMonad (M m) where f >>= g = lift $ Prelude.(>>=) (lower f) (lower . g) ... but then we'd have to lift all our operations, so an ordinary IO function in a module that used my fancy rebound do notation would look like f :: IO Char f = lower $ do lift $ putStr "Hello world" lift $ getChar which seems rather heavy. Can anyone think of syntax-light way to allow my hypothesized rebound do-notation to also work with ordinary monads? -- David Roundy Department of Physics Oregon State University

10 17

FFI basics
by Yitzchak Gale 27 Feb '07

27 Feb '07

Hi, I would like to use FFI for the first time. Can someone give me a really, really simple complete example? I want to be able to take a simple C program and access a function from it in Haskell. A simple example of the other way around would be nice, too, but I don't happen to need that just now. I started reading the Addendum, but that looks like it would be a lot easier to read if I saw a simple complete example first. Everything I found on the wiki seems way beyond that - maybe I missed it. I am using GHC. I am not using Windows. Thanks, Yitz

10 16

Splitting Hairs Over Terminology
by P. R. Stanley 26 Feb '07

26 Feb '07

Hi folks in C and C++ world the humble comma is an operator. Is this also the case in Haskell or, is it classed as a function? In the wikibook they talk about consing new elements onto a list. Does this cons stand for anything meaningful in the English language? For example, is it short for construction or something similar? I'm assuming that the ":" function takes two arguments and returns a newly constructed list which is assigned to the variable holding/pointing to the old list. Cheers Paul

4 6

OO Design in Haskell Example (Draft)
by oleg＠pobox.com 26 Feb '07

26 Feb '07

Steve Downey wrote: > In the last OO design in Haskell thread (and probably in every one > preceeding it), it was suggested that having some examples might be a good > idea. > > Since most people with existing designs will have some familiarity with > Design Patterns, and those are typical building blocks for OO designs, it > occured to me that implementing some of them might be a useful > excersize. Have you looked at OOHaskell? http://homepages.cwi.nl/~ralf/OOHaskell/ http://darcs.haskell.org/OOHaskell/ With the exception of pure-functional objects and binary methods, I think we have considered almost every OO pattern/idiom we could find, including nominal/structural subtyping, co- and contra-variance, self-typing, etc. The DARCS repository contains the complete code for all of the examples and patterns. To clarify, the point of OOHaskell is to use Haskell as a tool, laboratory bench, for exploring various (thorny) OO issues.

2 1

Trouble with record syntax and classes
by Thomas Nelson 26 Feb '07

26 Feb '07

I'm brand new to haskell and I'm having trouble using classes. The basic idea is I want two classes, Sine and MetaSine, that are both instances of ISine. This way I can use the act method and recurse through the metasines and sines. Here's my code: module Main where class ISine a where period :: a -> Integer offset :: a -> Integer threshold :: a -> Integer act :: (ISine b) => Integer -> a -> b on :: Integer -> a -> Bool --on needs offset, period, threshold on time self = (mod (time-(offset self)) (period self)) < (threshold self) data Sine = Sine { period :: Integer, offset :: Integer, threshold :: Integer, letter :: String } instance Sine ISine where act time (Sine self) |on time self = [letter self] |otherwise = [] data MetaSine = MetaSine { period :: Integer, offset :: Integer, threshold :: Integer, sines :: (ISine a) => [a] } instance MetaSine ISine where act time (MetaSine self) |on time self = foldr (++) (map (act time) (sines self)) |otherwise = [] The errors I get involve multiple declarations of period, offset, and threshold. Any help would be greatly appreciated. -Thomas

6 6

Re: [Haskell-cafe] State of OOP in Haskell
by dons＠cse.unsw.edu.au 26 Feb '07

26 Feb '07

deliverable: > Well, I'm thinking in terms of OOD/OOA/OOP -- Design, Architecture, > Programming. That's about the only way to model a bog system. Say I > have a stock market model -- I'll have a database of tickers, a > simulator to backtest things, a trading strategy, etc. > > Do Haskell modules provide enough encapsulation to design a system in > terms of them? What are the design/architecture units in Haskell if > not OO-based? Haskell's pretty big on encapsulation (we like our strong statically checked guarantees after all) Some of the encapsulation mechanisms used in large (>5k loc up to 100k + Haskell programs I've hacked on): modules qualified modules type classes to specify generic interfaces existential types to hide implementations completely (and statically) existentials using typeclasses to package the interface monads for state/effect encapsulation abstract data types data types with smart constructors first class modules via existentials purity laziness So the same kind of encapsulation as OO stuff provides (existentials are essentially OO objects), and a few more besides. Monads in particular are perfect for encapsulating interesting effects, and having that encapsulation statically enforced. Probably some of the OO refugees can think of other mechanisms. Cheers, Don

4 4

Safe lists with GADT's
by Neil Mitchell 26 Feb '07

26 Feb '07

Hi I'm starting to play with GADT's, and I was trying to write a safe version of head and tail, on a safe version of lists. What I came up with is: > data ConsT a > data NilT > > data List a t where > Cons :: a -> List a b -> List a (ConsT b) > Nil :: List a NilT > > instance Show a => Show (List a t) where > show (Cons a b) = show a ++ ":" ++ show b > show Nil = "[]" > > safeHead :: List a (ConsT t) -> a > safeHead (Cons a b) = a > > safeTail :: List a (ConsT t) -> List a t > safeTail (Cons a b) = b > > safeMap :: (a -> b) -> List a t -> List b t > safeMap f Nil = Nil > safeMap f (Cons a b) = Cons (f a) (safeMap f b) Defining safeMap was trivial, but one thing I couldn't figure out was how to write something like fromList: fromList [] = Nil fromList (a:as) = Cons a (fromList as) fromList could obviously be anything such as reading from a file etc, where the input is not known in advance. Are there any techniques for this? In addition I was expecting to find some example like this in one of the papers/examples on GADT's, but I didn't. The Haskell wikibook has a slight example along these lines, but not with the recursive field in ConsT. [http://en.wikibooks.org/wiki/Haskell/GADT] Any help or hints would be appreciated, Thanks Neil

7 11