如何将类型族命名为高阶类函数

Question

是否可以使用类型族作为高阶 "type function" 传递给另一个类型族？一个简单的例子是下面的代码：

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Test where
import GHC.TypeLits as T

type family Apply (f :: Nat -> Nat -> Nat) (n :: Nat) (m :: Nat) :: Nat where
  Apply f n m = f n m

type family Plus (n :: Nat) (m :: Nat) :: Nat where
  Plus n m = n T.+ m

type family Plus' (n :: Nat) (m :: Nat) :: Nat where
  Plus' n m = Apply (T.+) n m

Plus 的第一个声明有效，而第二个 (Plus') 产生以下错误：

Test.hs:19:3: error:
    • The type family ‘+’ should have 2 arguments, but has been given none
    • In the equations for closed type family ‘Plus'’
      In the type family declaration for ‘Plus'’
   |
19 |   Plus' n m = Apply (T.+) n m
   |   ^^^^^^^^^^^^^^^^^^^^^^^^^^^

有没有办法用Apply类型的函数来实现Plus？

编辑链接到 https://ghc.haskell.org/trac/ghc/ticket/9898 上的功能请求报告的评论者。它提到了 singleton 库。我很乐意使用它或其他 "workarounds" 来实现对 Nat 上的算术运算进行抽象的类似效果，例如 +、*、- 和 Mod.

Answer 1

一个有用的方法是去功能化。您可以自己实现，也可以在 singletons 库中找到实现。

核心是“开放式”：

data TYFUN :: Type -> Type -> Type
type TyFun a b = TYFUN a b -> Type

TyFun a b是开放式；它不像正常的、提升的、data 那样关闭。您“声明”新功能如下。

data Plus :: TyFun Nat (TyFun Nat Nat)

然后您可以将此类型族定义为link声明和定义

type family Apply (f :: TyFun a b) (x :: a) :: b
data PlusSym1 :: Nat -> TyFun Nat Nat -- see how we curry
type instance Apply Plus x = PlusSym1 x
type instance Apply (PlusSym1 x) y = x + y

现在，Plus 是一个普通的类型构造器：一个数据类型，而不是一个类型族。这意味着您可以将其传递给其他类型族。请注意，他们必须 TyFun 意识到自己。

type family Foldr (cons :: TyFun a (TyFun b b)) (nil :: b) (xs :: [a]) :: b where
    Foldr _ n '[] = n
    Foldr c n (x:xs) = Apply (Apply c x) (Foldr c n xs)
type Example = Foldr Plus 0 [1,2,3]

开放类型背后的想法是 Type 已经是开放类型，而像 A -> Type、A -> B -> Type 这样的类型本身也是开放的。 TYFUN 是一个将事物标识为 TyFuns 的标签，而 TyFun 是一种与其他开放类型有效分离的开放类型。您也可以直接使用 Type 开放式：

type family TyFunI :: Type -> Type
type family TyFunO :: Type -> Type
type family Apply (f :: Type) (x :: TyFunI f) :: TyFunO f
data Plus :: Type
data PlusSym1 :: Nat -> Type
type instance TyFunI Plus = Nat
type instance TyFunO Plus = Type
type instance TyFunI (PlusSym1 _) = Nat
type instance TyFunO (PlusSym1 _) = Nat
type instance Apply Plus x = PlusSym1 x
type instance Apply (PlusSym1 x) y = x + y

从好的方面来说，这可以处理依赖类型的函数，但另一方面，它这样做只是因为它通过使所有内容都“Typely-typed”而厚颜无耻地抛出了类型检查。这并不像 String 直接输入的代码那么糟糕，因为它都是编译时的，但仍然如此。

如何将类型族命名为高阶类函数

How can one name a type family as a higher-order kind function

haskell

ghc