如何从容器中构建一个类型化的可变参数函数？

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 

他们提升到型A级单：与

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

然后：

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

类型existentials的名单

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 s，对列表中的每个数字加上(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 

我们需要在价值层面来比较Natty秒。两个Natty s为相等，当且仅当它们由相同数量的索引（这就是为什么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 

iee求和所有参数，直到遇到5（以Natty的形式），并添加100。如果列表中没有5，则返回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。