Data.Function的on函數如何推廣到n元函數？

Question

Data.Function在基座包中包含的功能on :: (b -> b -> c) -> (a -> b) -> a -> a -> c，其類似於(.) :: (b -> c) -> (a -> b) -> a -> c爲一元函數，所以我試圖寫的函數on' :: Int -> ...作爲概括，以便可以寫on' 1 length negate，on' 2 length compare等，然而這樣的功能將不是類型檢查，因爲on'的第三個參數的函數結果的類型取決於第一個參數。

我該如何去寫這樣的功能？也許我必須將函數封裝在自定義數據類型中，以便組合函數的類型僅取決於第一個參數的類型和最終結果的類型？

Answer 1

這是一種可能的方法。我們從定義類型級別自然開始。

{-# LANGUAGE ScopedTypeVariables, TypeFamilies, DataKinds, TypeApplications, 
      AllowAmbiguousTypes, MultiParamTypeClasses, FlexibleInstances #-} 
{-# OPTIONS -Wall #-} 

data Nat = O | S Nat 

我們定義a -> a -> ... a -> b與n參數。

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

然後介紹了這些土黃的自定義類我們on，並以感性的方式實現它爲每一個natiral。

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 ('S n) c where 
    on f g = \aVal -> on @n @c (f (g aVal)) g 

最後一些例子。

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 @('S ('S 'O)) fun2 funG 1 2 

test3 :: String 
test3 = on @('S ('S ('S 'O))) fun3 funG 1 2 3 

---

相對題外話注：

我無法找到一個方法來刪除從類型類c說法。由於c不是根據類型確定的，因此它是不明確的，因此我必須明確地通過它（通過類型應用程序 - 如上所述 - 或Proxy）。但是，要通過它，我需要c在範圍內。如果我從班級中刪除c，它將超出範圍。如果我使用實例簽名，我可以將c帶回範圍，但由於類型不明確，GHC不會將其識別爲相同的c。

OnGeneralization2.hs:18:10: error: 
    • Couldn't match type ‘F n a c0’ with ‘F n a c’ 
     Expected type: F ('S n) b c -> (a -> b) -> F ('S n) a c 
     Actual type: F ('S n) b c0 -> (a -> b) -> F ('S 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 ('S n) b c -> (a -> b) -> F ('S n) a c 
     is more polymorphic than: 
      forall a b c. F ('S n) b c -> (a -> b) -> F ('S 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 ('S n) b c -> (a -> b) -> F ('S n) a c 
      Class sig: forall a b c. 
         F ('S n) b c -> (a -> b) -> F ('S n) a c 
     In the instance declaration for ‘On ('S n)’ 

注意最後一行：他們是完全一樣的類型，但爲了檢查它們的亞型，GHC依然採用新鮮斯科倫類型常量c0，這使得它失敗。

我也試圖讓家庭內射，但失敗了。