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

Question

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

{-# 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库。我很乐意举一个例子，使用它或其他"变通方法"来实现对Nat上的算术运算(如+、*、-和Mod(进行抽象的类似效果。

Answer 1

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

核心是"开放型"：

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

CCD_ 12是一类开放的；它不像普通的、提升的、data类型那样是封闭的。您可以按如下方式"声明"新函数。

data Plus :: TyFun Nat (TyFun Nat Nat)

然后，您可以定义这个类型族来链接声明和定义

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类型的代码那么糟糕，因为它都是编译时的，但仍然如此。