0

我试过这个实验：

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

1 回答 1

4

是和不是！

首先，您的类型在函数的签名中不准确。以你的例子为例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在您的示例中），因为我们永远不会达到递归的基础。

但这也不是你想要的！这里的“无限”实际上是一个红鲱鱼：你希望能够包装一些东西有限的次数，使用一个参数来决定包装级别。

你可以用另一个包装器做这样的事情：

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']]]])
于 2019-08-15T22:33:58.700 回答