是否可以在 Haskell 中使用 Rank N 类型创建无限包装器？

Question

我试过这个实验：

{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE RankNTypes #-}

wrapper :: forall a (b :: * -> *). Monad b => Int -> a -> b a
wrapper 1 v = return v
wrapper n v = return $ wrapper (n-1) v

但它给我错误：

 Occurs check: cannot construct the infinite type: a ~ b0 a
      Expected type: b a
        Actual type: b (b0 a)
    • In the expression: return $ wrapper (n - 1) v
      In an equation for ‘wrapper’:
          wrapper n v = return $ wrapper (n - 1) v
    • Relevant bindings include
        v :: a (bound at main.hs:7:11)
        wrapper :: Int -> a -> b a (bound at main.hs:6:1)

是否可以创建函数包装器，例如：

wrapper 4 'a' :: [Char]
[[[['a']]]]

Answer 1

是也不是！

首先，函数签名中你的类型不准确。以你的wrapper 4 'a'为例，函数的return类型是m (m (m (m a)))（其中m是[]），而不是m a。

其次，Haskell 的类型系统不允许无限类型，因此即使我们想写也无法写下正确的类型！

也就是说，我们可以使用一些新类型来解决这两个问题，这些新类型将为我们执行类型级递归。首先，有 Fix:

newtype Fix f a = Fix { unFix :: f (Fix f a) }

使用这个我们可以无限循环：

wrap :: Monad m => Fix m a
wrap = Fix $ return $ wrap

如您所见，我们不需要基本元素（示例中的 a），因为我们永远不会达到递归的基数。

但这也不是你想要的！这里的 "infinite" 实际上是一个转移注意力的东西：你希望能够将某些东西包装有限次，使用参数来指定包装级别。

你可以用另一个包装器做一些事情比如：

data Wrap f a = Pure a | Wrap (f (Wrap f a))

wrapper :: Monad f => Int -> a -> Wrap f a
wrapper 0 x = Pure x
wrapper n x = Wrap $ pure $ wrapper (n-1) x

（这实际上是我们在这里使用的免费 monad）

您正在寻找的完全，虽然（即没有包装器）可以完成，但是，它非常复杂，可能不是您正在寻找的。尽管如此，我还是会把它包括在内。

{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE GADTs                #-}
{-# LANGUAGE ScopedTypeVariables  #-}
{-# LANGUAGE FlexibleContexts     #-}
{-# LANGUAGE AllowAmbiguousTypes  #-}
{-# LANGUAGE TypeApplications     #-}

import Data.Kind
import GHC.TypeLits

data N = Z | S N

type family Wrap (n :: N) (f :: Type -> Type) (a :: Type) :: Type where
  Wrap Z f a = a
  Wrap (S n) f a = Wrap n f (f a)

type family FromNat (n :: Nat) :: N where
  FromNat 0 = Z
  FromNat n = S (FromNat (n - 1))

data Ny (n :: N) where
  Zy :: Ny Z
  Sy :: Ny n -> Ny (S n)

class KnownN n where sing :: Ny n
instance KnownN Z where sing = Zy
instance KnownN n => KnownN (S n) where sing = Sy sing

wrap :: forall n f a. (KnownN (FromNat n), Monad f) => a -> Wrap (FromNat n) f a
wrap = go @(FromNat n) @f @a sing
  where
    go :: forall n f a. Monad f => Ny n -> a -> Wrap n f a
    go Zy x = x
    go (Sy n) x = go @_ @f n (return @f x)


main = print (wrap @4 'a' == [[[['a']]]])

是否可以在 Haskell 中使用 Rank N 类型创建无限包装器？

Is posible to create an infinite wrapper in Haskell with Rank N types?

haskell

rank-n-types