Implementing functional addition in Haskell

Here's a pretty simple approach using type families that works monomorphically in the numeric type (e.g., specialized to Int). We'll need a few extensions:

{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}

The function f will be defined in a type class:

class VarArgs r s where
  type F r s
  f :: r -> s -> F r s

and we'll handle the following cases. If the type of the first function is of form a :: Int -> r, we'll use the following instance to gobble an argument x and feed it to a:

instance VarArgs r s => VarArgs (Int -> r) s where
  type F (Int -> r) s = Int -> F r s
  f :: (Int -> r) -> s -> Int -> F r s
  f a b x = f (a x) b

This has the effect of recursing on the type of a until it's of the form Int. Then, we'll use a similar instance to recurse on the type b :: Int -> s:

instance VarArgs Int s => VarArgs Int (Int -> s) where
  type F Int (Int -> s) = Int -> F Int s
  f :: Int -> (Int -> s) -> Int -> F Int s
  f a b x = f a (b x)

Ultimately, both functions will be reduced to 0-ary functions of type a, b :: Int, and we can use the terminal instance:

instance VarArgs Int Int where
  type F Int Int = Int
  f :: Int -> Int -> Int
  f a b = a + b

Here's a little test to prove it works:

times2 :: Int -> Int -> Int
times2 x y = x * y
times3 :: Int -> Int -> Int -> Int
times3 x y z = x * y * z

foo :: [Int]
foo = [ f times2 times2 1 2 3 4
      , f times2 times3 1 2 3 4 5
      , f times3 times2 1 2 3 4 5
      , f times3 times3 1 2 3 4 5 6]

and loading this into GHCi gives:

> foo
[14,62,26,126]
>

Generalizing this to be polymorphic in any Num type doesn't seem to be straightforward. Replacing the Int type with a constrained Num n type leads to errors regarding conflicting family instance declarations.

This is easy and simple - much simpler than @K.A.Buhr's type family approach, in my opinion - if you tweak your representation of an n-ary function, instead using a unary function of an n-dimensional vector.

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

import Prelude hiding (splitAt)
import Data.Bifunctor

The usual suspects: (type-level) natural numbers, their (value-level) singletons, type-level addition, and vectors.

data Nat = Z | S Nat
data Natty n where
    Zy :: Natty Z
    Sy :: Natty n -> Natty (S n)
type family n + m where
    Z + m = m
    S n + m = S (n + m)

data Vec n a where
    Nil :: Vec Z a
    (:>) :: a -> Vec n a -> Vec (S n) a

splitAt takes a runtime Natty - it needs to know at runtime where to split the vector - and a vector that is at least as long as the Natty.

splitAt :: Natty n -> Vec (n + m) a -> (Vec n a, Vec m a)
splitAt Zy xs = (Nil, xs)
splitAt (Sy n) (x :> xs) =
    let (ys, zs) = splitAt n xs
    in (x :> ys, zs)

Then your f, which I'm calling splitApply, is a straightforward application of splitAt.

splitApply :: Natty n -> (Vec n a -> b) -> (Vec m a -> c) -> Vec (n + m) a -> (b, c)
splitApply at f g xs = bimap f g $ splitAt at xs

(I haven't bothered to show the "add the results" part, because it's so simple that I bored myself writing it. You could argue that, since Hask is a monoidal category, (,) represents a sort of addition anyway.)