是否可以在 Haskell 中创建具有 Rank N 类型的无限包装器？答案

【问题标题】：Is posible to create an infinite wrapper in Haskell with Rank N types?是否可以在 Haskell 中创建具有 Rank N 类型的无限包装器？
【发布时间】：2019-12-22 07:24:05
【问题描述】：

我试过这个实验：

{-# 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']]]]

【问题讨论】：

无限类型在任何情况下都是不可能的。您必须将这种复杂性隐藏在构造函数后面。但是，这与无限列表相同，例如foo = () : foo。相关问题：stackoverflow.com/questions/9566683/…

标签： haskell rank-n-types

【解决方案1】：

是和不是！

首先，您的类型在函数签名中不准确。以wrapper 4 'a' 为例，函数的返回类型是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），因为我们永远不会达到递归的基数。

但这也不是你想要的！这里的“无限”实际上是一条红鲱鱼：您希望能够以 finite 次包装某物，使用参数来指定包装级别。

你可以用另一个包装器来做类似的事情：

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']]]])

【讨论】：