- Haskell-Cafe - Haskell.org

OT - lamba calculus definition - alpha reduction
by Dušan Kolář 29 May '06

29 May '06

Hello all, I'm asking in place of several my colleagues and myself of course. The question is almost off topic. It is from lambda calculus definition, in particular, definition of alpha reduction (and others as well). Alpha reduction definition: a lambda expression (\v.e) can be transformed (reduced) to (\v'.e[v'/v]) if the substitution e[v'/v] is valid. Beta reduction definition: a lambda expression (e1 e2) can be reduced to the expression e[e2/v] if e1 is of the form (\v.e) and if the substitution e[e2/v] is valid. Eta reduction definition: a lambda expression e can be reduced to a lambda expression (\v.e v) if v is not free in e. OK. If we have these two expressions: 1) (\x.x b x) 2) (\x.x c x) The question is, are they equal? (They are not identical, of course.) For answer "no", there is a strong argument - there is no reduction sequence that can make these identical. On the other hand, their "meaning" expresses the same operation. Well, what is the answer? I will be lucky with any link to WWW resource or your opinion. Nevertheless, the more formal and precise your answer will be the more I will be lucky. ;-) Thx and regards Dusan

4 5

(no subject)
by Christophe Poucet 29 May '06

29 May '06

Dear, I will try to explain what I'm trying to achieve, below you can find the code demonstrating where I'm at currently, and where I would like to ideally get, as well as the current compilation error. Basically I'm working on a minilanguage that I would like to simulate. This language is based on a core concept which can in the example below is "Foo". Now there is a 'primitive' instance of Foo that is the list. What I now want to do is make FooF an instance as well. FooF being a record based on a map that contains some other instances of Foo by name as well as code that will use this lookup table. For instance (this is not definite syntax): my pseudoproglanguage: A = [1..10] (aka refer to the 'primitive' instance of Foo) B = [1..10] (aka refer to the 'primitive' instance of Foo) bar C = if dum B then bar A else bar B dum C = dum A && dum B I realize I need existentials for this, but I'm afraid that my type-fu is lacking in this area. Perhaps one of you could point me in the right direction. With regards, Christophe ------------------------------------------------------------------------------------------------------------ {-# OPTIONS_GHC -fglasgow-exts #-} module FooBar where import qualified Data.Map as M class Foo f b | f -> b where foo :: f a -> b bar :: f a -> b -> b dum :: f a -> b -> Bool instance Foo [] Int where foo c = 0 bar c i = i+1 dum c i = (length c == i) data F b a = forall f. Foo f b => F (f a) instance Foo (F b) b where foo (F c) = F . foo $ c bar (F c) i = bar c i dum (F c) i = dum c i data FooF b a = FooF { cols :: M.Map String (F b a), barC :: M.Map String (F b a) -> b -> b, dumC :: M.Map String (F b a) -> b -> Bool } instance Foo (FooF b) b where foo c = fmap (foo) c bar c i = barC c (cols c) i dum c i = dumC c (cols c) i makeFooF cols barC dumC = FooF {cols = cols, barC = barC, dumC = dumC} -- Example: -- makeFooF -- [("A", [1..10]), ("B", [1..8])] -- (\t -> if dum (M.lookup "A" t) -- then bar (M.lookup "B" t) -- else bar (M.lookup "A" t) -- (\t -> dum (M.lookup "A" t) && dum (M.lookup "B" t) -- Ideally this system would also allow to make some FooF that is based on another FooF, hence the reason for existentials -- FooBar.hs:19:16: -- Couldn't match the rigid variable `b' against `F b1 a' -- `b' is bound by the instance declaration at FooBar.hs:18:0 -- Expected type: b -- Inferred type: F b1 a -- In the expression: (F . foo) $ c -- In the definition of `foo': foo (F c) = (F . foo) $ c -- -- FooBar.hs:31:12: -- Couldn't match the rigid variable `b' against `f b1' -- `b' is bound by the instance declaration at FooBar.hs:30:0 -- Expected type: b -- Inferred type: f b1 -- In the application `fmap (foo) c' -- In the definition of `foo': foo c = fmap (foo) c -- Failed, modules loaded: none. -- ----------------------------------------- -- Christophe Poucet Ph.D. Student Phone:+32 16 28 87 20 E-mail: Christophe (dot) Poucet (at) imec (dot) be Website: http://notvincenz.com/ IMEC vzw – Register of Legal Entities Leuven VAT BE 0425.260.668 – Kapeldreef 75, B-3001 Leuven, Belgium – www.imec.be *****DISCLAIMER***** This e-mail and/or its attachments may contain confidential information. It is intended solely for the intended addressee(s). Any use of the information contained herein by other persons is prohibited. IMEC vzw does not accept any liability for the contents of this e-mail and/or its attachments. **********

1 0

Re: [Haskell] (.) . (.)
by Brian Hulley 28 May '06

28 May '06

[moved to cafe] Robert Dockins wrote: > On Sunday 28 May 2006 05:02 pm, Brian Hulley wrote: >> I see my error was that I was reversing the args in eta expansion, >> so the correct derivation is: > > FYI, eta-expansions isn't valid in Haskell. Its safe in this > derivation, but it isn't always. Am I right in thinking that this is because of _|_ ? In any case I suppose I should have instead just replaced the function with it's definition like you (view Lambda Shell) and Christophe did. Also, is your Lambda Shell publicly available? (I had a quick look on the wiki in the Theorem provers section but couldn't find a link.) Thanks, Brian.

2 2

Re: [Haskell-cafe] Linking to third party libraries in windows
by Matthew Bromberg 28 May '06

28 May '06

That's an interesting statement that bears further scrutiny. I've been viewing monads as a kind of encapsulation in a quasi-hidden world state. Yes a monad is a function that would give you an output if you had access to the input world. That is the picture drawn in Simon Peyton Jones' tutorial. I've been thinking of actions in terms of the functions x -> IO(a), but Simon calls these IO actions and calls monads actions as you do. Is it your claim that whenever an 'IO action' is performed on something like IO (x) with x <- newListArray a l that the newListArray function will be called ? So with the old paradigm, where Rmatrix was stored as (Int, Int, IO(StorableArry Int CDouble)). A typical matrix operation, that calls out to a BLAS C routine cside_effect() looks something like this under the old scheme matfunc A = (u,v, arr) where u = f1 (getrows A) (getcols B) v = f2 (getrows A) (getcols B) arr = do arrA <- getarr A withStorableArray arrA (\vara -> cside_effect vara ) return arrA Now when one uses this code do A <- getAfromSomewhere fA = matfunc A B <- anotherfunc A fA has been changed by the cside_effect function, but A has not! Is it your contention that the array in A is essentially copied or created anew for every getarr A call? I think getarr A looked something like getarr (Rmatrix (r,c,arr)) = arr in the old technique, but now looks like getarr (Rmatrix (r,c,arr)) = return arr Is this perhaps an effect of lazy evaluation? When does one actually need to evaluate the constructor for the storable array contained in A? Hmmm. Is it that the rules specify that an IO action forces the evaluation of the value in the monad, but otherwise this value may be unevaluated? So return x doesn't evaluate x but (return x) >>= \z -> IOfunc z does? This would actually make sense in the end. The IO action of A <- getAfromSomewhere would not evaluate the monad that is the third element of the tuple A, since there is no real 'need' to do so. So in fact no constructor of A's array would ever get evaluated until a function was applied to it, which would have to be in the form of an IO action. That's a nice mind twister. Clean's uniqueness types are a little easier to grasp I think. Ahh I think I understand now. It has to work that way or else you cannot guarantee the sequential execution property of monads. Thus if y :: IO (a) and you evaluate z <- func (f1 y) (f2 y), the evaluation order of y is controlled by what is implemented in func (and f1 and f2), not by evaluation rules for arguments. The value wrapped in y MUST remain unevaluated until IO 'actions' are performed on it. Brian Hulley wrote: this is not correct. IO (StorableArray Int CDouble) is a monadic *value* itself, which represents an *action* which returns a storable array, and since you are filling in the slot in Rmatrix with the action (newListArray a l), this monadic value represents the action of creating a new array whenever the action is executed.

3 4

Re: [Haskell] (.) . (.)
by Brian Hulley 28 May '06

28 May '06

[Moved to cafe] Christophe Poucet wrote: > Hello, > > I think you look at the (.) . (.) as all being c's in the wrong way. > You have to consider what will evaluate first (syntactical priority > rules). (.) . (.) === (.) (.) (.) -- a + b === (+) a b === c c c > Anyways the simplest case that this is equivalent can be seen > here: 22:33 < vincenz> @pl \f g a b -> f (g a b) > 22:33 < lambdabot> (.) . (.) > > Writing it explicilty: > (.) f g a = f (g a) > > > so we get > (.) . (.) = \f -> (.) ((.) f) > (.) . (.) f = (.) ((.) f) > (.) . (.) f g = (.) ((.) f) g > (.) . (.) f g = ((.) f) . g > (.) . (.) f g a = ((.) f) (g a) > (.) . (.) f g a = (.) f (g a) > (.) . (.) f g a = f . (g a) > (.) . (.) f g a b = f . (g a) $ b > (.) . (.) f g a b = f ((g a) b) > (.) . (.) f g a b = f (g a b) Thanks for the proof. I see it's got the advantage over mine that it doesn't need to use eta expansion and is also much clearer. Regards, Brian.

1 0

Projects related to Haskell
by Imam Tashdid ul Alam 27 May '06

27 May '06

I was just wondering, when the HCAR will come out. just the same, for people like me who are not very involved with the community, it is difficult to get an overview of the ongoing projects. the wiki says Gofer is now abandoned and Hugs replaces it. nice to know. I wonder how about Mondrian, Eden and the rest. there should be a mechanism to officially deprecate a project, shouldn't there? and once again, a mechanism to nominate a successor so that newbies like me will know where to start exploring. cheers. Imam __________________________________________________ Do You Yahoo!? Tired of spam? Yahoo! Mail has the best spam protection around http://mail.yahoo.com

1 0

request for co-development: improving Data.CharEncoding module
by Bulat Ziganshin 27 May '06

27 May '06

Hello Haskell, i plan to publish new version of Streams library on next week (see http://haskell.org/haskellwiki/Library/Streams if you still don't know about it :) ). one of it's current drawbacks is lack of support for file encodings other than UTF-8 and Latin-1. if someone can work on this support, it will widen usage area of the library i attached to letter current version of this module. it uses monadic approach to encoding and decoding: each encoder is just a function that performs monadic PutChar action via calls to monadic PutByte action, and decoder in the same fashion translates each call to GetChar into calls to GetByte. this allows to use encoders in various environments - for monadic i/o, string conversion and so on this module requires two improvements - first, support for other UTF encodings; second, raising an exception in situations when data can't be encoded (such as char > '\255' for Latin-1) or decoded (bad UTF bytes sequence). if you are going to work on this module, please write about this here - to avoid overlapping of work -- Best regards, Bulat mailto:Bulat.Ziganshin@gmail.com

2 2

Re: [Haskell] Keeping input separate from output?
by Clifford Beshers 27 May '06

27 May '06

ihope wrote: > > How would I keep the "Foo!" from conflicting with the "Lorem ipsum > dolor sit amet."? Well, if two millennia were not enough, I'm not sure any amount of Haskell will help.

1 0

help with MPTC for type proofs?
by David Roundy 26 May '06

26 May '06

Hi all, I've been thinking about extending some (experimental) GADT-based proof code that verifies that the darcs patch theory code is properly used. A given patch has type (Patch a b), and I'd like to be able to write something like commute :: (Patch a b, Patch b c) -> (Patch a d, Patch d c) in such a way that the type system know that the type d is one particular type, uniquely determined by the types a, b and c. Currently, which I do is to make d be existential with data Pair a c where (:.) :: Patch a d -> Patch d c -> Pair a c commute :: Pair a c -> Pair a c which prevents misuse of the returned pair, but doesn't allow proper use, for example we ought to be able to compile: test (a :. b) = do (b' :. a') <- return $ commute (a :. b) (b'' :. a'') <- return $ commute (a :. b) (a''' :. b''') <- return $ commute (b' :. a'') return () but this will fail, because the compiler doesn't know that b' and b'' have the same type. So I'd like to write something like class Commutable a b d c commute :: Commutable a b d c => (Patch a b, Patch b c) -> (Patch a d, Patch d c) But for this to work properly, I'd need to guarantee that 1. if (Commutable a b d c) then (Commutable a d b c) 2. for a given three types (a b c) there exists at most one type d such that (Commutable a b c d) I have a feeling that these may be enforceable using fundeps (or associated types?), but have pretty much no idea to approach this problem, or even if it's soluble. Keep in mind that all these types (a, b, c and d) will be phantom types. Any suggestions would be welcome. -- David Roundy http://www.darcs.net

2 1

Re: [Haskell-cafe] Linking to third party libraries in windows
by Brian Hulley 26 May '06

26 May '06

Dear friends - I must have clicked "reply" instead of "reply all" so here is the reply haskell cafe would have received: Matthew Bromberg wrote: > Not only does your suggestion make more sense than what I was doing, > but also > it causes the 'matrices' to behave as expected, namely to have the > side effects > incorporated into their array values. > > I can't say I fully understand why this is true. In both cases I was > wrapping Rmatrix in > a monad after every computation. The difference is that the array > component had an > additional monad wrapper around and now it doesn't. That is, > > old case > newtype Rmatrix = Rmatrix (Int, Int, IO(StorableArray Int CDouble)) > > new case > newtype Rmatrix = Rmatrix (Int, Int, StorableArray Int CDouble) > > In the old way, the additional IO wrapper forces an additional > nesting of do loops for most processing. This is the essential difference, but I think you haven't quite understood what it means. When you say > The difference is that the array component had an > additional monad wrapper around and now it doesn't. this is not correct. IO (StorableArray Int CDouble) is a monadic *value* itself, which represents an *action* which returns a storable array, and since you are filling in the slot in Rmatrix with the action (newListArray a l), this monadic value represents the action of creating a new array whenever the action is executed. Whereas (StorableArray Int CDouble) is the actual array itself. You could also use your old definition of Rmatrix but change the way it is created eg: listtoRmatrix r c es = do arr <- newListArray (0, r * c) es return (Rmatrix r c (return arr)) do r2 <- listtoRmatrix 3 2 [1, 1, 1, 1, 1, 1] -- the rest is old code and everything would work as expected, because in this case, the monadic action contained in Rmatrix just returns the array arr that was created in the execution of listtoRmatrix 3 2 [1, 1, 1, 1, 1, 1], because listtoRmatrix is the only place where the action of creating a new array, ie (newListArray (0, r * c) es) is actually executed. I think the subtlety is one of these things that's very difficult to understand at first, but once you've grasped the fact that in Haskell expressions can evaluate to actions which are themselves values, and which in turn can create new values when executed, it will hopefully become a lot clearer. Regards, Brian. -- Logic empowers the living and justifies the dead. But societal laws, and religious dogma, empower the dead, to destroy what's living. http://www.metamilk.com

1 0