如何从容器构建类型可变参数函数?

How to build a typed variadic function from a container?

考虑可爱的小 HoleyMonoid 库,它可以让您构建类型可变的 printf 类函数,如下所示:

{-# LANGUAGE NoMonomorphismRestriction #-}

import Control.Category
import Data.HoleyMonoid
import Prelude hiding ((.), id)

foo =
    now "hello "
  . later id
  . now ", you are "
  . later show
  . now " years old"

bar = run foo

-- > bar "alice" 42
-- "hello alice, you are 42 years old"

-- > bar 42 "alice"
-- type error

有什么方法可以检查容器(列表、AST 等)并根据其内容构建这样的函数吗?

作为玩具示例,您可以想象如下内容:

import Data.Monoid

adder = go where
  go [] = now (Sum 0)
  go (x:xs)
    | x == 5    = now 100 . go xs
    | otherwise = later id . go xs

-- hypothetical usage
--
-- > :t run adder [1, 3, 5]
-- Num a => Sum a -> Sum a -> Sum a
--
-- > getSum $ run adder [1, 3, 5] 0 1
-- 101

adder 未通过发生检查,但您可以看到我的目的。问题似乎是很难在任何地方保持计算状态,因为 now 100later id 是不同的类型。

我将忽略 HoleyMonoid 库。

我们需要自然数:

data Nat = Z | S Nat

将它们提升到类型级别的单例:

data Natty :: Nat -> * where
    Zy :: Natty Z
    Sy :: Natty n -> Natty (S n)

存在列表的类型:

data Listy (b :: a -> *) :: [a] -> * where
    Nilly :: Listy b '[]
    Consy :: b x -> Listy b xs -> Listy b (x ': xs)

然后

type Natties = Listy Natty

我们可以定义

adder :: Natties ns -> Adder ns

其中 ns :: [Nat]Adder 类型族定义如下:

type family Adder (ns :: [Nat]) :: * where
    Adder '[]       = Int
    Adder (n ': ns) = If (NatEq n (S (S (S (S (S Z)))))) Int (Int -> Adder ns)

即折叠 Nat 的列表,为列表中的每个数字添加 (Int ->),直到遇到 5(以 Nat 形式)。它实际上应该是

if_then_else_ b x y = if b then x else y

type family Adder (ns :: [Nat]) :: * where
    Adder '[]       = Int
    Adder (n ': ns) = 'if_then_else_ (n '== 'fromInt 5) Int (Int -> Adder ns)

但是 GHC 向我抛出一些我不想理解的令人毛骨悚然的错误。

NatEq 类型族的定义方式很明显:

type family NatEq n m :: Bool where
    NatEq  Z     Z    = True
    NatEq  Z    (S m) = False
    NatEq (S n)  Z    = False
    NatEq (S n) (S m) = NatEq n m

我们需要在价值层面比较Nattys。两个 Natty 相等,当且仅当它们由相同的数字索引(这就是 Natty 是单例的原因):

nattyEq :: Natty n -> Natty m -> Booly (NatEq n m)
nattyEq  Zy     Zy    = Truly
nattyEq  Zy    (Sy m) = Falsy
nattyEq (Sy n)  Zy    = Falsy
nattyEq (Sy n) (Sy m) = nattyEq n m

其中 Booly 是另一个单例:

data Booly :: Bool -> * where
    Truly :: Booly True
    Falsy :: Booly False

最后,adder的定义:

adder = go 0 where
    go :: Int -> Natties ns -> Adder ns
    go i  Nilly       = 0
    go i (Consy n ns) = case nattyEq n (Sy (Sy (Sy (Sy (Sy Zy))))) of
        Truly -> i + 100
        Falsy -> \a -> go (i + a) ns

即对所有参数求和,直到遇到 5(以 Natty 形式),然后添加 100。如果列表中没有 5,则 return 0.

测试:

list = Consy Zy $ Consy (Sy Zy) $ Consy (Sy (Sy (Sy (Sy (Sy Zy))))) $ Consy Zy $ Nilly

main = do
    print $ adder (Consy Zy $ Consy (Sy Zy) $ Nilly) 3 9 -- 0
    print $ adder list 6 8                               -- 114
    print $ adder (Consy (Sy (Sy Zy)) list) 1 2 3        -- 106

code.