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

1 answer

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.



All Articles