是否有可能迭代非内同态的应用？

Question

在Haskell中,如果我想重复将一个内同态a -> a应用于a我可以使用的类型的值iterate.

那个函数不是一个endomorphisms,但通用到足以在返回类型上正常工作？

考虑一下Just :: a -> Maybe a; 我可以写

Just . Just . Just ...

我想要多次.有没有办法用这样的东西写这个

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

或者我们需要像依赖类型这样的东西吗？

Answer 1

可以通过对您提出的语法进行微调: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))

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

[1]但是,给定一种消耗迭代值的特定方法(例如,如果您事先知道您只需要show它们),您可能可以调整此代码以便即使对于动态值也是如此n.这种类型中没有任何东西iterate'需要静态知道Nat; 唯一的挑战是证明迭代的结果满足您需要的约束.

Answer 2

你可以用模板haskell来做,如果你知道编译时的数字(但除非数字很大,我认为这不值得麻烦).如果您在编译时尚未知道该数字,则需要正确建模返回类型,我们可以使用非常规类型:

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.此函数也必须是a -> f a某种类型构造函数的形式f,因此您可能需要执行一些newtype包装才能实现.所以......无论哪种方式都是痛苦的.