05:10 <pyro-> now i am writing a cpsTransform function :D
05:10 <pyro-> it already works, but the current version introduces superflous continuations
05:10 <pyro-> so i am trying to fix :D
05:10 <ReinH> pyro-: Here's a CPS transform function: flip ($)
05:11 <pyro-> i will find out about flip
05:11 <ReinH>@src flip
05:11 <lambdabot> flip f x y = f y x
05:11 <ReinH> pyro-: the essence of CPS can be described as follows:
05:11 <ReinH> :t flip ($)
05:11 <lambdabot> b -> (b -> c) -> c
05:12 <ReinH> is the type of a function which takes a value and produces a suspended computation that takes a continuation and runs it against the value
05:12 <ReinH> for example:
05:12 <ReinH> > let c = flip ($) 3 in c show
05:12 <lambdabot> "3"
05:12 <ReinH> > let c = flip ($) 3 in c succ
05:12 <lambdabot> 4
05:13 <mm_freak_> direct style: f x = 3*x + 1
05:13 <mm_freak_> CPS: f x k = k (3*x + 1)
05:13 <mm_freak_> the rules are: take a continuation argument and be fully polymorphic on the result type
05:13 <mm_freak_> f :: Integer -> (Integer -> r) -> r
05:14 <mm_freak_> as long as your result type is fully polymorphic and doesn't unify with anything else in the type signature you can't do anything wrong other than to descend
05:38 <ReinH> So for example, if you have an incredibly simple expression language like data Expr a = Val a | Neg a | Add a a
05:38 <ReinH> a (more) initial encoding of an expression would be Add (Val 1) (Neg (Val 1))
05:38 <ReinH> A (more) final encoding might be (1 - 1) or even 0
05:39 <ReinH> The initial encoding generally is more flexible (you can still write a double-negation elimination rule, for instance
05:39 <ReinH> the final encoding is less flexible, but also does more work up-front
05:40 <ReinH> More initial encodings tend to force you to use quantification and type-level tricks, CPS and pre-applied functions tend to appear more in final encodings
05:40 <ReinH> An even smaller example:
05:40 <ReinH> \f z -> foldr f z [1,2,3] is a final encoding of the list [1,2,3]
05:41 <ReinH> pyro-: I'm not really a lisper, but I'm always looking for good reading material
05:41 <ReinH> for bonus points, the foldr encoding is *invertible* as well :)
05:44 <ReinH> pyro-: the relevance is that you seem to be using the cps transform in a more initial encoding than I usually see it
05:44 <ReinH> not that this is at all bad
05:46 <bitemyapp> ReinH: where does the invertibility in the final encoding come from?
05:46 <ReinH> foldr (:) [] :)
05:46 <ReinH> it's not generally so
05:46 <bitemyapp> > foldr (:) [] [1, 2, 3]
05:46 <lambdabot> [1,2,3]
05:47 <bitemyapp> I may not understand the proper meaning of invertibility in this case.
05:47 <bitemyapp> Do you mean invertibility from final to initial encoding?
05:47 <ReinH> Just that, yes
05:47 <bitemyapp> how would it get you back to final from initial?
05:47 <ReinH> I'm not sure if that's the correct term
05:47 <bitemyapp> I don't think it is, but the intent is understood and appreciated.
05:48 <bitemyapp> invertibility implies isomorphism, implies ability to go final -> initial -> final
05:48 <ReinH> well, there is an isomorphism
05:48 <bitemyapp> well, we've established final -> initial, where's initial -> final for this example?
05:49 <bitemyapp> I figured it was a morphism of some sort, but with only a final -> initial and not a way to get back, I wasn't sure which.
05:49 <ReinH> toInitial k = k (:) []; toFinal xs = \f z -> foldr f z xs
