- Haskell-Cafe - Haskell.org

Higher kinds (and impredicativity?)
by Jim Apple 16 Jan '07

16 Jan '07

Why is this declaration ill-formed: data Bad t where Bad :: Bad (forall (f :: * -> *) . f) GHC 6.6 says: `f' is not applied to enough type arguments Expected kind `*', but `f' has kind `* -> *' In the type `forall f :: (* -> *). f' In the type `Bad (forall f :: (* -> *). f)' In the data type declaration for `Bad' I suppose this is because the kind inference rule is C, x : k1 |- y : * ----------------------- C |- (\forall x : k1 . y) : * I'd expect C, x : k1 |- y : k2 ----------------------- C |- (\forall x : k1 . y) : k2 Is there a foundational or an implementation reason for this restriction? Jim

2 4

Newbie: Project: Missionary and Cannibal in Haskell
by thapaps＠gmail.com 16 Jan '07

16 Jan '07

I am very new to haskell. my project is to solve Missionary and Cannibal this is what I have been given : 1. 3 Missionary and 3 Cannibal . 2. 1 boat. 3. Max passengers=2. 4. RULE: at any given time number of cannibal cannot exceed number of missionary 5. I need to move all the missionary and cannibal from one bank to the other. I am really confused as to how to proceed to solving this problem. based on 2 passenger I can come of with five different boat loads. this would lead to five different combination at each state. how would i preserve the previous state value and pass it to the next state, What would be the best way to tackle this problem? any direction any help in this will be highly appreciated.

2 1

Redefining superclass default methods in a subclass
by Brian Hulley 15 Jan '07

15 Jan '07

Hi, Looking at some of the ideas in http://www.haskell.org/haskellwiki/The_Other_Prelude , it struck me that the class system at the moment suffers from the problem that as hierarchies get deeper, the programmer is burdened more and more by the need to cut-and-paste method definitions between instances because Haskell doesn't allow a superclass (or ancestor class) method default to be redefined in a subclass. For example, consider this part of a proposal for Functor => Applicative => Monad: -- I've just used 'm' so it's easy to see what parts are relevant to Monad class Functor m where fmap :: (a -> b) -> m a -> m b class Functor m => Applicative m where return :: a -> m a (<*>) :: m (a -> b) -> m a -> m b (>>) :: m a -> m b -> m b ma >> mb = -- left as exercise for a rainy day! class Applicative m => Monad m where (>>=) :: m a -> (a -> m b) -> m b The problem with this is that whereas someone defining a Monad at the moment only needs to define (return) and (>>=), with the above, though it gives obvious advantages in flexibility, generality etc, defining a new Monad involves providing methods (in instance decls) for fmap and (<*>) as well, and the default method for (>>) is ma >> mb = (fmap (const id) ma) <*> mb (from that page above) which I'm sure everyone will agree is a *lot* more complicated than: ma >> mb = ma >>= (\_ -> mb) Not only is the first definition for (>>) more complicated, it obscures the simple fact that for monads it's just a trivial special-use case of >>= where the bound argument is ignored. Therefore I'm wondering if it would be possible to allow default methods for a superclass to be defined, or redefined, in a subclass, so we could write: class Applicative m => Monad m where (>>=) :: m a -> (a -> m b) -> m b mf <*> ma = mf >>= \f -> ma >>= \a -> return (f a) ma >> mb = ma >>= \_ = -> mb fmap f ma = ma >>= \a -> return (f a) (I know the above can be written in a more point-free style but I wrote it like that to make it easy to understand what's happening.) The essential point here (excuse the pun :-) ) is that it is impossible to write the default methods in the class in which the operation is defined, because the implementation depends on methods of the relevant subclass (and will therefore be different for different subclasses though not for each particular instance of a given ancestor class of a particular subclass). As Haskell stands at the moment, we are forced to cut and paste identical methods for each individual instance of each ancestor class of a particular subclass because we can't override an ancestor class method in the *class* decl for a subclass. The type class system at present is based on the idea that you can define related methods together and in terms of each other, at one level of the hierarchy. However as the above example shows, related methods sometimes need to be spread over the hierarchy but we still want to be able to define default implementations of them in terms of each other. Perhaps there is some reason this can't be done? Brian. -- http://www.metamilk.com

6 10

Re: [Haskell-cafe] Higher kinds (and impredicativity?)
by Jim Apple 15 Jan '07

15 Jan '07

On 1/15/07, Doaitse Swierstra <doaitse(a)cs.uu.nl> wrote: > Values that live as elements in data have to be data themselves, and > thus have to be of a type that has kind *. But the example I give doesn't have a "value" of kind * -> * living in data. The constructor is nullary, only the parameter to the type is not of kind *. This is fine in declarations like: data Good (x :: * -> *) where Good :: Good Maybe What I'm asking is why, for declarations like data OK (x :: * -> *) where OK :: OK x type Fine = OK Maybe type Evil = OK (forall (f :: * -> *) . f) Fine is allowed, while Evil is not. This is not the case for data OK' (x :: *) where OK' :: OK' x type Fine' = OK' Maybe type Evil' = OK' (forall (f :: *) . f) When both Fine' and Evil' are accpeted. Jim > On Jan 15, 2007, at 3:39 AM, Jim Apple wrote: > > > Why is this declaration ill-formed: > > > > data Bad t where > > Bad :: Bad (forall (f :: * -> *) . f) > > > > GHC 6.6 says: > > > > `f' is not applied to enough type arguments > > Expected kind `*', but `f' has kind `* -> *' > > In the type `forall f :: (* -> *). f' > > In the type `Bad (forall f :: (* -> *). f)' > > In the data type declaration for `Bad' > > > > I suppose this is because the kind inference rule is > > > > C, x : k1 |- y : * > > ----------------------- > > C |- (\forall x : k1 . y) : * > > > > I'd expect > > > > C, x : k1 |- y : k2 > > ----------------------- > > C |- (\forall x : k1 . y) : k2 > > > > Is there a foundational or an implementation reason for this > > restriction? > > > > Jim

1 1

Pattern matching
by Stefan Aeschbacher 15 Jan '07

15 Jan '07

Hi I sometimes have a function definition similar to this: myFunction x@(Constructor1 _ _ _ _ _ _) = ... myFunction x@(Constructor2 _ _ _ _ _ _ _ _) = ... which in my eyes is not very elegant and easy to type. Is there an easier way to switch on the different constructors of a type (Data.Generics certainly could be used..)? If not, has thought been put in a pattern matching possibility of the form _*. This would allow: myFunction x@(Constructor1 _*) = ... myFunction x@(Constructor2 _*) = ... Also pattern matches of the form: myFunction2 (Constructor1 _* a _*) = ... could be possible as long as the pattern is non-ambiguous (in this case, only one variable with the type of a is present in this constructor). regards Stefan

3 3

Meaning abbreviations stat file GHC
by Ron 13 Jan '07

13 Jan '07

Dear, I made a profile[1] of a test program: Where can I find documentation for the meaning of everything mentioned below? Or alternatively, can anyone explain them? Where can I see the effect of using the -xt option in this profile? Ron [1] /Main +RTS -p -s -xt -hc 1,372,408,024 bytes allocated in the heap 121,255,600 bytes copied during GC (scavenged) 6,584,692 bytes copied during GC (not scavenged) 2,768,896 bytes maximum residency (68 sample(s)) 2649 collections in generation 0 ( 1.11s) 68 collections in generation 1 ( 0.49s) 6 Mb total memory in use INIT time 0.00s ( 0.00s elapsed) MUT time 5.97s ( 6.63s elapsed) GC time 1.60s ( 1.88s elapsed) RP time 0.00s ( 0.00s elapsed) PROF time 0.19s ( 0.20s elapsed) EXIT time 0.00s ( 0.00s elapsed) Total time 7.76s ( 8.71s elapsed) %GC time 20.6% (21.5% elapsed) Alloc rate 229,946,873 bytes per MUT second Productivity 76.9% of total user, 68.5% of total elapsed Ron

1 0

Are GADTs expressive? Simple proof-carrying code in Haskell98
by oleg＠pobox.com 13 Jan '07

13 Jan '07

Inspired by the recent post by Jim Apple, we demonstrate a datatype `Terminates' that can hold only an assuredly terminating (strongly normalizable) term in untyped lambda-calculus. Furthermore, the values of the datatype `Terminates' contain all and only those untyped lambda-calculus terms with that property. As in Jim Apple's solution, to create the value `Terminates', the user submits the term in question and the proof of its termination. The proof will be verified -- and if it holds, the Terminates certificate will be created. As in Jim Apple's solution, verification of the submitted proof has to be done at run-time, to make sure the proof is not fake, that is, has no undefined values. Our solution uses neither GADTs nor typeclasses; in fact, it is in Haskell98. Also, the required proof from the user couldn't be simpler. Jim Apple wrote: > To show how expressive GADTs are, the datatype Terminating can hold > any term in the untyped lambda calculus that terminates, and none that > don't. I don't think that an encoding of this is too surprising, but I > thought it might be a good demonstration of the power that GADTs > bring. The shown GADT encoding seems to be of the kind that is convertible to typeclasses in the straightforward way, see for example, http://pobox.com/~oleg/ftp/Haskell/GADT-interpreter.hs Inn this particular example, GADT do not bring any power. Incidentally, the typeclass encoding has an advantage: If the submitted proof is invalid, the error will be reported at compile time. There is not even a possibility of a run-time error. This is because the typeclasses approach does only type-level computations and does not look at values at all (which may as well be undefined). Placing a value into a (rank-1) datatype forces the typechecker to resolve any constraints associated with the value, or report an error if constraints are not satisfiable. However, it seems that the problem at hand admits a far simpler solution -- in Haskell98. The solution is in spirit of lightweight static capabilities. Here it is: > module PCC (Terminates, -- data constructor is not exported > make_terminates, get_term) where > > import YourFavorite.Lambda_calc > > data Terminates = Terminates{get_term::Term} > > make_terminates :: Term -> Integer -> Maybe Terminates > make_terminates term limit = > case reduce_term_nsteps term limit of > Left _ -> Nothing > Right normal_form -> Just (Terminates term) Because the data constructor is not exported, the only way to construct a value `Terminates' from which a term can be extracted is by invoking the function make_terminates. The function accepts a lambda-term, and a proof of its termination. The proof takes the form of the (upper bound of the) number of steps needed to normalize the term. The function make_terminates checks the proof, by trying to reduce the term that many steps. If the normal form is found in the process, the term is normalizable and we create the certificate. Otherwise, we conclude the termination proof does not hold and we return Nothing. This proof checking is clearly decidable. The module PCC constitutes the `trusted kernel' with respect to the Terminates datatype. The function make_terminates must be rigorously verified in order to deserve our trust. But the same should be said for the GADT or any other solution: e.g., one can easily add a new case alternative to the Normal datatype declaring Omega to be in the normal form.

3 2

mapTuple
by Marco Túlio Gontijo e Silva 13 Jan '07

13 Jan '07

Hello, is there a way to defined something as a map to use in tuples? I tried this: mapTuple f (a, b) = (f a, f b) But the type inferred to it is not as generic as I wanted: mapTuple :: (t -> t1) -> (t, t) -> (t1, t1) Then I tried a different, but not much, implementation: mapTuple' f g (a, b) = (f a, g b) mapTuple f = mapTuple' f f But the inferred type was the same. Is there a way to define a function in which I can be able to do something as this? mapTuple show ("string", True) -- malebria Marco Túlio Gontijo e Silva Correio (MSN): malebria(a)riseup.net Jabber (GTalk): malebria(a)jabber.org Telefone: 33346720 Celular: 98116720 Endereço: Rua Paula Cândido, 257/201 Gutierrez 30430-260 Belo Horizonte/MG Brasil

8 11

different performance of equivalent expression
by Alexander Vodomerov 13 Jan '07

13 Jan '07

Hello! I've run into strange effect that I can not explain. I have simple expression that can be written by two equivalent ways. However one way give much performance gain over another. Here is an example: -- apply function many times (tail-recursive) many n f x = if n == 0 then x else many (n-1) f $! (f x) -- first adder function adder1 = let r = many 5000000 sin 1.0 in \x -> x + r -- second adder function adder2 = \x -> x + many 5000000 sin 1.0 main = do putStrLn $ show $ adder1 1 putStrLn $ show $ adder1 2 putStrLn $ show $ adder1 3 putStrLn $ show $ adder1 4 putStrLn $ show $ adder2 1 putStrLn $ show $ adder2 2 putStrLn $ show $ adder2 3 putStrLn $ show $ adder2 4 If you run program it think some seconds performing math, and them prints 4 results immediately. But with adder2 function, it perform calculation in every call, which can be seen visually. It seems that compiler is able to "cache" in some way long computation in first case, but not in second. I always thought that let a = b in x + a is just a syntactic sugar for x + b. Is it wrong? Of course, this is just a toy example. In reality I was writing run-time compilation. Suppose, you have an simple arithmetic expression with variables. data Expr = Var String | Add Expr Expr | Mul Expr Expr | ... type Env = Map.Map String Double compile :: Expr -> (Env -> Double) compile e = case e of Var n -> \env -> env Map.! n Add e1 e2 -> \env -> (compile e1) env + (compile e2) env Mul e1 e2 -> \env -> (compile e1) env * (compile e2) env .... The same thing occur here. Expressions (compile e1) and (compile e2) are re-evaluated every time when compiled expression is run with some environment. So, it is much more an interpretation than compilation. I want that compile function returns expression that are pre-evaluated as much as possible to maximally speed up subsequent evaluation in different environments. How can I force (compile e1) to be evaluated eagerly in case line for Add/Mul? P.S. I'm using GHC 6.6 on Debian Linux (x86 arch). With best regards, Alexander.

3 4

STM and random numbers
by Chad Scherrer 13 Jan '07

13 Jan '07

Hi, I'd like to be able to use randomIO, but I'm working within the context of STM. Is there a way to get these working together happily? For now, I guess I could kludgingly use unsafePerformIO inside STM (it's the other way around that's not allowed, right?), but I would need to be sure it doesn't get inlined. Thanks, Chad

9 10