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