haskell - 是否可以在 Haskell 中创建具有 Rank N 类型的无限包装器?
问题描述
我试过这个实验:
{-# 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']]]]
解决方案
是和不是!
首先,您的类型在函数的签名中不准确。以你的例子为例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']]]])
推荐阅读
- mysql - 删除列表框VB.net中的多个相同值
- c# - 查看帖子表单返回null?
- android - 为什么我在这里收到“由:java.lang.ClassCastException:java.lang.Float 无法转换为 java.lang.String”错误?
- java - 为什么我的基本谣言模拟程序不起作用?
- javascript - 自动聚焦下一个输入字段
- python - python - 使用由另一个函数确定的变量
- python-3.x - Anaconda 环境创建
- angular - Nullinjectorerror:没有 FormBuilder 的提供者(我正在导入 ReactiveFormsModule)
- r - R函数比较列
- android - 如何在firebase storage v16.0.1中获取上传图片的url