- Haskell - Haskell.org

Fundep & Datatype Request
by Ashley Yakeley 05 Sep '03

05 Sep '03

OK, this is an issue I have raised before I think, but I don't remember what the opinion on it was. The following doesn't compile with ghc -fglasgow-exts (or Hugs -98): -- ghc -fglasgow-exts -c TypeLambda.hs module TypeLambda where { class Fc a b | a -> b; instance Fc Bool Int; data F1 a = forall b. (Fc a b) => MkF1 b; makeF1 :: Int -> F1 Bool; makeF1 = MkF1; getF1 :: F1 Bool -> Int; getF1 (MkF1 i) = i; data F2 a = MkF2 (forall b. (Fc a b) => b); makeF2 :: Int -> F2 Bool; makeF2 i = MkF2 i; getF2 :: F2 Bool -> Int; getF2 (MkF2 i) = i; } Clearly makeF1 and getF2 are OK. But I claim getF1 and makeF2 should compile, since the type inside either an "F1 Bool" or an "F2 Bool" must always be an Int. Instead I get this: TypeLambda.hs:14: Inferred type is less polymorphic than expected Quantified type variable `b' is unified with `Int' When checking an existential match that binds i :: b and whose type is F1 Bool -> Int In the definition of `getF1': getF1 (MkF1 i) = i TypeLambda.hs:19: Cannot unify the type-signature variable `b' with the type `Int' Expected type: b Inferred type: Int In the first argument of `MkF2', namely `i' In the definition of `makeF2': makeF2 i = MkF2 i So why is this useful? Because you can do some form of type-lambda with it. For instance, you might have some system of collection types: Word8 -->> UArray Int Word8 Word16 -->> UArray Int Word16 (a -> b) -->> Array Int (a -> b) It would be nice to hide the implementation and just expose some type-constructor: MyCollection Word8 MyCollection Word16 MyCollection (a -> b) I believe this can't be done currently. -- Ashley Yakeley, Seattle WA

1 0

need some info/help
by Pratik Bhadra 04 Sep '03

04 Sep '03

Hi I know there is a general consensus about finding out new things to use with Haskell but I am quite a newcomer in this field and am attempting to write a compiler and a runtime system in Haskell. At this important juncture I would like to ask for some help with some resources, books or links which I can look up which would help me understand the process better. Your help is highly appreciated. Thanks :)

3 2

Re: proving the monad laws
by oleg＠pobox.com 04 Sep '03

04 Sep '03

Steffen Mazanek posed a problem: given the monad: > data Error a = Error String | Ok a > data TI a = TI (Subst -> Int -> Error (Subst, Int, a)) > instance Monad TI where > return x = TI (\s n -> Ok (s,n,x)) > TI f >>= g = TI (\s n -> case f s n of > Ok (s',m,x) -> let TI gx = g x in > gx s' m > Error s->Error s) > fail s = TI (\_ _->Error s) prove the associativity of bind: > m@(TI mf) >>= (\a->f a >>= h) = > = TI (\s n -> case mf s n of > Ok (s',m,x) -> let TI gx = (\a->f a >>= h) x in > gx s' m > Error s->Error s) = ... > = ((TI mf) >>= f) >>= h > I was wondering, if it is possible to simplify: "let TI gx = f x >>=h in > ...". > But the "a" may occur in "h"? No, it may not. First of all, the third monadic law specifically disclaims such an occurrence. Indeed, if 'a' had occurred free in 'h', then ((TI mf) >>= f) >>= h would make no sense. Although (>>=) notation is better for practical programming, I believe Filinski's notation is superior for manipulation. Filinski defines a postfix operator "raised star", which is denoted 'st' below: st:: (Monad m) => (a -> m b) -> m a -> m b st f m = m >>= f Indeed, st = flip (>>=) In Filinski's notation, the third monadic law has an especially appealing form: st ((st f) . g) = (st f) . (st g) Let us also define arun (TI f) s n = f s n We can then write for our monad: st f = \m -> TI $ \s n -> case arun m s n of Ok (s',m',x') -> arun (f x') s' m' Error s' -> Error s' Let _m, _s and _n denote "fresh" values of the right type (so we can later appeal to the universal generalization rule (closely related to eta-reduction) Phase 1: arun ((st ((st f) . g)) _m) _s _n => case arun _m _s _n of Ok (s',m',x') -> arun ((st f) $ g x') s' m' -- x' is not free in f, g Error s' -> Error s' => case arun _m _s _n of Ok (s',m',x') -> case arun (g x') s' m' of Ok (s'',m'',x'') -> arun (f x'') s'' m'' Error s'' -> Error s'' Error s' -> Error s' Phase 2: arun (((st f) . (st g)) _m) _s _n => arun (((st f) $ (st g) _m) _s _n => case arun ((st g) _m) _s _n of Ok (s'',m'',x'') -> arun (f x'') s'' m'' -- x'' is not free in f, g Error s'' -> Error s'' => case (case arun _m _s _n of Ok (s',m',x') -> arun (g x') s' m' -- x' is not free in f, g Error s' -> Error s') of Ok (s'',m'',x'') -> arun (f x'') s'' m'' -- x'' is not free in f, g Error s'' -> Error s'' => {see note below} case arun _m _s _n of Ok (s',m',x') -> case arun (g x') s' m' of Ok (s'',m'',x'') -> arun (f x'') s'' m'' Error s'' -> Error s'' Error s' -> Error s' Now, the results of Phase 1 and Phase 2 are identical. Given that _m, _s and _n were unique, fresh variables, by appealing to the universal generalization rule and the Church-Rosser property of our reductions, we conclude that st ((st f) . g) = (st f) . (st g) The critical step is the associativity of case: case (case x of C1 -> O1; C2 -> O2) of C1' -> O1'; C2' -> O2' ==> case x of C1 -> case O1 of C1' -> O1'; C2' -> O2' C2 -> case O2 of C1' -> O1'; C2' -> O2' provided that variables bound in C1 and C2 do not occur in C1', O1', C2', O2'

2 1

Haskell for non-Haskell sake
by Gordon James Miller 03 Sep '03

03 Sep '03

I'm currently examining using Haskell for doing numerical modelling of middle atmospheric photochemistry for my PhD work. I've long been troubled by the disconnect between the mathematical formulation of physical laws as found in textbooks and the imperative formulation of them in C/Fortran/Java. I absolutely love the expressiveness of Haskell with respect to writing mathematical software and so I'm pursuing this with some vigor and hope to have a series of web reports to present my successes and failures with this. Gordon James Miller Promisemark, Inc. Senior Computer Scientist gmiller(a)promisemark.com (571)330-9012 Everyone has a place, some just need to be put there.

2 1

New address
by jan.skibinski＠SAFe-mail.net 02 Sep '03

02 Sep '03

I apologize to anyone who wrote me last week and did not get any response. For a reason unknown to me I can no longer access the email account which I used when subscribing to this list. I hope this address will remain stable enough. Jan

1 0

RE: Type class problem
by Simon Peyton-Jones 02 Sep '03

02 Sep '03

| > b) at the moment dictionaries have the property that you can always | > evaluate them using call-by-value; if they could be recursively | > defined (as you suggest) that would no longer be the case | > | > Mind you, GHC doesn't currently take advantage of (b), so maybe it | > should be ignored. Adding the current goal as an axiom would not be | > difficult, but I don't have time to do it today! Is anyone else | > interested in such a feature? | | I would like to try making this change, but I couldn't puzzle out enough | of the type class system the last time I looked. I would appreciate | advice, references, or even just a list of the relevant modules. If you want to try fiddling with GHC, try the -fdicts-strict flag, and look for where it is used in the source (opt_DictsStrict). The predicate Type.isStrictPred is also relevant. | Allowing implications in contexts even allows us to derive instances for | some irregular types: | | data Twice f x = T (f (f x)) | data Growing f = G (f (Growing (Twice f))) | data Id x = Id x | | Suppose we want to define instances that will imply Show (Growing Id). | Growing Id is an irregular type so allowing irregular derivations isn't | enough, but the following instances are acceptable | | instance (forall a.Show a => Show f a,Show x) => Show (Twice f x) where | show (T ffx) = show "T "++show ffx Indeed so. That's exactly what the "Deriving type classes" paper points out, and Valery's Haskell Workshp 2003 paper "Simulating quantified class constraints" is also highly relevant. Simon

1 0

RE: Type class problem
by Simon Peyton-Jones 02 Sep '03

02 Sep '03

| I'm wondering if the general method of avoiding non-termination can be | made to work in these more complex cases. | | Incidentally, the constraint solver stack overflow problem can be | turned to our advantage. The typechecker's exhausting the stack should | be considered a failure to match the instance -- and so the | typechecker should mark the current instance inappropriate and try | another one, if any. Ultimately, this boils down to solving the halting problem, I believe. Stack-overflow isn't a proof that the thing isn't soluble. I can believe that it woks nicely in practice, but it's a bit of a hack! Simon

1 0

RE: Haskell for non-Haskell's sake
by Simon Peyton-Jones 02 Sep '03

02 Sep '03

| Since the opening of this thread by Hal Daume 11 (binary), we see a constant | flow of interesting contributions/confessions. Plenty of applications, it | seems that Haskell is really used in a wider context than we might think. | It is a pleasure to read all this. Yes, it is indeed! As Jerzy remarks, it is quite hard to get application papers published in conferences. I know from personal experience that it's hard even when the program committee is strongly motivated to take application papers. Why? One reason is that application papers seldom have a new research result to report -- their strength is in the integration of language with application. Another is that application papers are hard to write; they can easily degenerate into a "we did this and then we did that" ramble. It is genuinely difficult to abstract the re-usable lessons from an application experience. Mindful of this, the Journal of Functional Programming *explicitly welcomes* application-oriented papers (we call them "practice and experience" papers). We have tried to articulate the criteria we use when evaluating them: http://www.dcs.gla.ac.uk/jfp/editorialMay98.html So let me encourage those who have responded to Hal's call to consider submitting a paper to JFP. It really is helpful to the FP community to learn hard-won lessons from others. Let's hear them! (The Haskell Community Newsletter is an excellent complementary forum. It's ideal for a short "here's what we did" mutual-information contribution. Claus has done a fantastic job with the newsletter.) Simon

1 0

proving the monad laws
by Steffen Mazanek 01 Sep '03

01 Sep '03

Hello, consider the following monad (which is a slight adaptation of the one used in "Typing Haskell in Haskell") as given: data Error a = Error String | Ok a data TI a = TI (Subst -> Int -> Error (Subst, Int, a)) instance Monad TI where return x = TI (\s n -> Ok (s,n,x)) TI f >>= g = TI (\s n -> case f s n of Ok (s',m,x) -> let TI gx = g x in gx s' m Error s->Error s) fail s = TI (\_ _->Error s) Now I would like to verify the monad laws. It is really easy to show that return is both a left- and a right-unit. But I got stuck with associativity: m@(TI mf) >>= (\a->f a >>= h) = = TI (\s n -> case mf s n of Ok (s',m,x) -> let TI gx = (\a->f a >>= h) x in gx s' m Error s->Error s) = ... = ((TI mf) >>= f) >>= h Is there someone outside who is willing to tell what fills the gap? A hint may be sufficient already. Or is there a tool, which finds such derivations? I have read the tutorial "All about Monads", but there only is mentioned, that there is an obligation for the programmer to prove these laws. It would be helpful as well, to provide an example! I was wondering, if it is possible to simplify: "let TI gx = f x >>=h in ...". But the "a" may occur in "h"? Thank you. Steffen

2 1

RE: Haskell for non-Haskell's sake
by Tim Docker 01 Sep '03

01 Sep '03

Jerzy Karczmarczuk wrote: > Presumably this reviewer has his particular visions what a science is, > but I don't believe that such people dominate in the milieu of FPL. > I believe that it would be interesting to organize some workshops > on "practical" applications of functional programming...) Actually, I would be more likely to attend a workshop focusing on real world applications of functional programming than one on more theoretical advances (as interesting as they are). Tim

2 1