Возможно ли повторять применение неэндоморфизма?

Ответ 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 ( 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; единственная задача - доказать, что результат итерации удовлетворяет требуемым ограничениям.

Ответ 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 | fa | f (fa) | f (f (fa)) |... a | fa | f (fa) | f (f (fa)) |... a | fa | f (fa) | f (f (fa)) |... Чтобы использовать результат, вам нужно записаться на Iter. Также функция должна иметь вид a → fa для некоторого конструктора типов f, поэтому вам может понадобиться сделать некоторую упаковку newtype, чтобы попасть туда. Так... это как бы боль в любом случае.