haskell – 如何从容器构建类型化的可变参数函数？

2023年8月4日 276次阅读

考虑一下可爱的小
HoleyMonoid库,它允许您构建类型化的类似variadic的函数,如下所示：

{-# 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

加法器未通过发生检查,但你可以看到我正在拍摄的内容.问题似乎是难以在任何地方保持计算状态,即现在100和后来的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)

即折叠Nats列表,在列表中的每个数字前面加上(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.两个Nattys是平等的,如果他们用相同的数字索引(这就是为什么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 = 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,则返回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.

点赞