haskell - 如何将 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

我们用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 引入一个针对这些自然数的自定义类，并以归纳方式为每个自然数实现它。

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 仍然使用新的 Skolem 类型常量 c0 ，这使得它失败。

我也尝试过让家庭单射，但失败了。