haskell - 是否可以迭代非同形的应用？

在Haskell中，如果我想重复将内同性a -> a应用于a类型的值，则可以只使用iterate。

不是内同态但足够通用以在其返回类型上正常工作的函数呢？

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

Just . Just . Just ...

我要多少次有没有一种方法可以像这样写

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

还是我们需要像依赖类型这样的东西？

最佳答案

可能需要稍微修改一下您建议的语法:iterate' @3 Just而不是iterate' 3 Just。

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

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

该代码使用两种不同的类型级自然语言:来自Nat的内置GHC.TypeLits和来自Data.Type.Natural的经典Peano数字。前者需要提供漂亮的iterate' @3语法，后者需要执行递归(这发生在Iterate类中)。我使用Data.Type.Natural.Builtin从文字转换为相应的Peano数字。

[1]但是，给定一种消耗迭代值的特定方式(例如，如果您事先知道只想对它们进行show编码)，则即使对于n的动态值，也可以使此代码适用。 iterate'类型没有什么需要静态已知的Nat；唯一的挑战是证明迭代结果满足您所需的约束。