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

Question

考虑可爱的小 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 100 和 later id 是不同的类型。

Answer 1

我将忽略 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.

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

How to build a typed variadic function from a container?

continuations

haskell

variadic-functions