# How should Data.Function `on` be generalized to work with n-ary functions?

The Data.Function in the base package contains a function `on :: (b -> b -> c) -> (a -> b) -> a -> a -> c`

that is similar `(.) :: (b -> c) -> (a -> b) -> a -> c`

for unary functions, so I tried to write the function `on' :: Int -> ...`

as a generalization so that I could write `on' 1 length negate`

, `on' 2 length compare`

etc., however, such a function will not check the type because the result type of the function is from the `on'`

third the argument depends on the first argument.

How can I write a function like this? Maybe I'll have to wrap the functions in a custom data type so that the types of composite functions only depend on the type of the first parameter and the type of the final result?

source to share

Here's a possible approach. Let's start by defining type-level naturals.

```
{-# LANGUAGE ScopedTypeVariables, TypeFamilies, DataKinds, TypeApplications,
AllowAmbiguousTypes, MultiParamTypeClasses, FlexibleInstances #-}
{-# OPTIONS -Wall #-}
data Nat = O | S Nat
```

Let's define `a -> a -> ... a -> b`

with arguments `n`

.

```
type family F (n :: Nat) a b where
F 'O a b = b
F ( n) a b = a -> F n a b
```

Then we inject a custom class above these naturals for ours `on`

and implement it for each natiral in an inductive way.

```
class On (n :: Nat) c where
on :: forall a b. F n b c -> (a -> b) -> F n a c
instance On 'O c where
on f _g = f
instance On n c => On ( n) c where
on f g = \aVal -> on @n @c (f (g aVal)) g
```

Finally, some examples.

```
fun2 :: String -> String -> String
fun2 x y = "(" ++ x ++ ", " ++ y ++ ")"
fun3 :: String -> String -> String -> String
fun3 x y z = "(" ++ x ++ ", " ++ y ++ ", " ++ z ++ ")"
funG :: Int -> String
funG n = replicate n '#'
test2 :: String
test2 = on @( ( 'O)) fun2 funG 1 2
test3 :: String
test3 = on @( ( ( 'O))) fun3 funG 1 2 3
```

Relative non-standard note:

I cannot find a way to remove the argument `c`

from the type class. Since `c`

it is not type-specific, it is ambiguous, so I have to pass it explicitly (either through the type application as done above, or through `Proxy`

). However, in order to pass it, I need to `c`

be in scope. If I remove `c`

from the class it goes out of scope. If I use instance signature, I can revert `c`

back to scope, but GHC does not recognize it as the same `c`

due to type ambiguity.

```
OnGeneralization2.hs:18:10: error:
β’ Couldn't match type βF n a c0β with βF n a cβ
Expected type: F ( n) b c -> (a -> b) -> F ( n) a c
Actual type: F ( n) b c0 -> (a -> b) -> F ( n) a c0
NB: βFβ is a type function, and may not be injective
The type variable βc0β is ambiguous
β’ When checking that:
forall a b c. F ( n) b c -> (a -> b) -> F ( n) a c
is more polymorphic than:
forall a b c. F ( n) b c -> (a -> b) -> F ( n) a c
When checking that instance signature for βonβ
is more general than its signature in the class
Instance sig: forall a b c.
F ( n) b c -> (a -> b) -> F ( n) a c
Class sig: forall a b c.
F ( n) b c -> (a -> b) -> F ( n) a c
In the instance declaration for βOn ( n)β
```

Notice the last line: they are exactly the same types, but GHC still uses fresh Skolem constants to check for subtyping `c0`

, and this crashes.

I also tried to make the family injective, but failed.

source to share