Taral wrote:
On 5/28/06, Dominic Steinitz <dominic.steinitz@blueyonder.co.uk> wrote:
Is this defined in some library? Thanks, Dominic.
Don't think so. I use:
\a b -> f (g a b)
I don't see how (.) . (.) translates into something so simple. Using c for (.) to make things easier to write, I get: (.) . (.) === c c c === \x -> (c c c x) === \x -> (c (c x)) === \x -> (\y z -> c (c x) y z) === \x -> (\y z -> (c x) (y z)) === \x -> (\y z -> (\p q -> c x q p) (y z)) === \x -> (\y z -> (\p q -> x (q p) (y z)) === \x -> (\y z -> (\q -> x (q (y z)))) === \x y z q -> x (q (y z)) Have I made an error somewhere above? Thanks, Brian. -- Logic empowers us and Love gives us purpose. But societal laws, and religious dogma, empower the dead, to destroy us. http://www.metamilk.com
Why not ask the computer? -- Lennart bamse% ghci ___ ___ _ / _ \ /\ /\/ __(_) / /_\// /_/ / / | | GHC Interactive, version 6.4.1, for Haskell 98. / /_\\/ __ / /___| | http://www.haskell.org/ghc/ \____/\/ /_/\____/|_| Type :? for help. Loading package base-1.0 ... linking ... done. Prelude> :t (.) . (.) (.) . (.) :: (b -> c) -> (a -> a1 -> b) -> a -> a1 -> c Prelude> Leaving GHCi. bamse% djinn Welcome to Djinn version 2005-12-12. Type :h to get help. Djinn> f ? (b -> c) -> (a -> a1 -> b) -> a -> a1 -> c f :: (b -> c) -> (a -> a1 -> b) -> a -> a1 -> c f x1 x2 x3 x4 = x1 (x2 x3 x4) Djinn> :q Bye. Brian Hulley wrote:
Taral wrote:
On 5/28/06, Dominic Steinitz <dominic.steinitz@blueyonder.co.uk> wrote:
Is this defined in some library? Thanks, Dominic.
Don't think so. I use:
\a b -> f (g a b)
I don't see how (.) . (.) translates into something so simple. Using c for (.) to make things easier to write, I get:
(.) . (.) === c c c === \x -> (c c c x) === \x -> (c (c x)) === \x -> (\y z -> c (c x) y z) === \x -> (\y z -> (c x) (y z)) === \x -> (\y z -> (\p q -> c x q p) (y z)) === \x -> (\y z -> (\p q -> x (q p) (y z)) === \x -> (\y z -> (\q -> x (q (y z))))
=== \x y z q -> x (q (y z))
Have I made an error somewhere above?
Thanks, Brian.
On Sunday 28 May 2006 04:17 pm, Lennart Augustsson wrote:
> Why not ask the computer?
>
> -- Lennart
[snip]
Another proof-by-calculation:
-----------------------------------------------------------
The Lambda Shell, version 0.2
Copyright 2005-2006, Robert Dockins
The Lambda Shell comes with ABSOLUTELY NO WARRANTY; for details
type ':nowarranty'. This is free software, and you are welcome to
redistribute it under certain conditions; type ':gpl'
for details
> let c = \f g x. f (g x)
> c c c
\x g x_0 x_1. x (g x_0 x_1)
> :trace
trace on
> c c c
1) c c c
2) (\f g x. f (g x)) c c
3) (\g x. c (g x)) c
4) \x. c (c x)
5) \x. (\f g x_0. f (g x_0)) (c x)
6) \x g x_0. c x (g x_0)
7) \x g x_0. (\f g_1 x_2. f (g_1 x_2)) x (g x_0)
8) \x g x_0. (\g_1 x_2. x (g_1 x_2)) (g x_0)
9) \x g x_0 x_1. x (g x_0 x_1)
--
Rob Dockins
Talk softly and drive a Sherman tank.
Laugh hard, it's a long way to the bank.
-- TMBG
Lennart Augustsson wrote:
Why not ask the computer?
-- Lennart
bamse% ghci ___ ___ _ / _ \ /\ /\/ __(_) / /_\// /_/ / / | | GHC Interactive, version 6.4.1, for Haskell 98. / /_\\/ __ / /___| | http://www.haskell.org/ghc/ \____/\/ /_/\____/|_| Type :? for help.
Loading package base-1.0 ... linking ... done. Prelude> :t (.) . (.) (.) . (.) :: (b -> c) -> (a -> a1 -> b) -> a -> a1 -> c Prelude> Leaving GHCi. bamse% djinn Welcome to Djinn version 2005-12-12. Type :h to get help. Djinn> f ? (b -> c) -> (a -> a1 -> b) -> a -> a1 -> c f :: (b -> c) -> (a -> a1 -> b) -> a -> a1 -> c f x1 x2 x3 x4 = x1 (x2 x3 x4) Djinn> :q Bye.
Thanks! Although I note that Djinn will give a representative function corresponding to the type which is not necessarily (.) . (.), and the type given by GHCi doesn't tell me how it got there...
Brian Hulley wrote:
Taral wrote:
On 5/28/06, Dominic Steinitz <dominic.steinitz@blueyonder.co.uk> wrote:
Is this defined in some library? Thanks, Dominic.
Don't think so. I use:
\a b -> f (g a b)
I don't see how (.) . (.) translates into something so simple. Using c for (.) to make things easier to write, I get:
(.) . (.) === c c c === \x -> (c c c x) === \x -> (c (c x)) === \x -> (\y z -> c (c x) y z) === \x -> (\y z -> (c x) (y z)) === \x -> (\y z -> (\p q -> c x q p) (y z)) === \x -> (\y z -> (\p q -> x (q p) (y z)) === \x -> (\y z -> (\q -> x (q (y z))))
=== \x y z q -> x (q (y z))
Have I made an error somewhere above?
I see my error was that I was reversing the args in eta expansion, so the correct derivation is: (.) . (.) === c c c === \x -> c c c x === \x -> c (c x) === \x -> (\y z -> c (c x) y z) === \x -> (\y z -> (c x) (y z)) === \x -> (\y z -> (\p q -> c x p q)(y z)) -- where I went wrong before === \x -> (\y z -> (\p q -> x (p q))(y z)) === \x -> (\y z -> (\q -> x ((y z) q)) === \x y z q -> x (y z q) My apologies to Taral for doubting the original simplification... Regards, Brian. - Logic empowers us and Love gives us purpose. But societal laws, and religious dogma, empower the dead, to destroy us. http://www.metamilk.com
On Sunday 28 May 2006 05:02 pm, Brian Hulley wrote:
Lennart Augustsson wrote:
Why not ask the computer?
-- Lennart
bamse% ghci ___ ___ _ / _ \ /\ /\/ __(_) / /_\// /_/ / / | | GHC Interactive, version 6.4.1, for Haskell 98. / /_\\/ __ / /___| | http://www.haskell.org/ghc/ \____/\/ /_/\____/|_| Type :? for help.
Loading package base-1.0 ... linking ... done. Prelude> :t (.) . (.) (.) . (.) :: (b -> c) -> (a -> a1 -> b) -> a -> a1 -> c Prelude> Leaving GHCi. bamse% djinn Welcome to Djinn version 2005-12-12. Type :h to get help. Djinn> f ? (b -> c) -> (a -> a1 -> b) -> a -> a1 -> c f :: (b -> c) -> (a -> a1 -> b) -> a -> a1 -> c f x1 x2 x3 x4 = x1 (x2 x3 x4) Djinn> :q Bye.
Thanks! Although I note that Djinn will give a representative function corresponding to the type which is not necessarily (.) . (.), and the type given by GHCi doesn't tell me how it got there...
Brian Hulley wrote:
Taral wrote:
On 5/28/06, Dominic Steinitz <dominic.steinitz@blueyonder.co.uk>
wrote:
Is this defined in some library? Thanks, Dominic.
Don't think so. I use:
\a b -> f (g a b)
I don't see how (.) . (.) translates into something so simple. Using c for (.) to make things easier to write, I get:
[snip]
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.
(.) . (.) === c c c === \x -> c c c x === \x -> c (c x) === \x -> (\y z -> c (c x) y z) === \x -> (\y z -> (c x) (y z)) === \x -> (\y z -> (\p q -> c x p q)(y z)) -- where I went wrong before === \x -> (\y z -> (\p q -> x (p q))(y z)) === \x -> (\y z -> (\q -> x ((y z) q))
=== \x y z q -> x (y z q)
My apologies to Taral for doubting the original simplification...
Regards, Brian.
-- Rob Dockins Talk softly and drive a Sherman tank. Laugh hard, it's a long way to the bank. -- TMBG
Brian Hulley wrote:
Taral wrote:
On 5/28/06, Dominic Steinitz <dominic.steinitz@blueyonder.co.uk> wrote:
Is this defined in some library? Thanks, Dominic.
Don't think so. I use:
\a b -> f (g a b)
I don't see how (.) . (.) translates into something so simple. Using c for (.) to make things easier to write, I get:
(.) . (.) === c c c === \x -> (c c c x) === \x -> (c (c x)) === \x -> (\y z -> c (c x) y z)
Here was one error ^^^^ so fixing it and continuing: \x -> (c (c x)) === \x -> (\y z -> c (c x) z y) === \x -> (\y z -> (c x) (z y)) === \x -> (\y z -> (\p q -> c x q p) (z y)) === \x -> (\y z -> (\p q -> x (q p)) (z y)) === \x -> (\y z -> (\q -> x (q (z y)))) === \x y z q -> x (q (z y)) But it still doesn't match f (g a b)... Regards, Brian.
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). 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) Cheers Christophe Brian Hulley wrote:
Brian Hulley wrote:
Taral wrote:
On 5/28/06, Dominic Steinitz <dominic.steinitz@blueyonder.co.uk> wrote:
Is this defined in some library? Thanks, Dominic.
Don't think so. I use:
\a b -> f (g a b)
I don't see how (.) . (.) translates into something so simple. Using c for (.) to make things easier to write, I get:
(.) . (.) === c c c === \x -> (c c c x) === \x -> (c (c x)) === \x -> (\y z -> c (c x) y z)
Here was one error ^^^^ so fixing it and continuing:
\x -> (c (c x)) === \x -> (\y z -> c (c x) z y) === \x -> (\y z -> (c x) (z y)) === \x -> (\y z -> (\p q -> c x q p) (z y)) === \x -> (\y z -> (\p q -> x (q p)) (z y)) === \x -> (\y z -> (\q -> x (q (z y))))
=== \x y z q -> x (q (z y))
But it still doesn't match f (g a b)...
Regards, Brian. _______________________________________________ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
-- 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. **********
Taral wrote:
On 5/28/06, Dominic Steinitz <dominic.steinitz@blueyonder.co.uk> wrote:
Is this defined in some library? Thanks, Dominic.
Don't think so. I use:
\a b -> f (g a b)
Taral, Thanks. What prompted this question is that I find myself writing things like: foo = ((.).(.)) concat intersperse I think foo' = \a b -> concat (intersperse a b) is probably clearer but I ended up writing infixr $. ($.) = (.) . (.) and then foo' = concat $. intersperse Of course one could go on and define infixr $.. ($..) = (.) . (.) . (.) and so on. I just wondered if there was a standard nomenclature for such functions a la liftM, liftM2 etc? The answer seems to be no. Thanks, Dominic.
participants (6)
-
Brian Hulley -
Christophe Poucet -
Dominic Steinitz -
Lennart Augustsson -
Robert Dockins -
Taral