Data.Functionの `on`関数は、どのようにn項関数で動作するように一般化できますか？基本パッケージに

Question

Data.Functionは単項機能のため(.) :: (b -> c) -> (a -> b) -> a -> cに類似している機能on :: (b -> b -> c) -> (a -> b) -> a -> a -> cを含有するので、私はon' 1 length negate、on' 2 length compare、等を書き込むことができるように、一般化として機能on' :: Int -> ...を記述しようとした、しかし、そのような機能しますタイプチェックではありません。on'の3番目の引数の関数結果の型は最初の引数に依存するためです。

どうすればこのような関数を書くことができますか？たぶん、カスタムデータ型の関数をラップする必要があります。そのため、作成される関数の型は、最初のパラメータの型と最終結果の型のみに依存します。

Answer 1

これは可能な方法です。まず、レベル・ナチュラルを定義します。

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

data Nat = O | S Nat 

我々はn引数を持つa -> a -> ... a -> bを定義します。

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 

最後に、いくつかの例です。私は型クラスからc引数を削除する方法を見つけることができません

：

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は型から決定されていないので、あいまいです。したがって、明示的に渡す必要があります（上記のようにタイプアプリケーションを使用するか、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、それはそれは失敗します。

私はまた、家族に注射しようとしましたが、失敗しました。