如何“迭代”在类型在迭代中改变的函数上，但形式定义是相同的 [英] How to "iterate" over a function whose type changes among iteration but the formal definition is the same

问题描述

我刚开始学习Haskell，遇到以下问题。我尝试迭代函数 \x-> [x] 。我希望得到结果 [[8]] 由

  foldr1 （。）（replicate 2（\x-> [x]））$（8 :: Int）
  

这不起作用，并提供以下错误消息：

发生检查：无法构造无限类型： a〜[a]

预期类型： [a - > a]

实际类型： [a - > [a]]

我可以理解为什么它不起作用。这是因为 foldr1 具有类型签名 foldr1 :: Foldable t => （a - > a - > a） - > a - > t a - > a ，并且取 a - > a - > a 作为其第一个参数的类型签名，而不是 a - > a - > b

$ p





$ p $ （（!! 2）$ iterate（\ x-> [x]）。）id）（8 :: Int）

$ b

然而，这是有效的：



 （\x-> （$ x $）$（8 :: Int）
  



<我知道第一个（\x-> [x]），第二个是不同类型的（即 [Int ] - > [[Int]] 和 Int-> [Int] ），尽管形式上它们看起来一样。

现在说我需要将2改成一个很大的数字，比如100。

我的问题是，有没有办法构建这样的列表？我是否需要使用模板Haskell等元编程技术？如果我不得不求助于元编程，我该怎么做呢？

作为一个边节点，我也尝试构造这样一个列表的字符串表示形式，并且读取它。虽然字符串构造起来更容易，但我不知道如何读取这样的字符串。例如，

  read[[[[[8]]]]:: ?? 
  

我不知道如何构建 ?? 时，$ c>部分。我能想到的唯一方法就是采用元编程。

上面的问题看起来可能不够有趣，而且我有一个现实生活的例子。考虑以下函数：

  natSucc x = [Left x，Right [x]] 
 
这是中使用的 succ  en.wikipedia.org/wiki/Set-theoretic_definition_of_natural_numbersrel =nofollow noreferrer>正式定义自然数。再次，我不能简单地 foldr1-replicate 或 !!  -  iterate 它。
 
 
 
任何帮助将不胜感激。也欢迎对代码样式的建议。
 
 
 
 编辑：
查看到目前为止给出的3个答案（再次感谢大家非常重视您的时间和精力）我意识到这是一个更为普遍的问题，不仅限于列表。类似的问题可以为每个有效类型的函子组成（如果我想得到 Just Just 8 ，虽然这可能没有多大意义，但它本身可能没有多大意义？ ）。
 
解决方案
这个问题确实需要一些高级的类型编程。
 
 
 
我在评论中跟随了@ chi的建议，并且搜索了一个提供归纳类型级别自然和它们相应的单身人士的图书馆。我找到了  fin  库，用于回答。
 
 
 
通常的类型级欺骗扩展： 
 
 
  { - ＃语言DataKinds，PolyKinds，KindSignatures，ScopedTypeVariables，TypeFamilies＃ - } 
  
这里有一个 type family 将类型级别的自然元素和元素类型映射到相应嵌套列表的类型： 
 
 
  import Data。 Type.Nat 
 
类型嵌套（n :: Nat）a其中
嵌套Z a = [a] 
嵌套（S n）a = [嵌套na] 
  
例如，我们可以测试来自ghci  
  * Main> ：类！嵌套Nat3 Int 
嵌套Nat3 Int :: * 
 = [[[[Int]]]] 
  
（  Nat3  是一个在 Data.Type.Nat 中定义的方便别名。）
 
 
 
这里是一个包装我们想要构造的函数的新类型。它使用类型族来表示嵌套的级别。
 
 
  newtype Iterate（n :: Nat）a = Iterate {runIterate :: （a  - > [a]） - > a  - >嵌套na} 
  
  库提供了一个非常漂亮的  induction1  函数，它可以让我们通过归纳 Nat 来计算结果。我们可以用它来计算对应于每个 Nat 的迭代。  Nat 隐式传递 ，作为约束： 
 
 
 迭代':: forall n a。 SNATI n =>迭代（n :: Nat）
迭代'= 
让step :: forall m。 SNatI m =>迭代m a  - >迭代（S m）a 
步骤（迭代recN）=迭代（\ fa  - > [recN fa]）
 in induction1（迭代id）步骤
  
测试ghci中的函数（使用 -XTypeApplications 来提供 Nat ）： 
 
 
  * Main> runIterate（iterate'@Nat3）pure True 
 [[[[True]]]] 
  
 
I have just started learning Haskell and I come across the following problem. I try to "iterate" the function \x->[x]. I expect to get the result [[8]] by
foldr1 (.) (replicate 2 (\x->[x])) $ (8 :: Int)
This does not work, and gives the following error message:

  
Occurs check: cannot construct the infinite type: a ~ [a]
  
  
Expected type: [a -> a]
  
  
Actual type: [a -> [a]]
I can understand why it doesn't work. It is because that foldr1 has type signature foldr1 :: Foldable t => (a -> a -> a) -> a -> t a -> a, and takes a -> a -> a as the type signature of its first parameter, not a -> a -> b

Neither does this, for the same reason:
((!! 2) $ iterate (\x->[x]) .) id) (8 :: Int)
However, this works:
(\x->[x]) $ (\x->[x]) $ (8 :: Int)
and I understand that the first (\x->[x]) and the second one are of different type (namely [Int]->[[Int]] and Int->[Int]), although formally they look the same.

Now say that I need to change the 2 to a large number, say 100. 

My question is, is there a way to construct such a list? Do I have to resort to meta-programming techniques such as Template Haskell? If I have to resort to meta-programming, how can I do it?

As a side node, I have also tried to construct the string representation of such a list and read it. Although the string is much easier to construct, I don't know how to read such a string. For example,
read "[[[[[8]]]]]" :: ??
I don't know how to construct the ?? part when the number of nested layers is not known a priori. The only way I can think of is resorting to meta-programming.

The question above may not seem interesting enough, and I have a "real-life" case. Consider the following function:
natSucc x = [Left x,Right [x]]
This is the succ function used in the formal definition of natural numbers. Again, I cannot simply foldr1-replicate or !!-iterate it.

Any help will be appreciated. Suggestions on code styles are also welcome.

Edit:
After viewing the 3 answers given so far (again, thank you all very much for your time and efforts) I realized this is a more general problem that is not limited to lists. A similar type of problem can be composed for each valid type of functor (what if I want to get Just Just Just 8, although that may not make much sense on its own?).
解决方案
This problem indeed requires somewhat advanced type-level programming.

I followed @chi's suggestion in the comments, and searched for a library that provided inductive type-level naturals with their corresponding singletons. I found the fin library, which is used in the answer.

The usual extensions for type-level trickery:
{-# language DataKinds, PolyKinds, KindSignatures, ScopedTypeVariables, TypeFamilies #-}
Here's a type family that maps a type-level natural and an element type to the type of the corresponding nested list:
import Data.Type.Nat

type family Nested (n::Nat) a where
    Nested Z a = [a]
    Nested (S n) a = [Nested n a]
For example, we can test from ghci that
*Main> :kind! Nested Nat3 Int
Nested Nat3 Int :: *
= [[[[Int]]]]
(Nat3 is a convenient alias defined in Data.Type.Nat.)

And here's a newtype that wraps the function we want to construct. It uses the type family to express the level of nesting
newtype Iterate (n::Nat) a = Iterate { runIterate :: (a -> [a]) -> a -> Nested n a }
The fin library provides a really nifty induction1 function that lets us compute a result by induction on Nat. We can use it to compute the Iterate that corresponds to every Nat. The Nat is passed implicitly, as a constraint:
iterate' :: forall n a. SNatI n => Iterate (n::Nat) a
iterate' =
    let step :: forall m. SNatI m => Iterate m a -> Iterate (S m) a
        step (Iterate recN) = Iterate (\f a -> [recN f a])
    in  induction1 (Iterate id) step
Testing the function in ghci (using -XTypeApplications to supply the Nat):
*Main> runIterate (iterate' @Nat3) pure True
[[[[True]]]]


                        
这篇关于如何“迭代”在类型在迭代中改变的函数上，但形式定义是相同的的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！