是否可以迭代一个非自同态的应用？

Question

在 Haskell 中，如果我想将自同态 a -> a 重复应用于 a 类型的值，我可以只使用 iterate.

不是自同态但足够通用以在其 return 类型上正确工作的函数怎么样？

考虑例如Just :: a -> Maybe a；我会写

Just . Just . Just ...

想多少次都可以。有没有办法用

之类的东西很快地写这个

iterate' 3 Just :: a -> Maybe (Maybe (Maybe a))

或者我们是否需要依赖类型之类的东西来做到这一点？

Answer 1

如果您在编译时知道数字，则可以使用模板 haskell 来完成（但除非数字非常大，否则我认为不值得这么麻烦）。如果您在编译时还不知道数字，则需要正确建模 return 类型，我们可以使用非常规类型来做到这一点：

data Iter f a = Iter0 a | IterS (Iter f (f a))

iterate' :: Int -> (forall x. x -> f x) -> a -> Iter f a
iterate' 0 f x = Iter0 x
iterate' n f x = IterS (iterate' (n-1) f (f x))

Iter本质上是一种表达数据类型a | f a | f (f a) | f (f (f a)) | ...的方式。要使用结果，您需要在 Iter 上递归。此外，对于某些类型构造函数 f，该函数必须采用 a -> f a 形式，因此您可能需要进行一些新类型包装才能到达那里。所以...无论哪种方式都是一种痛苦。

Answer 2

可以对您建议的语法进行细微调整：iterate' @3 Just 而不是 iterate' 3 Just。

这是因为结果类型取决于数字，所以数字必须是类型文字，而不是值文字 .正如您正确注意到的那样，使用任意数字执行此操作需要依赖类型[1]，Haskell 没有。

{-# OPTIONS_GHC -Wall #-}
{-# LANGUAGE TypeFamilies, KindSignatures, DataKinds,
    FlexibleInstances, UndecidableInstances, ScopedTypeVariables,
    FunctionalDependencies, TypeApplications, RankNTypes, FlexibleContexts,
    AllowAmbiguousTypes #-}

import qualified GHC.TypeLits as Lit

-- from type-natural
import Data.Type.Natural
import Data.Type.Natural.Builtin

class Iterate (n :: Nat) (f :: * -> *) (a :: *) (r :: *)
  | n f a -> r
  where
  iterate_peano :: Sing n -> (forall b . b -> f b) -> a -> r

instance Iterate 'Z f a a where
  iterate_peano SZ _ = id
instance Iterate n f (f a) r => Iterate ('S n) f a r where
  iterate_peano (SS n) f x = iterate_peano n f (f x)

iterate'
  :: forall (n :: Lit.Nat) f a r .
     (Iterate (ToPeano n) f a r, SingI n)
  => (forall b . b -> f b) -> a -> r
iterate' f a = iterate_peano (sToPeano (sing :: Sing n)) f a

如果你在 ghci 中加载它，你可以说

*Main> :t iterate' @3 Just
iterate' @3 Just :: a -> Maybe (Maybe (Maybe a))
*Main> iterate' @3 Just True
Just (Just (Just True))

此代码使用了两种不同类型的自然数：来自 GHC.TypeLits 的内置 Nat 和来自 Data.Type.Natural 的 classic Peano 数字。前者需要提供漂亮的 iterate' @3 语法，后者需要执行递归（发生在 Iterate class 中）。我使用 Data.Type.Natural.Builtin 将文字转换为相应的 Peano 数字。

[1] 但是，给定一种使用迭代值的特定方式（例如，如果您事先知道您只想 show 它们），您可能甚至可以调整此代码以使其工作n 的动态值。 iterate' 类型中没有任何东西需要静态已知的 Nat；唯一的挑战是证明迭代的结果满足您需要的约束。

Answer 3

您可以在没有模板 Haskell 或类型级 Nats 的情况下执行此操作。您正在构建的那种深度可变递归类型实际上非常适合自由 monad 的模型。我们可以使用 unfold function from the free 包构建一个 Free 结构并在我们的计数器达到 0.

时短路

-- This extension is enabled so we can have nice type annotations
{-# Language ScopedTypeVariables #-}

import Control.Monad.Free (Free)
import qualified Control.Monad.Free as Free

iterate' :: forall f a. Functor f => Int -> (a -> f a) -> a -> Free f a
iterate' counter0 f x0 = Free.unfold run (counter0, x0)
  where

    -- If counter is 0, short circuit with current result
    -- Otherwise, continue computation with modified counter
    run :: (Int, a) -> Either a (f (Int, a))
    run (0      , x) = Left x
    run (counter, x) = Right (countDown counter <$> f x)

    countDown :: Int -> a -> (Int, a)
    countDown counter x = (counter - 1, x)

现在，很容易为任何 Functor 创建和消化这些类型的值。

> iterate' 3 Just True
Free (Just (Free (Just (Free (Just (Pure True))))))

> let f i = if i == 1 then Left "abort" else Right (i+1)

> iterate' 0 f 0
Pure 0
> iterate' 1 f 0
Free (Right (Pure 1))
> iterate' 2 f 0
Free (Right (Free (Left "abort")))

如果你的 Functor 恰好也是 Monad，你可以使用 retract 来折叠递归结构。

> Free.retract (iterate' 3 Just True)
Just True
> Free.retract (iterate' 0 f 0)
Right 0
> Free.retract (iterate' 1 f 0)
Right 1
> Free.retract (iterate' 2 f 0)
Left "abort"

我建议阅读 Control.Monad.Free 的文档，这样您就可以了解这些结构是如何 created/consumed。

（顺便说一句，a -> Maybe a 是一个自同态，但它是Maybe的Kleisli范畴中的一个自同态。）

是否可以迭代一个非自同态的应用？

Is it possible to iterate the application of a non-endomorphism?

haskell

template-haskell