Function composition and currying

Stefan Karrmann sk@mathematik.uni-ulm.de
Thu, 17 Jul 2003 22:01:38 +0200


K. Fritz Ruehr (Wed, Jul 16, 2003 at 11:19:55PM -0700):
      c0 = ($)                      -- application

>     c1 = (.)                      -- good old composition
> 
>     c2 = (.) . (.)                -- my (.<) from above
> 
>     c3 = (.) . (.) . (.)
> 
>     c4 = (.) . (.) . (.) . (.)
> 
>     -- etc.
> 
> Each of these gives an appropriate generalization allowing the
> composition of a one-argument function with an n-argument one (similar
> to the notations used in the usual definitions for primitive recursive
> function). That is to say, the types are as follows (the middle three
> dots on the second line are an ellipsis, apologies in advance):
> 
>     cn :: (a -> b) -> F(t,n,a) -> F(t,n,b)
> 
>     cn  = (.)  .  ...  .  (.)      -- n occurrences of (.)
> 
> where the awkward phrase "F(t,n,x)" expands as follows via some imagined
> macro facility.
> 
>     F(t,n,x)  ===  t1 -> t2 -> ... -> tn -> x
> 
> Of course, what we really want to do is to express this as a fold of
> composition over a dynamically generated list of compositions, i.e.:
> 
>     c n = foldr (.) id (take n (repeat (.)))
> 
> But I think giving this a nice general type, where n is a run-time
> argument and the replicated (.)s have distinct but related types,
> is quite difficult.

Such an abstraction would not only be good for functions but also for
tuples.

      t 0 = ()          -- void
      t 1 = t1          -- singleton
      t 2 = (t1,t2)     -- tuple
      t 3 = (t1,t2,t3)  -- triple
      t n = (t1,...,tn) -- n-tuple

or even more general

      t * = (t1,t2,...) -- countable infinite tuple

such that

      t n == t[forall k in Natural without Zero . t(n+k) = t 0]

and something like

      curry   :: (t * -> a) -> c * -> a
      uncurry :: (c * -> a) -> t * -> a
      zip     :: c [*] -> [t *]     -- What's a good notation for this?
      unzip   :: [t *] -> c [*]

(Maybe only with n instead of * forall n.)

-- 
Stefan Karrmann