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

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

TyFun a b是开放的; 它没有像正常,升职,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" 无耻地抛出类型检查.这并不是Stringly-typed代码那么糟糕,因为它只是编译时,但仍然如此.